refactor: change the definition of 1 : Submodule R A to the image o…

…f `(· • 1)`

Mathlib/Algebra/Algebra/Bilinear.lean

@@ -215,6 +215,9 @@ theorem pow_mulRight (a : A) (n : ℕ) : mulRight R a ^ n = mulRight R (a ^ n) :
   exact
     LinearMap.coe_injective (((mulRight R a).coe_pow n).symm ▸ mul_right_iterate a n)
 
+theorem toSpanSingleton_eq_algebra_linearMap : toSpanSingleton R A 1 = Algebra.linearMap R A := by
+  ext; simp
+
 end Semiring
 
 section Ring

Mathlib/Algebra/Algebra/Operations.lean

@@ -36,6 +36,11 @@ It is proved that `Submodule R A` is a semiring, and also an algebra over `Set A
 Additionally, in the `Pointwise` locale we promote `Submodule.pointwiseDistribMulAction` to a
 `MulSemiringAction` as `Submodule.pointwiseMulSemiringAction`.
 
+When `R` is not necessarily commutative, and `A` is merely a `R`-module with a ring structure
+such that `IsScalarTower R A A` holds (equivalent to the data of a ring homomorphism `R →+* A`
+by `ringHomEquivModuleIsScalarTower`), we can still define `1 : Submodule R A` and
+`Mul (Submodule R A)`, but `1` is only a left identity, not necessarily a right one.
+
 ## Tags
 
 multiplication of submodules, division of submodules, submodule semiring
@@ -62,49 +67,53 @@ end SubMulAction
 
 namespace Submodule
 
-variable {ι : Sort uι}
-variable {R : Type u} [CommSemiring R]
+section Module
 
-section Ring
-
-variable {A : Type v} [Semiring A] [Algebra R A]
-variable (S T : Set A) {M N P Q : Submodule R A} {m n : A}
+variable {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A]
 
-/-- `1 : Submodule R A` is the submodule R of A. -/
+/-- `1 : Submodule R A` is the submodule `R ∙ 1` of A. -/
 instance one : One (Submodule R A) :=
-  -- Porting note: `f.range` notation doesn't work
-  ⟨LinearMap.range (Algebra.linearMap R A)⟩
+  ⟨LinearMap.range (LinearMap.toSpanSingleton R A 1)⟩
 
-theorem one_eq_range : (1 : Submodule R A) = LinearMap.range (Algebra.linearMap R A) :=
-  rfl
+theorem one_eq_span : (1 : Submodule R A) = R ∙ 1 :=
+  (LinearMap.span_singleton_eq_range _ _ _).symm
 
 theorem le_one_toAddSubmonoid : 1 ≤ (1 : Submodule R A).toAddSubmonoid := by
   rintro x ⟨n, rfl⟩
-  exact ⟨n, map_natCast (algebraMap R A) n⟩
-
-theorem algebraMap_mem (r : R) : algebraMap R A r ∈ (1 : Submodule R A) :=
-  LinearMap.mem_range_self (Algebra.linearMap R A) _
-
-@[simp]
-theorem mem_one {x : A} : x ∈ (1 : Submodule R A) ↔ ∃ y, algebraMap R A y = x :=
-  Iff.rfl
+  exact ⟨n, show (n : R) • (1 : A) = n by rw [Nat.cast_smul_eq_nsmul, nsmul_one]⟩
 
 @[simp]
 theorem toSubMulAction_one : (1 : Submodule R A).toSubMulAction = 1 :=
-  SetLike.ext fun _ => mem_one.trans SubMulAction.mem_one'.symm
-
-theorem one_eq_span : (1 : Submodule R A) = R ∙ 1 := by
-  apply Submodule.ext
-  intro a
-  simp only [mem_one, mem_span_singleton, Algebra.smul_def, mul_one]
+  SetLike.ext fun _ ↦ by rw [one_eq_span, SubMulAction.mem_one]; exact mem_span_singleton
 
 theorem one_eq_span_one_set : (1 : Submodule R A) = span R 1 :=
   one_eq_span
 
-theorem one_le : (1 : Submodule R A) ≤ P ↔ (1 : A) ∈ P := by
+theorem one_le {P : Submodule R A} : (1 : Submodule R A) ≤ P ↔ (1 : A) ∈ P := by
   -- Porting note: simpa no longer closes refl goals, so added `SetLike.mem_coe`
   simp only [one_eq_span, span_le, Set.singleton_subset_iff, SetLike.mem_coe]
 
+end Module
+
+variable {ι : Sort uι}
+variable {R : Type u} [CommSemiring R]
+
+section Ring
+
+variable {A : Type v} [Semiring A] [Algebra R A]
+variable (S T : Set A) {M N P Q : Submodule R A} {m n : A}
+
+theorem one_eq_range : (1 : Submodule R A) = LinearMap.range (Algebra.linearMap R A) := by
+  rw [one_eq_span, LinearMap.span_singleton_eq_range,
+    LinearMap.toSpanSingleton_eq_algebra_linearMap]
+
+theorem algebraMap_mem (r : R) : algebraMap R A r ∈ (1 : Submodule R A) := by
+  rw [one_eq_range]; exact LinearMap.mem_range_self _ _
+
+@[simp]
+theorem mem_one {x : A} : x ∈ (1 : Submodule R A) ↔ ∃ y, algebraMap R A y = x := by
+  rw [one_eq_range]; rfl
+
 protected theorem map_one {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
     map f.toLinearMap (1 : Submodule R A) = 1 := by
   ext
@@ -425,7 +434,7 @@ protected theorem pow_induction_on_left' {C : ∀ (n : ℕ) (x), x ∈ M ^ n →
   induction n generalizing x with
   | zero =>
     rw [pow_zero] at hx
-    obtain ⟨r, rfl⟩ := hx
+    obtain ⟨r, rfl⟩ := mem_one.mp hx
     exact algebraMap r
   | succ n n_ih =>
     revert hx
@@ -446,7 +455,7 @@ protected theorem pow_induction_on_right' {C : ∀ (n : ℕ) (x), x ∈ M ^ n 
   induction n generalizing x with
   | zero =>
     rw [pow_zero] at hx
-    obtain ⟨r, rfl⟩ := hx
+    obtain ⟨r, rfl⟩ := mem_one.mp hx
     exact algebraMap r
   | succ n n_ih =>
     revert hx

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -777,7 +777,8 @@ instance : Inhabited (Subalgebra R A) := ⟨⊥⟩
 
 theorem mem_bot {x : A} : x ∈ (⊥ : Subalgebra R A) ↔ x ∈ Set.range (algebraMap R A) := Iff.rfl
 
-theorem toSubmodule_bot : Subalgebra.toSubmodule (⊥ : Subalgebra R A) = 1 := rfl
+theorem toSubmodule_bot : Subalgebra.toSubmodule (⊥ : Subalgebra R A) = 1 :=
+  Submodule.one_eq_range.symm
 
 @[simp]
 theorem coe_bot : ((⊥ : Subalgebra R A) : Set A) = Set.range (algebraMap R A) := rfl
@@ -800,7 +801,8 @@ theorem map_top (f : A →ₐ[R] B) : (⊤ : Subalgebra R A).map f = f.range :=
 
 @[simp]
 theorem map_bot (f : A →ₐ[R] B) : (⊥ : Subalgebra R A).map f = ⊥ :=
-  Subalgebra.toSubmodule_injective <| Submodule.map_one _
+  Subalgebra.toSubmodule_injective <| by
+    simpa only [Subalgebra.map_toSubmodule, toSubmodule_bot] using Submodule.map_one _
 
 @[simp]
 theorem comap_top (f : A →ₐ[R] B) : (⊤ : Subalgebra R B).comap f = ⊤ :=

Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean

@@ -51,12 +51,12 @@ lemma le_flip_dualSubmodule {N₁ N₂ : Submodule R M} :
 This is bundled as a bilinear map in `BilinForm.dualSubmoduleToDual`. -/
 noncomputable
 def dualSubmoduleParing {N : Submodule R M} (x : B.dualSubmodule N) (y : N) : R :=
-  (x.prop y y.prop).choose
+  (Submodule.mem_one.mp <| x.prop y y.prop).choose
 
 @[simp]
 lemma dualSubmoduleParing_spec {N : Submodule R M} (x : B.dualSubmodule N) (y : N) :
     algebraMap R S (B.dualSubmoduleParing x y) = B x y :=
-  (x.prop y y.prop).choose_spec
+  (Submodule.mem_one.mp <| x.prop y y.prop).choose_spec
 
 /-- The natural paring of `B.dualSubmodule N` and `N`. -/
 -- TODO: Show that this is perfect when `N` is a lattice and `B` is nondegenerate.
@@ -94,7 +94,7 @@ lemma dualSubmodule_span_of_basis {ι} [Finite ι] [DecidableEq ι]
     rw [← (B.dualBasis hB b).sum_repr x]
     apply sum_mem
     rintro i -
-    obtain ⟨r, hr⟩ := hx (b i) (Submodule.subset_span ⟨_, rfl⟩)
+    obtain ⟨r, hr⟩ := Submodule.mem_one.mp <| hx (b i) (Submodule.subset_span ⟨_, rfl⟩)
     simp only [dualBasis_repr_apply, ← hr, Algebra.linearMap_apply, algebraMap_smul]
     apply Submodule.smul_mem
     exact Submodule.subset_span ⟨_, rfl⟩
@@ -107,7 +107,7 @@ lemma dualSubmodule_span_of_basis {ι} [Finite ι] [DecidableEq ι]
     rw [← IsScalarTower.algebraMap_smul S (f j), map_smul]
     simp_rw [apply_dualBasis_left]
     rw [smul_eq_mul, mul_ite, mul_one, mul_zero, ← (algebraMap R S).map_zero, ← apply_ite]
-    exact ⟨_, rfl⟩
+    exact Submodule.mem_one.mpr ⟨_, rfl⟩
 
 lemma dualSubmodule_dualSubmodule_flip_of_basis {ι : Type*} [Finite ι]
     (hB : B.Nondegenerate) (b : Basis ι S M) :

Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean

@@ -197,8 +197,8 @@ theorem even_induction {motive : ∀ x, x ∈ evenOdd Q 0 → Prop}
           motive (ι Q m₁ * ι Q m₂ * x)
             (zero_add (0 : ZMod 2) ▸ SetLike.mul_mem_graded (ι_mul_ι_mem_evenOdd_zero Q m₁ m₂) hx))
     (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) : motive x hx := by
-  refine evenOdd_induction _ _ (motive := motive) (fun rx => ?_) add ι_mul_ι_mul x hx
-  rintro ⟨r, rfl⟩
+  refine evenOdd_induction _ _ (motive := motive) (fun rx h => ?_) add ι_mul_ι_mul x hx
+  obtain ⟨r, rfl⟩ := Submodule.mem_one.mp h
   exact algebraMap r
 
 /-- To show a property is true on the odd parts, it suffices to show it is true on the

Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean

@@ -271,7 +271,8 @@ theorem rank_eq_one_iff [Nontrivial E] [Module.Free F S] : Module.rank F S = 1 
   obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := F) (M := (⊥ : Subalgebra F E))
   refine le_antisymm ?_ ?_
   · have := lift_rank_range_le (Algebra.linearMap F E)
-    rwa [← one_eq_range, rank_self, lift_one, lift_le_one_iff] at this
+    rwa [← one_eq_range, rank_self, lift_one, lift_le_one_iff,
+      ← Algebra.toSubmodule_bot, rank_toSubmodule] at this
   · by_contra H
     rw [not_le, lt_one_iff_zero] at H
     haveI := mk_eq_zero_iff.1 (H ▸ b.mk_eq_rank'')

Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

@@ -241,7 +241,8 @@ theorem ι_range_disjoint_one :
     Disjoint (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M))
       (1 : Submodule R (ExteriorAlgebra R M)) := by
   rw [Submodule.disjoint_def]
-  rintro _ ⟨x, hx⟩ ⟨r, rfl : algebraMap R (ExteriorAlgebra R M) r = _⟩
+  rintro _ ⟨x, hx⟩ h
+  obtain ⟨r, rfl : algebraMap R (ExteriorAlgebra R M) r = _⟩ := Submodule.mem_one.mp h
   rw [ι_eq_algebraMap_iff x] at hx
   rw [hx.2, RingHom.map_zero]
 

Mathlib/LinearAlgebra/LinearDisjoint.lean

@@ -232,12 +232,12 @@ theorem bot_right : M.LinearDisjoint (⊥ : Submodule R S) :=
 
 /-- The image of `R` in `S` is linearly disjoint with any other submodules. -/
 theorem one_left : (1 : Submodule R S).LinearDisjoint N := by
-  rw [linearDisjoint_iff, mulMap_one_left_eq]
+  rw [linearDisjoint_iff, ← Algebra.toSubmodule_bot, mulMap_one_left_eq]
   exact N.injective_subtype.comp N.lTensorOne.injective
 
 /-- The image of `R` in `S` is linearly disjoint with any other submodules. -/
 theorem one_right : M.LinearDisjoint (1 : Submodule R S) := by
-  rw [linearDisjoint_iff, mulMap_one_right_eq]
+  rw [linearDisjoint_iff, ← Algebra.toSubmodule_bot, mulMap_one_right_eq]
   exact M.injective_subtype.comp M.rTensorOne.injective
 
 /-- If for any finitely generated submodules `M'` of `M`, `M'` and `N` are linearly disjoint,

Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean

@@ -288,7 +288,7 @@ theorem ι_ne_one [Nontrivial R] (x : M) : ι R x ≠ 1 := by
 theorem ι_range_disjoint_one :
     Disjoint (LinearMap.range (ι R : M →ₗ[R] TensorAlgebra R M))
       (1 : Submodule R (TensorAlgebra R M)) := by
-  rw [Submodule.disjoint_def]
+  rw [Submodule.disjoint_def, Submodule.one_eq_range]
   rintro _ ⟨x, hx⟩ ⟨r, rfl⟩
   rw [Algebra.linearMap_apply, ι_eq_algebraMap_iff] at hx
   rw [hx.2, map_zero]

Mathlib/LinearAlgebra/TensorProduct/Submodule.lean

@@ -121,16 +121,17 @@ theorem mulMap'_surjective : Function.Surjective (mulMap' M N) := by
 `i(R) ⊗[R] N →ₗ[R] N` induced by multiplication in `S`, here `i : R → S` is the structure map.
 This is promoted to an isomorphism of `R`-modules as `Submodule.lTensorOne`. Use that instead. -/
 def lTensorOne' : (⊥ : Subalgebra R S) ⊗[R] N →ₗ[R] N :=
-  show (1 : Submodule R S) ⊗[R] N →ₗ[R] N from
-    (LinearEquiv.ofEq _ _ (by rw [mulMap_range, one_mul])).toLinearMap ∘ₗ (mulMap _ N).rangeRestrict
+  show Subalgebra.toSubmodule ⊥ ⊗[R] N →ₗ[R] N from
+    (LinearEquiv.ofEq _ _ (by rw [Algebra.toSubmodule_bot, mulMap_range, one_mul])).toLinearMap ∘ₗ
+      (mulMap _ N).rangeRestrict
 
 variable {N} in
 @[simp]
 theorem lTensorOne'_tmul (y : R) (n : N) :
     N.lTensorOne' (algebraMap R _ y ⊗ₜ[R] n) = y • n := Subtype.val_injective <| by
   simp_rw [lTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
     LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul, Algebra.smul_def]
-  exact mulMap_tmul 1 N _ _
+  exact mulMap_tmul _ N _ _
 
 variable {N} in
 @[simp]
@@ -163,15 +164,17 @@ variable {N} in
 @[simp]
 theorem lTensorOne_symm_apply (n : N) : N.lTensorOne.symm n = 1 ⊗ₜ[R] n := rfl
 
-theorem mulMap_one_left_eq : mulMap 1 N = N.subtype ∘ₗ N.lTensorOne.toLinearMap :=
+theorem mulMap_one_left_eq :
+    mulMap (Subalgebra.toSubmodule ⊥) N = N.subtype ∘ₗ N.lTensorOne.toLinearMap :=
   TensorProduct.ext' fun _ _ ↦ rfl
 
 /-- If `M` is a submodule in an algebra `S` over `R`, there is the natural `R`-linear map
 `M ⊗[R] i(R) →ₗ[R] M` induced by multiplication in `S`, here `i : R → S` is the structure map.
 This is promoted to an isomorphism of `R`-modules as `Submodule.rTensorOne`. Use that instead. -/
 def rTensorOne' : M ⊗[R] (⊥ : Subalgebra R S) →ₗ[R] M :=
-  show M ⊗[R] (1 : Submodule R S) →ₗ[R] M from
-    (LinearEquiv.ofEq _ _ (by rw [mulMap_range, mul_one])).toLinearMap ∘ₗ (mulMap M _).rangeRestrict
+  show M ⊗[R] Subalgebra.toSubmodule ⊥ →ₗ[R] M from
+    (LinearEquiv.ofEq _ _ (by rw [Algebra.toSubmodule_bot, mulMap_range, mul_one])).toLinearMap ∘ₗ
+      (mulMap M _).rangeRestrict
 
 variable {M} in
 @[simp]
@@ -180,7 +183,7 @@ theorem rTensorOne'_tmul (y : R) (m : M) :
   simp_rw [rTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
     LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul]
   rw [Algebra.smul_def, Algebra.commutes]
-  exact mulMap_tmul M 1 _ _
+  exact mulMap_tmul M _ _ _
 
 variable {M} in
 @[simp]
@@ -213,7 +216,8 @@ variable {M} in
 @[simp]
 theorem rTensorOne_symm_apply (m : M) : M.rTensorOne.symm m = m ⊗ₜ[R] 1 := rfl
 
-theorem mulMap_one_right_eq : mulMap M 1 = M.subtype ∘ₗ M.rTensorOne.toLinearMap :=
+theorem mulMap_one_right_eq :
+    mulMap M (Subalgebra.toSubmodule ⊥) = M.subtype ∘ₗ M.rTensorOne.toLinearMap :=
   TensorProduct.ext' fun _ _ ↦ rfl
 
 @[simp]

Mathlib/RingTheory/DedekindDomain/Different.lean

@@ -57,7 +57,7 @@ namespace Submodule
 
 lemma mem_traceDual {I : Submodule B L} {x} :
     x ∈ Iᵛ ↔ ∀ a ∈ I, traceForm K L x a ∈ (algebraMap A K).range :=
-  Iff.rfl
+  forall₂_congr fun _ _ ↦ mem_one
 
 lemma le_traceDual_iff_map_le_one {I J : Submodule B L} :
     I ≤ Jᵛ ↔ ((I * J : Submodule B L).restrictScalars A).map
@@ -147,14 +147,15 @@ variable [IsIntegrallyClosed A]
 
 lemma Submodule.mem_traceDual_iff_isIntegral {I : Submodule B L} {x} :
     x ∈ Iᵛ ↔ ∀ a ∈ I, IsIntegral A (traceForm K L x a) :=
-  forall₂_congr (fun _ _ ↦ IsIntegrallyClosed.isIntegral_iff.symm)
+  forall₂_congr fun _ _ ↦ mem_one.trans IsIntegrallyClosed.isIntegral_iff.symm
 
 variable [FiniteDimensional K L] [IsIntegralClosure B A L]
 
 lemma Submodule.one_le_traceDual_one :
     (1 : Submodule B L) ≤ 1ᵛ := by
-  rw [le_traceDual_iff_map_le_one, mul_one]
+  rw [le_traceDual_iff_map_le_one, mul_one, one_eq_range]
   rintro _ ⟨x, ⟨x, rfl⟩, rfl⟩
+  rw [mem_one]
   apply IsIntegrallyClosed.isIntegral_iff.mp
   apply isIntegral_trace
   rw [IsIntegralClosure.isIntegral_iff (A := B)]
@@ -260,7 +261,7 @@ variable {A K L B}
 
 lemma mem_dual (hI : I ≠ 0) {x} :
     x ∈ dual A K I ↔ ∀ a ∈ I, traceForm K L x a ∈ (algebraMap A K).range := by
-  rw [dual, dif_neg hI]; rfl
+  rw [dual, dif_neg hI]; exact forall₂_congr fun _ _ ↦ mem_one
 
 variable (A K)
 
@@ -298,6 +299,7 @@ lemma le_dual_inv_aux (hI : I ≠ 0) (hIJ : I * J ≤ 1) :
     J ≤ dual A K I := by
   rw [dual, dif_neg hI]
   intro x hx y hy
+  rw [mem_one]
   apply IsIntegrallyClosed.isIntegral_iff.mp
   apply isIntegral_trace
   rw [IsIntegralClosure.isIntegral_iff (A := B)]
@@ -410,7 +412,7 @@ lemma coeSubmodule_differentIdeal_fractionRing
   simp only [← one_div, FractionalIdeal.val_eq_coe] at this
   rw [FractionalIdeal.coe_div (FractionalIdeal.dual_ne_zero _ _ _),
     FractionalIdeal.coe_dual] at this
-  · simpa only [FractionalIdeal.coe_one] using this
+  · simpa only [FractionalIdeal.coe_one, Submodule.one_eq_range] using this
   · exact one_ne_zero
   · exact one_ne_zero
 
@@ -557,7 +559,7 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B]
     derivative_map, aeval_map_algebraMap, aeval_algebraMap_apply, mul_assoc,
     FractionalIdeal.mem_one_iff, forall_exists_index, forall_apply_eq_imp_iff]
   simp_rw [← IsScalarTower.toAlgHom_apply A B L x, ← AlgHom.map_adjoin_singleton]
-  simp only [Subalgebra.mem_map, IsScalarTower.coe_toAlgHom',
+  simp only [Subalgebra.mem_map, IsScalarTower.coe_toAlgHom', Submodule.one_eq_range,
     forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, ← _root_.map_mul]
   exact ⟨fun H b ↦ (mul_one b) ▸ H b 1 (one_mem _), fun H _ _ _ ↦ H _⟩
 

Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

@@ -95,7 +95,7 @@ theorem IsIntegralClosure.range_le_span_dualBasis [Algebra.IsSeparable K L] {ι
   rintro _ ⟨i, rfl⟩ _ ⟨y, rfl⟩
   simp only [LinearMap.coe_restrictScalars, linearMap_apply, LinearMap.BilinForm.flip_apply,
     traceForm_apply]
-  refine IsIntegrallyClosed.isIntegral_iff.mp ?_
+  refine Submodule.mem_one.mpr <| IsIntegrallyClosed.isIntegral_iff.mp ?_
   exact isIntegral_trace ((IsIntegralClosure.isIntegral A L y).algebraMap.mul (hb_int i))
 
 theorem integralClosure_le_span_dualBasis [Algebra.IsSeparable K L] {ι : Type*} [Fintype ι]

Mathlib/RingTheory/FractionalIdeal/Basic.lean

@@ -215,7 +215,7 @@ theorem isFractional_of_le_one (I : Submodule R P) (h : I ≤ 1) : IsFractional
   use 1, S.one_mem
   intro b hb
   rw [one_smul]
-  obtain ⟨b', b'_mem, rfl⟩ := h hb
+  obtain ⟨b', b'_mem, rfl⟩ := mem_one.mp (h hb)
   exact Set.mem_range_self b'
 
 theorem isFractional_of_le {I : Submodule R P} {J : FractionalIdeal S P} (hIJ : I ≤ J) :