FiniteTensorQuotient.lean

1 import Mathlib.RingTheory.PiTensorProduct
2 import Mathlib.RingTheory.Ideal.Quotient.Operations
3 import Mathlib.RingTheory.Ideal.Maps
4 
5 /-! Actual finite algebra tensor products and simultaneous ideal quotients. -/
6 noncomputable section
7 open Function
8 set_option autoImplicit false
9 namespace PaperXII.FiniteTensor
10 
11 variable {O ι : Type*} [CommRing O] [Fintype ι] [DecidableEq ι]
12 variable (R : ι → Type*) [∀ i, CommRing (R i)] [∀ i, Algebra O (R i)]
13 
14 abbrev Raw := PiTensorProduct O R
15 
16 /-- The canonical inclusion of one factor in the actual finite tensor product. -/
17 def includeFactor (i : ι) : R i →ₐ[O] Raw (O := O) R := PiTensorProduct.singleAlgHom i
18 
19 /-- The universal algebra map, constructed by the multilinear product of the factor maps. -/
20 def liftFamily {A : Type*} [CommRing A] [Algebra O A] (f : ∀ i, R i →ₐ[O] A) :
21     Raw (O := O) R →ₐ[O] A :=
22   PiTensorProduct.liftAlgHom
23     ((MultilinearMap.mkPiAlgebra O ι A).compLinearMap (fun i ↦ (f i).toLinearMap))
24     (by simp [MultilinearMap.compLinearMap_apply, MultilinearMap.mkPiAlgebra_apply])
25     (by intro x y; simp [MultilinearMap.compLinearMap_apply, MultilinearMap.mkPiAlgebra_apply,
26       Pi.mul_apply, Finset.prod_mul_distrib])
27 
28 omit [DecidableEq ι] in
29 @[simp] theorem liftFamily_tprod {A : Type*} [CommRing A] [Algebra O A]
30     (f : ∀ i, R i →ₐ[O] A) (x : ∀ i, R i) :
31     liftFamily R f (PiTensorProduct.tprod O x) = ∏ i, f i (x i) := by
32   change PiTensorProduct.lift _ (PiTensorProduct.tprod O x) = _
33   rw [PiTensorProduct.lift.tprod]
34   rfl
35 
36 @[simp] theorem liftFamily_include {A : Type*} [CommRing A] [Algebra O A]
37     (f : ∀ i, R i →ₐ[O] A) (i : ι) (x : R i) :
38     liftFamily R f (includeFactor R i x) = f i x := by
39   change liftFamily R f (PiTensorProduct.tprod O (Pi.mulSingle i x)) = _
40   rw [liftFamily_tprod]
41   have h : (fun j ↦ f j (Pi.mulSingle i x j)) = Pi.mulSingle i (f i x) := by
42     funext j
43     by_cases hj : j = i
44     · subst j; simp
45     · simp [Pi.mulSingle, Function.update_of_ne hj]
46   rw [h]
47   simp
48 
49 @[simp] theorem liftFamily_comp_include {A : Type*} [CommRing A] [Algebra O A]
50     (f : ∀ i, R i →ₐ[O] A) (i : ι) :
51     (liftFamily R f).comp (includeFactor R i) = f i := by ext x; simp
52 
53 /-- Uniqueness is proved using the actual finite tensor product's extensionality theorem. -/
54 theorem hom_ext {A : Type*} [CommRing A] [Algebra O A]
55     {f g : Raw (O := O) R →ₐ[O] A}
56     (h : ∀ i, f.comp (includeFactor R i) = g.comp (includeFactor R i)) : f = g :=
57   PiTensorProduct.algHom_ext h
58 
59 /-- The literal algebraic ideal generated by all local conditions. -/
60 def conditions (J : ∀ i, Ideal (R i)) : Ideal (Raw (O := O) R) :=
61   ⨆ i, (J i).map (includeFactor R i).toRingHom
62 
63 /-- The defining ideal also retains the base ideal, necessary for the empty family. -/
64 def definingIdeal (mO : Ideal O) (m : ∀ i, Ideal (R i)) : Ideal (Raw (O := O) R) :=
65   mO.map (algebraMap O (Raw (O := O) R)) ⊔ conditions R m
66 
67 variable (J : ∀ i, Ideal (R i))
68 
69 /-- Apply the actual quotient map in every factor. -/
70 def quotientMap : Raw (O := O) R →ₐ[O] Raw (O := O) (fun i ↦ R i ⧸ J i) :=
71   liftFamily R (fun i ↦ (includeFactor (fun i ↦ R i ⧸ J i) i).comp (Ideal.Quotient.mkₐ O (J i)))
72 
73 @[simp] theorem quotientMap_include (i : ι) (x : R i) :
74     quotientMap (O := O) R J (includeFactor R i x) =
75       includeFactor (fun i ↦ R i ⧸ J i) i (Ideal.Quotient.mk (J i) x) := by
76   simp [quotientMap]
77 
78 /-- Each source condition vanishes in the actual tensor of quotients. -/
79 theorem conditions_le_ker : conditions (O := O) R J ≤ RingHom.ker (quotientMap (O := O) R J) := by
80   rw [conditions, iSup_le_iff]
81   intro i
82   rw [Ideal.map_le_iff_le_comap]
83   intro x hx
84   change quotientMap (O := O) R J (includeFactor R i x) = 0
85   rw [quotientMap_include, Ideal.Quotient.eq_zero_iff_mem.mpr hx, map_zero]
86 
87 def quotientForward : (Raw (O := O) R ⧸ conditions (O := O) R J) →ₐ[O]
88     Raw (O := O) (fun i ↦ R i ⧸ J i) :=
89   Ideal.Quotient.liftₐ _ (quotientMap (O := O) R J) (conditions_le_ker R J)
90 
91 def factorQuotient (i : ι) : (R i ⧸ J i) →ₐ[O] (Raw (O := O) R ⧸ conditions (O := O) R J) :=
92   Ideal.Quotient.liftₐ (J i) ((Ideal.Quotient.mkₐ O (conditions (O := O) R J)).comp (includeFactor R i))
93     (by
94       intro x hx
95       apply Ideal.Quotient.eq_zero_iff_mem.mpr
96       exact (le_iSup (fun i ↦ (J i).map (includeFactor R i).toRingHom) i)
97         (Ideal.mem_map_of_mem _ hx))
98 
99 omit [Fintype ι] in
100 @[simp] theorem factorQuotient_mk (i : ι) (x : R i) :
101     factorQuotient (O := O) R J i (Ideal.Quotient.mk (J i) x) =
102       Ideal.Quotient.mk (conditions (O := O) R J) (includeFactor R i x) := rfl
103 
104 def quotientBackward : Raw (O := O) (fun i ↦ R i ⧸ J i) →ₐ[O]
105     (Raw (O := O) R ⧸ conditions (O := O) R J) :=
106   liftFamily _ (factorQuotient (O := O) R J)
107 
108 @[simp] theorem quotientForward_mk (x : Raw (O := O) R) :
109     quotientForward (O := O) R J (Ideal.Quotient.mk _ x) = quotientMap (O := O) R J x := rfl
110 
111 @[simp] theorem quotientBackward_include (i : ι) (x : R i ⧸ J i) :
112     quotientBackward (O := O) R J (includeFactor (fun i ↦ R i ⧸ J i) i x) = factorQuotient (O := O) R J i x := by
113   simp [quotientBackward]
114 
115 theorem quotientForward_backward :
116     (quotientForward (O := O) R J).comp (quotientBackward (O := O) R J) = AlgHom.id O _ := by
117   apply hom_ext
118   intro i
119   ext x
120   obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
121   simp
122 
123 theorem quotientBackward_forward :
124     (quotientBackward (O := O) R J).comp (quotientForward (O := O) R J) = AlgHom.id O _ := by
125   apply Ideal.Quotient.algHom_ext
126   apply hom_ext
127   intro i
128   ext x
129   simp
130 
131 /-- Finite simultaneous tensor quotient, at the algebraic level. -/
132 def quotientEquiv : (Raw (O := O) R ⧸ conditions (O := O) R J) ≃ₐ[O]
133     Raw (O := O) (fun i ↦ R i ⧸ J i) :=
134   AlgEquiv.ofAlgHom (quotientForward (O := O) R J) (quotientBackward (O := O) R J)
135     (quotientForward_backward R J) (quotientBackward_forward R J)
136 
137 @[simp] theorem quotientEquiv_mk (x : Raw (O := O) R) :
138     quotientEquiv (O := O) R J (Ideal.Quotient.mk _ x) = quotientMap (O := O) R J x := rfl
139 
140 /-- The tensor-of-quotients map is an actual surjection. -/
141 theorem quotientMap_surjective : Function.Surjective (quotientMap (O := O) R J) := by
142   intro y
143   obtain ⟨x, hx⟩ := (quotientEquiv (O := O) R J).surjective y
144   obtain ⟨z, rfl⟩ := Ideal.Quotient.mk_surjective x
145   exact ⟨z, hx⟩
146 
147 /-- Applying a coefficient quotient maps the topological defining ideal exactly. -/
148 theorem quotientMap_definingIdeal (mO : Ideal O) (m : ∀ i, Ideal (R i)) :
149     (definingIdeal R mO m).map (quotientMap (O := O) R J).toRingHom =
150       definingIdeal (fun i ↦ R i ⧸ J i) mO
151         (fun i ↦ (m i).map (Ideal.Quotient.mk (J i))) := by
152   simp only [definingIdeal, conditions, Ideal.map_sup, Ideal.map_iSup, Ideal.map_map]
153   congr 1
154   · congr 1
155     ext r
156     exact (quotientMap (O := O) R J).commutes r
157   · apply congrArg iSup
158     funext i
159     congr 1
160     ext x
161     exact quotientMap_include R J i x
162 
163 /-- The algebra equivalence carries the quotient's defining ideal to the actual target ideal. -/
164 theorem quotientEquiv_definingIdeal (mO : Ideal O) (m : ∀ i, Ideal (R i)) :
165     ((definingIdeal R mO m).map (Ideal.Quotient.mk (conditions (O := O) R J))).map
166       (quotientEquiv (O := O) R J).toRingEquiv.toRingHom =
167       definingIdeal (fun i ↦ R i ⧸ J i) mO
168         (fun i ↦ (m i).map (Ideal.Quotient.mk (J i))) := by
169   rw [Ideal.map_map]
170   exact quotientMap_definingIdeal R J mO m
171 
172 end PaperXII.FiniteTensor

Back to source controls