Skip to content

Commit b02f79a

Browse files
RaggedRRaggedR
committed
refactor: inline comul/counit AlgHom defs, fix where style, add toLinearMap lemmas
Address review feedback: - Remove comulAdditiveAlgHom/counitAdditiveAlgHom as standalone defs, inline aeval expressions directly in the Coalgebra instance - Use where style for instCoalgebra instead of { ... with } - Add Algebra.TensorProduct.toLinearMap_includeRight/Left as rfl lemmas in TensorProduct/Basic.lean, replacing the reversed mk_one_eq lemmas - State simp lemmas in terms of Coalgebra.comul/counit after the instance
1 parent 660d6b3 commit b02f79a

2 files changed

Lines changed: 88 additions & 121 deletions

File tree

‎Mathlib/RingTheory/HopfAlgebra/Polynomial.lean‎

Lines changed: 82 additions & 121 deletions
Original file line numberDiff line numberDiff line change
@@ -56,139 +56,99 @@ namespace Polynomial
5656

5757
variable (R : Type*) [CommSemiring R]
5858

59-
/-! ### Comultiplication and counit -/
60-
61-
/-- The comultiplication on `R[X]` for the additive group scheme `𝔾ₐ`:
62-
the unique `R`-algebra homomorphism sending `X ↦ X ⊗ 1 + 1 ⊗ X`.
63-
As a linear map, this encodes `Δ(p(x)) = p(x + x')`. -/
64-
def comulAdditiveAlgHom : R[X] →ₐ[R] R[X] ⊗[R] R[X] :=
65-
Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))
66-
67-
/-- The counit on `R[X]` for the additive group scheme `𝔾ₐ`:
68-
evaluation at `0`, as an `R`-algebra homomorphism. This is `ε(p) = p(0)`. -/
69-
def counitAdditiveAlgHom : R[X] →ₐ[R] R :=
70-
Polynomial.aeval (0 : R)
71-
72-
@[simp]
73-
theorem comulAdditiveAlgHom_X :
74-
comulAdditiveAlgHom R (X : R[X]) = (X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]) := by
75-
simp [comulAdditiveAlgHom]
76-
77-
@[simp]
78-
theorem comulAdditiveAlgHom_C (r : R) :
79-
comulAdditiveAlgHom R (C r) = (C r) ⊗ₜ 1 := by
80-
simp [comulAdditiveAlgHom]
81-
82-
@[simp]
83-
theorem counitAdditiveAlgHom_X :
84-
counitAdditiveAlgHom R (X : R[X]) = 0 := by
85-
simp [counitAdditiveAlgHom]
86-
87-
@[simp]
88-
theorem counitAdditiveAlgHom_C (r : R) :
89-
counitAdditiveAlgHom R (C r) = r := by
90-
simp [counitAdditiveAlgHom]
91-
9259
/-! ### Coalgebra instance
9360
9461
The three coalgebra axioms (coassociativity, left counitality, right counitality)
9562
reduce to checking equality of `R`-algebra hom compositions on the generator `X`.
9663
-/
9764

98-
/-- The `𝔾ₐ` coalgebra structure on `R[X]`. -/
99-
instance instCoalgebraStruct : CoalgebraStruct R R[X] where
100-
comul := (comulAdditiveAlgHom R).toLinearMap
101-
counit := (counitAdditiveAlgHom R).toLinearMap
102-
103-
-- Auxiliary equations for unfolding the CoalgebraStruct fields
104-
theorem comul_eq : (CoalgebraStruct.comul : R[X] →ₗ[R] _) =
105-
(comulAdditiveAlgHom R).toLinearMap := rfl
106-
107-
theorem counit_eq : (CoalgebraStruct.counit : R[X] →ₗ[R] _) =
108-
(counitAdditiveAlgHom R).toLinearMap := rfl
109-
110-
-- Glue lemmas connecting rTensor/lTensor to Algebra.TensorProduct.map
111-
theorem rTensor_counit_eq :
112-
(counitAdditiveAlgHom R).toLinearMap.rTensor R[X] =
113-
(Algebra.TensorProduct.map (counitAdditiveAlgHom R)
114-
(AlgHom.id R R[X])).toLinearMap := by
65+
-- Glue lemmas connecting rTensor/lTensor of AlgHom.toLinearMap to Algebra.TensorProduct.map
66+
private theorem rTensor_toLinearMap_eq (f : R[X] →ₐ[R] A) :
67+
f.toLinearMap.rTensor R[X] =
68+
(Algebra.TensorProduct.map f (AlgHom.id R R[X])).toLinearMap := by
11569
ext x y; simp [LinearMap.rTensor_tmul]
11670

