feat(Algebra): Submodule R A is algebra over Ideal A (#18493)

alreadydone · alreadydone · commit 72194f73ba22 · 2024-11-18T16:07:34.000Z
Also upgrade `Submodule.mapHom` and `Ideal.mapHom` to RingHoms and show the former is also an `AlgHom` (`Submodule.mapAlgHom`).
diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean
@@ -159,6 +159,9 @@ theorem mul_le_mul_left (h : M ≤ N) : M * P ≤ N * P :=
 theorem mul_le_mul_right (h : N ≤ P) : M * N ≤ M * P :=
   AddSubmonoid.mul_le_mul_right h
 
+theorem mul_comm_of_commute (h : ∀ m ∈ M, ∀ n ∈ N, Commute m n) : M * N = N * M :=
+  toAddSubmonoid_injective <| AddSubmonoid.mul_comm_of_commute h
+
 variable (M N P)
 
 theorem mul_sup : M * (N ⊔ P) = M * N ⊔ M * P :=
@@ -505,14 +508,17 @@ protected theorem pow_induction_on_right {C : A → Prop} (hr : ∀ r : R, C (al
     (fun x y _i _hx _hy => hadd x y)
     (fun _i _x _hx => hmul _) hx
 
-/-- `Submonoid.map` as a `MonoidWithZeroHom`, when applied to `AlgHom`s. -/
+/-- `Submonoid.map` as a `RingHom`, when applied to an `AlgHom`. -/
 @[simps]
 def mapHom {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
-    Submodule R A →*₀ Submodule R A' where
+    Submodule R A →+* Submodule R A' where
   toFun := map f.toLinearMap
   map_zero' := Submodule.map_bot _
+  map_add' := (Submodule.map_sup · · _)
   map_one' := Submodule.map_one _
-  map_mul' _ _ := Submodule.map_mul _ _ _
+  map_mul' := (Submodule.map_mul · · _)
+
+theorem mapHom_id : mapHom (.id R A) = .id _ := RingHom.ext map_id
 
 /-- The ring of submodules of the opposite algebra is isomorphic to the opposite ring of
 submodules. -/
@@ -553,14 +559,11 @@ theorem map_unop_pow (n : ℕ) (M : Submodule R Aᵐᵒᵖ) :
 on either side). -/
 @[simps]
 def span.ringHom : SetSemiring A →+* Submodule R A where
-  -- Note: the hint `(α := A)` is new in https://github.com/leanprover-community/mathlib4/pull/8386
-  toFun s := Submodule.span R (SetSemiring.down (α := A) s)
+  toFun s := Submodule.span R (SetSemiring.down s)
   map_zero' := span_empty
   map_one' := one_eq_span.symm
   map_add' := span_union
-  map_mul' s t := by
-    dsimp only -- Porting note: new, needed due to new-style structures
-    rw [SetSemiring.down_mul, span_mul_span]
+  map_mul' s t := by simp_rw [SetSemiring.down_mul, span_mul_span]
 
 section
 
diff --git a/Mathlib/Algebra/Group/Submonoid/Pointwise.lean b/Mathlib/Algebra/Group/Submonoid/Pointwise.lean
@@ -595,6 +595,10 @@ theorem iSup_mul (S : ι → AddSubmonoid R) (T : AddSubmonoid R) : (⨆ i, S i)
 theorem mul_iSup (T : AddSubmonoid R) (S : ι → AddSubmonoid R) : (T * ⨆ i, S i) = ⨆ i, T * S i :=
   smul_iSup T S
 
+theorem mul_comm_of_commute (h : ∀ m ∈ M, ∀ n ∈ N, Commute m n) : M * N = N * M :=
+  le_antisymm (mul_le.mpr fun m hm n hn ↦ h m hm n hn ▸ mul_mem_mul hn hm)
+    (mul_le.mpr fun n hn m hm ↦ h m hm n hn ▸ mul_mem_mul hm hn)
+
 end NonUnitalNonAssocSemiring
 
 section NonUnitalNonAssocRing
diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean
@@ -248,15 +248,16 @@ theorem smul_top_eq_map {R S : Type*} [CommSemiring R] [CommSemiring S] [Algebra
     congrArg _ <| Eq.trans (Ideal.smul_eq_mul _ _) (Ideal.mul_top _)
 
 @[simp]
-theorem coe_restrictScalars {R S : Type*} [CommSemiring R] [Semiring S] [Algebra R S]
-    (I : Ideal S) : (I.restrictScalars R : Set S) = ↑I :=
+theorem coe_restrictScalars {R S : Type*} [Semiring R] [Semiring S] [Module R S]
+    [IsScalarTower R S S] (I : Ideal S) : (I.restrictScalars R : Set S) = ↑I :=
   rfl
 
 /-- The smallest `S`-submodule that contains all `x ∈ I * y ∈ J`
 is also the smallest `R`-submodule that does so. -/
 @[simp]
-theorem restrictScalars_mul {R S : Type*} [CommSemiring R] [CommSemiring S] [Algebra R S]
-    (I J : Ideal S) : (I * J).restrictScalars R = I.restrictScalars R * J.restrictScalars R :=
+theorem restrictScalars_mul {R S : Type*} [Semiring R] [Semiring S] [Module R S]
+    [IsScalarTower R S S] (I J : Ideal S) :
+    (I * J).restrictScalars R = I.restrictScalars R * J.restrictScalars R :=
   rfl
 
 section Surjective
@@ -493,13 +494,13 @@ end Ring
 
 section CommRing
 
-variable {F : Type*} [CommRing R] [CommRing S]
+variable {F : Type*} [CommSemiring R] [CommSemiring S]
 variable [FunLike F R S] [rc : RingHomClass F R S]
 variable (f : F)
-variable {I J : Ideal R} {K L : Ideal S}
-variable (I J K L)
+variable (I J : Ideal R) (K L : Ideal S)
 
-theorem map_mul : map f (I * J) = map f I * map f J :=
+theorem map_mul {R} [Semiring R] [FunLike F R S] [RingHomClass F R S] (f : F) (I J : Ideal R) :
+    map f (I * J) = map f I * map f J :=
   le_antisymm
     (map_le_iff_le_comap.2 <|
       mul_le.2 fun r hri s hsj =>
@@ -511,12 +512,13 @@ theorem map_mul : map f (I * J) = map f I * map f J :=
           Set.singleton_subset_iff.2 <|
             hfri ▸ hfsj ▸ by rw [← _root_.map_mul]; exact mem_map_of_mem f (mul_mem_mul hri hsj)))
 
-/-- The pushforward `Ideal.map` as a monoid-with-zero homomorphism. -/
+/-- The pushforward `Ideal.map` as a (semi)ring homomorphism. -/
 @[simps]
-def mapHom : Ideal R →*₀ Ideal S where
+def mapHom : Ideal R →+* Ideal S where
   toFun := map f
-  map_mul' I J := Ideal.map_mul f I J
+  map_mul' := Ideal.map_mul f
   map_one' := by simp only [one_eq_top]; exact Ideal.map_top f
+  map_add' I J := Ideal.map_sup f I J
   map_zero' := Ideal.map_bot
 
 protected theorem map_pow (n : ℕ) : map f (I ^ n) = map f I ^ n :=
diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean
@@ -1241,7 +1241,6 @@ namespace Submodule
 variable {R : Type u} {M : Type v}
 variable [CommSemiring R] [AddCommMonoid M] [Module R M]
 
--- TODO: show `[Algebra R A] : Algebra (Ideal R) A` too
 instance moduleSubmodule : Module (Ideal R) (Submodule R M) where
   smul_add := smul_sup
   add_smul := sup_smul
@@ -1260,6 +1259,39 @@ theorem set_smul_top_eq_span (s : Set R) :
     s • ⊤ = Ideal.span s :=
   (span_smul_eq s ⊤).symm.trans (Ideal.span s).mul_top
 
+variable {A B} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
+
+open Submodule
+
+instance algebraIdeal : Algebra (Ideal R) (Submodule R A) where
+  __ := moduleSubmodule
+  toFun := map (Algebra.linearMap R A)
+  map_one' := by
+    rw [one_eq_span, map_span, Set.image_singleton, Algebra.linearMap_apply, map_one, one_eq_span]
+  map_mul' := (Submodule.map_mul · · <| Algebra.ofId R A)
+  map_zero' := map_bot _
+  map_add' := (map_sup · · _)
+  commutes' I M := mul_comm_of_commute <| by rintro _ ⟨r, _, rfl⟩ a _; apply Algebra.commutes
+  smul_def' I M := le_antisymm (smul_le.mpr fun r hr a ha ↦ by
+    rw [Algebra.smul_def]; exact Submodule.mul_mem_mul ⟨r, hr, rfl⟩ ha) (Submodule.mul_le.mpr <| by
+    rintro _ ⟨r, hr, rfl⟩ a ha; rw [Algebra.linearMap_apply, ← Algebra.smul_def]
+    exact Submodule.smul_mem_smul hr ha)
+
+/-- `Submonoid.map` as an `AlgHom`, when applied to an `AlgHom`. -/
+@[simps!] def mapAlgHom (f : A →ₐ[R] B) : Submodule R A →ₐ[Ideal R] Submodule R B where
+  __ := mapHom f
+  commutes' I := (map_comp _ _ I).symm.trans (congr_arg (map · I) <| LinearMap.ext f.commutes)
+
+/-- `Submonoid.map` as an `AlgEquiv`, when applied to an `AlgEquiv`. -/
+-- TODO: when A, B noncommutative, still has `MulEquiv`.
+@[simps!] def mapAlgEquiv (f : A ≃ₐ[R] B) : Submodule R A ≃ₐ[Ideal R] Submodule R B where
+  __ := mapAlgHom f
+  invFun := mapAlgHom f.symm
+  left_inv I := (map_comp _ _ I).symm.trans <|
+    (congr_arg (map · I) <| LinearMap.ext (f.left_inv ·)).trans (map_id I)
+  right_inv I := (map_comp _ _ I).symm.trans <|
+    (congr_arg (map · I) <| LinearMap.ext (f.right_inv ·)).trans (map_id I)
+
 end Submodule
 
 instance {R} [Semiring R] : NonUnitalSubsemiringClass (Ideal R) R where
