chore(Algebra/Algebra): split Subalgebra.Basic (#12267)

This PR was supposed to be simultaneous with #12090 but I got ill last week. This is based on seeing the import `Algebra.Algebra.Subalgebra.Basic → RingTheory.Ideal.Operations` on the [longest pole](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20long.20pole.20in.20mathlib/near/432898637). It feels like `Ideal.Operations` should not be needed to define the notion of subalgebra, only to construct some interesting examples. So I removed the import and split off anything that wouldn't fit. The following results and their corollaries were split off: * `Subalgebra.prod` * `Subalgebra.iSupLift` * `AlgHom.ker_rangeRestrict` * `Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem` Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
leanprover-community · Apr 20, 2024 · 4e9bd1d · 4e9bd1d
1 parent 28c79ff
commit 4e9bd1d
Show file tree

Hide file tree

Showing 13 changed files with 259 additions and 171 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -14,8 +14,11 @@ import Mathlib.Algebra.Algebra.Quasispectrum
 import Mathlib.Algebra.Algebra.RestrictScalars
 import Mathlib.Algebra.Algebra.Spectrum
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
+import Mathlib.Algebra.Algebra.Subalgebra.Directed
+import Mathlib.Algebra.Algebra.Subalgebra.Operations
 import Mathlib.Algebra.Algebra.Subalgebra.Order
 import Mathlib.Algebra.Algebra.Subalgebra.Pointwise
+import Mathlib.Algebra.Algebra.Subalgebra.Prod
 import Mathlib.Algebra.Algebra.Subalgebra.Tower
 import Mathlib.Algebra.Algebra.Subalgebra.Unitization
 import Mathlib.Algebra.Algebra.Tower

diff --git a/Mathlib/Algebra/Algebra/Spectrum.lean b/Mathlib/Algebra/Algebra/Spectrum.lean
@@ -5,6 +5,7 @@ Authors: Jireh Loreaux
 -/
 import Mathlib.Algebra.Star.Pointwise
 import Mathlib.Algebra.Star.Subalgebra
+import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.Tactic.NoncommRing
 
 #align_import algebra.algebra.spectrum from "leanprover-community/mathlib"@"58a272265b5e05f258161260dd2c5d247213cbd3"

diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
@@ -3,11 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
-import Mathlib.Algebra.Algebra.Basic
-import Mathlib.Algebra.Algebra.Prod
-import Mathlib.Data.Set.UnionLift
-import Mathlib.LinearAlgebra.Finsupp
-import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.Algebra.Algebra.Operations
 
 #align_import algebra.algebra.subalgebra.basic from "leanprover-community/mathlib"@"b915e9392ecb2a861e1e766f0e1df6ac481188ca"
 
@@ -630,9 +626,6 @@ theorem rangeRestrict_surjective (f : A →ₐ[R] B) : Function.Surjective (f.ra
     let ⟨x, hx⟩ := hy
     ⟨x, SetCoe.ext hx⟩
 
-theorem ker_rangeRestrict (f : A →ₐ[R] B) : RingHom.ker f.rangeRestrict = RingHom.ker f :=
-  Ideal.ext fun _ ↦ Subtype.ext_iff
-
 /-- The equalizer of two R-algebra homomorphisms -/
 def equalizer (ϕ ψ : A →ₐ[R] B) : Subalgebra R A where
   carrier := { a | ϕ a = ψ a }
@@ -1079,125 +1072,6 @@ theorem coe_equivMapOfInjective_apply (x : S) : ↑(equivMapOfInjective S f hf x
 
 end equivMapOfInjective
 
-section Prod
-
-variable (S₁ : Subalgebra R B)
-
-/-- The product of two subalgebras is a subalgebra. -/
-def prod : Subalgebra R (A × B) :=
-  { S.toSubsemiring.prod S₁.toSubsemiring with
-    carrier := S ×ˢ S₁
-    algebraMap_mem' := fun _ => ⟨algebraMap_mem _ _, algebraMap_mem _ _⟩ }
-#align subalgebra.prod Subalgebra.prod
-
-@[simp]
-theorem coe_prod : (prod S S₁ : Set (A × B)) = (S : Set A) ×ˢ (S₁ : Set B) :=
-  rfl
-#align subalgebra.coe_prod Subalgebra.coe_prod
-
-open Subalgebra in
-theorem prod_toSubmodule : toSubmodule (S.prod S₁) = (toSubmodule S).prod (toSubmodule S₁) := rfl
-#align subalgebra.prod_to_submodule Subalgebra.prod_toSubmodule
-
-@[simp]
-theorem mem_prod {S : Subalgebra R A} {S₁ : Subalgebra R B} {x : A × B} :
-    x ∈ prod S S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁ := Set.mem_prod
-#align subalgebra.mem_prod Subalgebra.mem_prod
-
-@[simp]
-theorem prod_top : (prod ⊤ ⊤ : Subalgebra R (A × B)) = ⊤ := by ext; simp
-#align subalgebra.prod_top Subalgebra.prod_top
-
-theorem prod_mono {S T : Subalgebra R A} {S₁ T₁ : Subalgebra R B} :
-    S ≤ T → S₁ ≤ T₁ → prod S S₁ ≤ prod T T₁ :=
-  Set.prod_mono
-#align subalgebra.prod_mono Subalgebra.prod_mono
-
-@[simp]
-theorem prod_inf_prod {S T : Subalgebra R A} {S₁ T₁ : Subalgebra R B} :
-    S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁) :=
-  SetLike.coe_injective Set.prod_inter_prod
-#align subalgebra.prod_inf_prod Subalgebra.prod_inf_prod
-
-end Prod
-
-section iSupLift
-
-variable {ι : Type*} [Nonempty ι] {K : ι → Subalgebra R A} (dir : Directed (· ≤ ·) K)
-
-theorem coe_iSup_of_directed : ↑(iSup K) = ⋃ i, (K i : Set A) :=
-  let s : Subalgebra R A :=
-    { __ := Subsemiring.copy _ _ (Subsemiring.coe_iSup_of_directed dir).symm
-      algebraMap_mem' := fun _ ↦ Set.mem_iUnion.2
-        ⟨Classical.arbitrary ι, Subalgebra.algebraMap_mem _ _⟩ }
-  have : iSup K = s := le_antisymm
-    (iSup_le fun i ↦ le_iSup (fun i ↦ (K i : Set A)) i) (Set.iUnion_subset fun _ ↦ le_iSup K _)
-  this.symm ▸ rfl
-#align subalgebra.coe_supr_of_directed Subalgebra.coe_iSup_of_directed
-
-variable (K)
-variable (f : ∀ i, K i →ₐ[R] B) (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h))
-  (T : Subalgebra R A) (hT : T = iSup K)
-
--- Porting note (#11215): TODO: turn `hT` into an assumption `T ≤ iSup K`.
--- That's what `Set.iUnionLift` needs
--- Porting note: the proofs of `map_{zero,one,add,mul}` got a bit uglier, probably unification trbls
-/-- Define an algebra homomorphism on a directed supremum of subalgebras by defining
-it on each subalgebra, and proving that it agrees on the intersection of subalgebras. -/
-noncomputable def iSupLift : ↥T →ₐ[R] B :=
-  { toFun := Set.iUnionLift (fun i => ↑(K i)) (fun i x => f i x)
-        (fun i j x hxi hxj => by
-          let ⟨k, hik, hjk⟩ := dir i j
-          dsimp
-          rw [hf i k hik, hf j k hjk]
-          rfl)
-        T (by rw [hT, coe_iSup_of_directed dir])
-    map_one' := by apply Set.iUnionLift_const _ (fun _ => 1) <;> simp
-    map_zero' := by dsimp; apply Set.iUnionLift_const _ (fun _ => 0) <;> simp
-    map_mul' := by
-      subst hT; dsimp
-      apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
-      on_goal 3 => rw [coe_iSup_of_directed dir]
-      all_goals simp
-    map_add' := by
-      subst hT; dsimp
-      apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
-      on_goal 3 => rw [coe_iSup_of_directed dir]
-      all_goals simp
-    commutes' := fun r => by
-      dsimp
-      apply Set.iUnionLift_const _ (fun _ => algebraMap R _ r) <;> simp }
-#align subalgebra.supr_lift Subalgebra.iSupLift
-
-variable {K dir f hf T hT}
-
-@[simp]
-theorem iSupLift_inclusion {i : ι} (x : K i) (h : K i ≤ T) :
-    iSupLift K dir f hf T hT (inclusion h x) = f i x := by
-  dsimp [iSupLift, inclusion]
-  rw [Set.iUnionLift_inclusion]
-#align subalgebra.supr_lift_inclusion Subalgebra.iSupLift_inclusion
-
-@[simp]
-theorem iSupLift_comp_inclusion {i : ι} (h : K i ≤ T) :
-    (iSupLift K dir f hf T hT).comp (inclusion h) = f i := by ext; simp
-#align subalgebra.supr_lift_comp_inclusion Subalgebra.iSupLift_comp_inclusion
-
-@[simp]
-theorem iSupLift_mk {i : ι} (x : K i) (hx : (x : A) ∈ T) :
-    iSupLift K dir f hf T hT ⟨x, hx⟩ = f i x := by
-  dsimp [iSupLift, inclusion]
-  rw [Set.iUnionLift_mk]
-#align subalgebra.supr_lift_mk Subalgebra.iSupLift_mk
-
-theorem iSupLift_of_mem {i : ι} (x : T) (hx : (x : A) ∈ K i) :
-    iSupLift K dir f hf T hT x = f i ⟨x, hx⟩ := by
-  dsimp [iSupLift, inclusion]
-  rw [Set.iUnionLift_of_mem]
-#align subalgebra.supr_lift_of_mem Subalgebra.iSupLift_of_mem
-
-end iSupLift
-
 /-! ## Actions by `Subalgebra`s
 
 These are just copies of the definitions about `Subsemiring` starting from
@@ -1387,47 +1261,6 @@ theorem centralizer_univ : centralizer R Set.univ = center R A :=
 
 end Centralizer
 
-/-- Suppose we are given `∑ i, lᵢ * sᵢ = 1` in `S`, and `S'` a subalgebra of `S` that contains
-`lᵢ` and `sᵢ`. To check that an `x : S` falls in `S'`, we only need to show that
-`sᵢ ^ n • x ∈ S'` for some `n` for each `sᵢ`. -/
-theorem mem_of_finset_sum_eq_one_of_pow_smul_mem {S : Type*} [CommRing S] [Algebra R S]
-    (S' : Subalgebra R S) {ι : Type*} (ι' : Finset ι) (s : ι → S) (l : ι → S)
-    (e : ∑ i in ι', l i * s i = 1) (hs : ∀ i, s i ∈ S') (hl : ∀ i, l i ∈ S') (x : S)
-    (H : ∀ i, ∃ n : ℕ, (s i ^ n : S) • x ∈ S') : x ∈ S' := by
-  -- Porting note: needed to add this instance
-  let _i : Algebra { x // x ∈ S' } { x // x ∈ S' } := Algebra.id _
-  suffices x ∈ Subalgebra.toSubmodule (Algebra.ofId S' S).range by
-    obtain ⟨x, rfl⟩ := this
-    exact x.2
-  choose n hn using H
-  let s' : ι → S' := fun x => ⟨s x, hs x⟩
-  let l' : ι → S' := fun x => ⟨l x, hl x⟩
-  have e' : ∑ i in ι', l' i * s' i = 1 := by
-    ext
-    show S'.subtype (∑ i in ι', l' i * s' i) = 1
-    simpa only [map_sum, map_mul] using e
-  have : Ideal.span (s' '' ι') = ⊤ := by
-    rw [Ideal.eq_top_iff_one, ← e']
-    apply sum_mem
-    intros i hi
-    exact Ideal.mul_mem_left _ _ <| Ideal.subset_span <| Set.mem_image_of_mem s' hi
-  let N := ι'.sup n
-  have hN := Ideal.span_pow_eq_top _ this N
-  apply (Algebra.ofId S' S).range.toSubmodule.mem_of_span_top_of_smul_mem _ hN
-  rintro ⟨_, _, ⟨i, hi, rfl⟩, rfl⟩
-  change s' i ^ N • x ∈ _
-  rw [← tsub_add_cancel_of_le (show n i ≤ N from Finset.le_sup hi), pow_add, mul_smul]
-  refine' Submodule.smul_mem _ (⟨_, pow_mem (hs i) _⟩ : S') _
-  exact ⟨⟨_, hn i⟩, rfl⟩
-#align subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem
-
-theorem mem_of_span_eq_top_of_smul_pow_mem {S : Type*} [CommRing S] [Algebra R S]
-    (S' : Subalgebra R S) (s : Set S) (l : s →₀ S) (hs : Finsupp.total s S S (↑) l = 1)
-    (hs' : s ⊆ S') (hl : ∀ i, l i ∈ S') (x : S) (H : ∀ r : s, ∃ n : ℕ, (r : S) ^ n • x ∈ S') :
-    x ∈ S' :=
-  mem_of_finset_sum_eq_one_of_pow_smul_mem S' l.support (↑) l hs (fun x => hs' x.2) hl x H
-#align subalgebra.mem_of_span_eq_top_of_smul_pow_mem Subalgebra.mem_of_span_eq_top_of_smul_pow_mem
-
 end Subalgebra
 
 section Nat

diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Directed.lean b/Mathlib/Algebra/Algebra/Subalgebra/Directed.lean
@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2018 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes
+-/
+
+import Mathlib.Algebra.Algebra.Subalgebra.Basic
+import Mathlib.Data.Set.UnionLift
+
+#align_import algebra.algebra.subalgebra.basic from "leanprover-community/mathlib"@"b915e9392ecb2a861e1e766f0e1df6ac481188ca"
+
+/-!
+# Subalgebras and directed Unions of sets
+
+## Main results
+
+ * `Subalgebra.coe_iSup_of_directed`: a directed supremum consists of the union of the algebras
+ * `Subalgebra.iSupLift`: define an algebra homomorphism on a directed supremum of subalgebras by
+   defining it on each subalgebra, and proving that it agrees on the intersection of subalgebras.
+-/
+
+namespace Subalgebra
+
+open BigOperators Algebra
+
+variable {R A B : Type*} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]
+variable (S : Subalgebra R A)
+
+variable {ι : Type*} [Nonempty ι] {K : ι → Subalgebra R A} (dir : Directed (· ≤ ·) K)
+
+theorem coe_iSup_of_directed : ↑(iSup K) = ⋃ i, (K i : Set A) :=
+  let s : Subalgebra R A :=
+    { __ := Subsemiring.copy _ _ (Subsemiring.coe_iSup_of_directed dir).symm
+      algebraMap_mem' := fun _ ↦ Set.mem_iUnion.2
+        ⟨Classical.arbitrary ι, Subalgebra.algebraMap_mem _ _⟩ }
+  have : iSup K = s := le_antisymm
+    (iSup_le fun i ↦ le_iSup (fun i ↦ (K i : Set A)) i) (Set.iUnion_subset fun _ ↦ le_iSup K _)
+  this.symm ▸ rfl
+#align subalgebra.coe_supr_of_directed Subalgebra.coe_iSup_of_directed
+
+variable (K)
+variable (f : ∀ i, K i →ₐ[R] B) (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h))
+  (T : Subalgebra R A) (hT : T = iSup K)
+
+-- Porting note (#11215): TODO: turn `hT` into an assumption `T ≤ iSup K`.
+-- That's what `Set.iUnionLift` needs
+-- Porting note: the proofs of `map_{zero,one,add,mul}` got a bit uglier, probably unification trbls
+/-- Define an algebra homomorphism on a directed supremum of subalgebras by defining
+it on each subalgebra, and proving that it agrees on the intersection of subalgebras. -/
+noncomputable def iSupLift : ↥T →ₐ[R] B :=
+  { toFun := Set.iUnionLift (fun i => ↑(K i)) (fun i x => f i x)
+        (fun i j x hxi hxj => by
+          let ⟨k, hik, hjk⟩ := dir i j
+          dsimp
+          rw [hf i k hik, hf j k hjk]
+          rfl)
+        T (by rw [hT, coe_iSup_of_directed dir])
+    map_one' := by apply Set.iUnionLift_const _ (fun _ => 1) <;> simp
+    map_zero' := by dsimp; apply Set.iUnionLift_const _ (fun _ => 0) <;> simp
+    map_mul' := by
+      subst hT; dsimp
+      apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
+      on_goal 3 => rw [coe_iSup_of_directed dir]
+      all_goals simp
+    map_add' := by
+      subst hT; dsimp
+      apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
+      on_goal 3 => rw [coe_iSup_of_directed dir]
+      all_goals simp
+    commutes' := fun r => by
+      dsimp
+      apply Set.iUnionLift_const _ (fun _ => algebraMap R _ r) <;> simp }
+#align subalgebra.supr_lift Subalgebra.iSupLift
+
+variable {K dir f hf T hT}
+
+@[simp]
+theorem iSupLift_inclusion {i : ι} (x : K i) (h : K i ≤ T) :
+    iSupLift K dir f hf T hT (inclusion h x) = f i x := by
+  dsimp [iSupLift, inclusion]
+  rw [Set.iUnionLift_inclusion]
+#align subalgebra.supr_lift_inclusion Subalgebra.iSupLift_inclusion
+
+@[simp]
+theorem iSupLift_comp_inclusion {i : ι} (h : K i ≤ T) :
+    (iSupLift K dir f hf T hT).comp (inclusion h) = f i := by ext; simp
+#align subalgebra.supr_lift_comp_inclusion Subalgebra.iSupLift_comp_inclusion
+
+@[simp]
+theorem iSupLift_mk {i : ι} (x : K i) (hx : (x : A) ∈ T) :
+    iSupLift K dir f hf T hT ⟨x, hx⟩ = f i x := by
+  dsimp [iSupLift, inclusion]
+  rw [Set.iUnionLift_mk]
+#align subalgebra.supr_lift_mk Subalgebra.iSupLift_mk
+
+theorem iSupLift_of_mem {i : ι} (x : T) (hx : (x : A) ∈ K i) :
+    iSupLift K dir f hf T hT x = f i ⟨x, hx⟩ := by
+  dsimp [iSupLift, inclusion]
+  rw [Set.iUnionLift_of_mem]
+#align subalgebra.supr_lift_of_mem Subalgebra.iSupLift_of_mem
+
+end Subalgebra