117-
theorem lTensor_counit_eq :
118-
(counitAdditiveAlgHom R).toLinearMap.lTensor R[X] =
119-
(Algebra.TensorProduct.map (AlgHom.id R R[X])
120-
(counitAdditiveAlgHom R)).toLinearMap := by
71+
private theorem lTensor_toLinearMap_eq (f : R[X] →ₐ[R] A) :
72+
f.toLinearMap.lTensor R[X] =
73+
(Algebra.TensorProduct.map (AlgHom.id R R[X]) f).toLinearMap := by
12174
ext x y; simp [LinearMap.lTensor_tmul]
12275

123-
theorem mk_one_eq_includeRight :
124-
TensorProduct.mk R R R[X] 1 =
125-
(Algebra.TensorProduct.includeRight : R[X] →ₐ[R] R ⊗[R] R[X]).toLinearMap := by
126-
ext y; simp [Algebra.TensorProduct.includeRight_apply]
76+
/-- The `𝔾ₐ` coalgebra instance on `R[X]`: coassociativity holds because both
77+
`(Δ ⊗ id) ∘ Δ` and `(id ⊗ Δ) ∘ Δ` send `X` to `X⊗1⊗1 + 1⊗X⊗1 + 1⊗1⊗X`. -/
78+
instance instCoalgebra : Coalgebra R R[X] where
79+
comul := (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))).toLinearMap
80+
counit := (Polynomial.aeval (0 : R)).toLinearMap
81+
rTensor_counit_comp_comul := by
82+
rw [rTensor_toLinearMap_eq, Algebra.TensorProduct.toLinearMap_includeRight]
83+
change ((Algebra.TensorProduct.map (Polynomial.aeval (0 : R))
84+
(AlgHom.id R R[X])).comp
85+
(Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))).toLinearMap = _
86+
congr 1
87+
apply Polynomial.algHom_ext
88+
simp [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeRight_apply]
89+
lTensor_counit_comp_comul := by
90+
rw [lTensor_toLinearMap_eq, Algebra.TensorProduct.toLinearMap_includeLeft]
91+
change ((Algebra.TensorProduct.map (AlgHom.id R R[X])
92+
(Polynomial.aeval (0 : R))).comp
93+
(Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))).toLinearMap = _
94+
congr 1
95+
apply Polynomial.algHom_ext
96+
simp [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeLeft_apply]
97+
coassoc := by
98+
rw [rTensor_toLinearMap_eq, lTensor_toLinearMap_eq]
99+
change ((Algebra.TensorProduct.assoc R R R R[X] R[X] R[X]).toAlgHom.comp
100+
((Algebra.TensorProduct.map
101+
(Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))
102+
(AlgHom.id R R[X])).comp
103+
(Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))))).toLinearMap =
104+
((Algebra.TensorProduct.map (AlgHom.id R R[X])
105+
(Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))).comp
106+
(Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))).toLinearMap
107+
congr 1
108+
apply Polynomial.algHom_ext
109+
simp only [AlgHom.comp_apply, AlgEquiv.toAlgHom_eq_coe,
110+
AlgHom.coe_coe, Algebra.TensorProduct.map_tmul, AlgHom.id_apply, aeval_X,
111+
map_add, map_one, Algebra.TensorProduct.one_def,
112+
Algebra.TensorProduct.assoc_tmul,
113+
TensorProduct.add_tmul, TensorProduct.tmul_add]
114+
abel
127115

128-
theorem mk_flip_one_eq_includeLeft :
129-
(TensorProduct.mk R R[X] R).flip 1 =
130-
(Algebra.TensorProduct.includeLeft : R[X] →ₐ[R] R[X] ⊗[R] R).toLinearMap := by
131-
ext y; simp [Algebra.TensorProduct.includeLeft_apply, LinearMap.flip_apply]
116+
@[simp]
117+
theorem comul_X :
118+
Coalgebra.comul (R := R) (X : R[X]) = (X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]) := by
119+
change (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))) X = _
120+
simp
132121

133-
theorem rTensor_comul_eq :
134-
(comulAdditiveAlgHom R).toLinearMap.rTensor R[X] =
135-
(Algebra.TensorProduct.map (comulAdditiveAlgHom R)
136-
(AlgHom.id R R[X])).toLinearMap := by
137-
ext x y; simp [LinearMap.rTensor_tmul]
122+
@[simp]
123+
theorem comul_C (r : R) :
124+
Coalgebra.comul (R := R) (C r : R[X]) = (C r) ⊗ₜ 1 := by
125+
change (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))) (C r) = _
126+
simp
138127

139-
theorem lTensor_comul_eq :
140-
(comulAdditiveAlgHom R).toLinearMap.lTensor R[X] =
141-
(Algebra.TensorProduct.map (AlgHom.id R R[X])
142-
(comulAdditiveAlgHom R)).toLinearMap := by
143-
ext x y; simp [LinearMap.lTensor_tmul]
128+
@[simp]
129+
theorem counit_X :
130+
Coalgebra.counit (R := R) (X : R[X]) = 0 := by
131+
change (Polynomial.aeval (0 : R)) X = _
132+
simp
144133

145-
/-- The `𝔾ₐ` coalgebra instance on `R[X]`: coassociativity holds because both
146-
`(Δ ⊗ id) ∘ Δ` and `(id ⊗ Δ) ∘ Δ` send `X` to `X⊗1⊗1 + 1⊗X⊗1 + 1⊗1⊗X`. -/
147-
instance instCoalgebra : Coalgebra R R[X] :=
148-
{ instCoalgebraStruct R with
149-
rTensor_counit_comp_comul := by
150-
rw [counit_eq, comul_eq, rTensor_counit_eq, mk_one_eq_includeRight]
151-
change ((Algebra.TensorProduct.map (counitAdditiveAlgHom R)
152-
(AlgHom.id R R[X])).comp (comulAdditiveAlgHom R)).toLinearMap = _
153-
congr 1
154-
apply Polynomial.algHom_ext
155-
simp [comulAdditiveAlgHom, counitAdditiveAlgHom,
156-
Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeRight_apply]
157-
lTensor_counit_comp_comul := by
158-
rw [counit_eq, comul_eq, lTensor_counit_eq, mk_flip_one_eq_includeLeft]
159-
change ((Algebra.TensorProduct.map (AlgHom.id R R[X])
160-
(counitAdditiveAlgHom R)).comp (comulAdditiveAlgHom R)).toLinearMap = _
161-
congr 1
162-
apply Polynomial.algHom_ext
163-
simp [comulAdditiveAlgHom, counitAdditiveAlgHom,
164-
Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeLeft_apply]
165-
coassoc := by
166-
rw [comul_eq, rTensor_comul_eq, lTensor_comul_eq]
167-
change ((Algebra.TensorProduct.assoc R R R R[X] R[X] R[X]).toAlgHom.comp
168-
((Algebra.TensorProduct.map (comulAdditiveAlgHom R)
169-
(AlgHom.id R R[X])).comp
170-
(comulAdditiveAlgHom R))).toLinearMap =
171-
((Algebra.TensorProduct.map (AlgHom.id R R[X])
172-
(comulAdditiveAlgHom R)).comp
173-
(comulAdditiveAlgHom R)).toLinearMap
174-
congr 1
175-
apply Polynomial.algHom_ext
176-
simp only [comulAdditiveAlgHom, AlgHom.comp_apply,
177-
Algebra.TensorProduct.map_tmul, AlgHom.id_apply, aeval_X,
178-
map_add, map_one, Algebra.TensorProduct.one_def,
179-
TensorProduct.add_tmul, TensorProduct.tmul_add]
180-
abel }
134+
@[simp]
135+
theorem counit_C (r : R) :
136+
Coalgebra.counit (R := R) (C r : R[X]) = r := by
137+
change (Polynomial.aeval (0 : R)) (C r) = _
138+
simp
181139

182140
/-! ### Bialgebra instance -/
183141

184142
/-- The `𝔾ₐ` bialgebra instance on `R[X]`: the comultiplication and counit are algebra
185143
homomorphisms by construction. -/
186144
instance instBialgebra : Bialgebra R R[X] :=
187145
Bialgebra.mk' R R[X]
188-
(by simp [counit_eq])
189-
(by intro a b; simp [counit_eq, map_mul])
190-
(by simp [comul_eq])
191-
(by intro a b; simp [comul_eq, map_mul])
146+
(by change (Polynomial.aeval (0 : R)) 1 = 1; simp)
147+
(fun {a b} => by change (Polynomial.aeval (0 : R)) (a * b) = _; simp [map_mul])
148+
(by change (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))) 1 = 1; simp)
149+
(fun {a b} => by
150+
change (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))) (a * b) = _
151+
simp [map_mul])
192152

193153
end Polynomial
194154

@@ -233,28 +193,29 @@ instance instHopfAlgebra : HopfAlgebra R R[X] where
233193
(Algebra.TensorProduct.map (antipodeAdditiveAlgHom R)
234194
(AlgHom.id R R[X])).toLinearMap := by
235195
ext x y; simp [LinearMap.rTensor_tmul]
236-
rw [comul_eq, counit_eq, rTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
237-
-- Both sides are toLinearMap of algebra hom compositions. Convert and check on X.
196+
rw [rTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
238197
change ((Algebra.TensorProduct.lmul' R : R[X] ⊗[R] R[X] →ₐ[R] R[X]).comp
239198
((Algebra.TensorProduct.map (antipodeAdditiveAlgHom R)
240-
(AlgHom.id R R[X])).comp (comulAdditiveAlgHom R))).toLinearMap =
241-
((Algebra.ofId R R[X]).comp (counitAdditiveAlgHom R)).toLinearMap
199+
(AlgHom.id R R[X])).comp
200+
(Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))))).toLinearMap =
201+
((Algebra.ofId R R[X]).comp (Polynomial.aeval (0 : R))).toLinearMap
242202
congr 1; apply Polynomial.algHom_ext
243-
simp [comulAdditiveAlgHom, antipodeAdditiveAlgHom, counitAdditiveAlgHom,
203+
simp [antipodeAdditiveAlgHom,
244204
Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lmul'_apply_tmul,
245205
Algebra.ofId_apply]
246206
mul_antipode_lTensor_comul := by
247207
have lTensor_eq : (antipodeAdditiveAlgHom R).toLinearMap.lTensor R[X] =
248208
(Algebra.TensorProduct.map (AlgHom.id R R[X])
249209
(antipodeAdditiveAlgHom R)).toLinearMap := by
250210
ext x y; simp [LinearMap.lTensor_tmul]
251-
rw [comul_eq, counit_eq, lTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
211+
rw [lTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
252212
change ((Algebra.TensorProduct.lmul' R : R[X] ⊗[R] R[X] →ₐ[R] R[X]).comp
253213
((Algebra.TensorProduct.map (AlgHom.id R R[X])
254-
(antipodeAdditiveAlgHom R)).comp (comulAdditiveAlgHom R))).toLinearMap =
255-
((Algebra.ofId R R[X]).comp (counitAdditiveAlgHom R)).toLinearMap
214+
(antipodeAdditiveAlgHom R)).comp
215+
(Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))))).toLinearMap =
216+
((Algebra.ofId R R[X]).comp (Polynomial.aeval (0 : R))).toLinearMap
256217
congr 1; apply Polynomial.algHom_ext
257-
simp [comulAdditiveAlgHom, antipodeAdditiveAlgHom, counitAdditiveAlgHom,
218+
simp [antipodeAdditiveAlgHom,
258219
Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lmul'_apply_tmul,
259220
Algebra.ofId_apply]
260221

‎Mathlib/RingTheory/TensorProduct/Basic.lean‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -317,6 +317,9 @@ theorem includeLeft_apply [SMulCommClass R S A] (a : A) :
317317
(includeLeft : A →ₐ[S] A ⊗[R] B) a = a ⊗ₜ 1 :=
318318
rfl
319319

320+
theorem toLinearMap_includeLeft [SMulCommClass R S A] :
321+
(includeLeft : A →ₐ[S] A ⊗[R] B).toLinearMap = (TensorProduct.mk R A B).flip 1 := rfl
322+
320323
/-- The algebra morphism `B →ₐ[R] A ⊗[R] B` sending `b` to `1 ⊗ₜ b`. -/
321324
def includeRight : B →ₐ[R] A ⊗[R] B where
322325
toFun b := 1 ⊗ₜ b
@@ -330,6 +333,9 @@ def includeRight : B →ₐ[R] A ⊗[R] B where
330333
theorem includeRight_apply (b : B) : (includeRight : B →ₐ[R] A ⊗[R] B) b = 1 ⊗ₜ b :=
331334
rfl
332335

336+
theorem toLinearMap_includeRight :
337+
(includeRight : B →ₐ[R] A ⊗[R] B).toLinearMap = TensorProduct.mk R A B 1 := rfl
338+
333339
theorem includeLeftRingHom_comp_algebraMap :
334340
(includeLeftRingHom.comp (algebraMap R A) : R →+* A ⊗[R] B) =
335341
includeRight.toRingHom.comp (algebraMap R B) := by

0 commit comments

Comments
 (0)