diff --git a/FLT/GlobalLanglandsConjectures/02061227_Proj2.lean b/FLT/GlobalLanglandsConjectures/02061227_Proj2.lean deleted file mode 100644 index 73b60cf4..00000000 --- a/FLT/GlobalLanglandsConjectures/02061227_Proj2.lean +++ /dev/null @@ -1,1179 +0,0 @@ -import Mathlib.Tactic -import Mathlib.RingTheory.TensorProduct -import Mathlib.RingTheory.HopfAlgebra -open Function -open scoped TensorProduct -set_option maxHeartbeats 5000000 -set_option linter.unusedVariables false -/-! -# Algebra and Linear Homomorphisms of Bialgebras, Coalgebras and Algebras -The first part of this files provides proofs of all the Algebra homomorphism from a -R-Bialgebra A to a Commutative R-Algebra L (defined as Points R A L) forms a monoid with the binary -operation "*" defined by convolution product and "one" defined by the composition of unit of L and -counit of A ((Algebra.ofId R L).comp (Bialgebra.counitAlgHom R A)), while the second part proves -that all the linear homomorphisms from a R-Coalgebra C to a R-Algebra B also forms a monoid by -the linear convolution product and the identity "linone" defined by (one _ _ _).toLinearMap. - -# Proof of TensorProduct of two R-Bialgebras (A1 and A2) are R-Bialgebras -The third part of this file is a preparation of the proof of the Antipode of a Hopf R-Algebra is -indeed an antihomomorphism (namely S(ab) = S(b)*S(a)), to do that we defined α β: H ⊗[R] H →ₗ H -to be α : (a ⊗ b) ↦ S(ab) and β : (a ⊗ b) ↦ S(b)*S(a). But for that to work we need the fact that -H ⊗ H is a Bialgebra and we genralized it to the Bialgebra case (In fact, C ⊗ C is a Coalgebra -for C being R-Coalgebra but we kind of include that in our proof of Bialgebra). - -# Proof of all Algebra Homomorphism from a Commutative Hopf Algebra to a R-Algebra forms a Group -The fourth part of the part proves that (Points R H L) is a group that inherits multiplication -and identity elements from the monoid structure proved in Part I with inverse given by f⁻¹ = -(S ∘ f). And to do that we need antipode is an antihomomorphism (hence under the condition of -commutativity, we have that the antipode is an Algebra Homomorphism), and we did that by showing -α * m = linone and m * β = linone where m is the multiplication of H. Therefore α = α * linone -= α * (m * β) = (α * m) * β = linone * β = β showing that the anipode S is indeed an -antihomomorphism in H, then everythings follows (proving the group axioms, etc.) - -# Finishing the TO-DO list in Hopf Algebra Files -At the end of this file (some are proved within the previous parts), we proved that S² = id and S -is a Bijection when H is Commutative (the case where H is Co-Commutative is unproved yet) and the -proof of the uniqueness of antipode is in the proof of LinPoints forms a monoid named as -anti_unique. - -## Main declarations -- `Points.Points R A L` is all the R-Algebra Homomorphisms A →ₐ[R] L -- `Points.Pointmul_assoc` is the associativity of R-Algebra Homomorphisms in `Points R A L` under - convolution product "*". -- `HopfPoints.LinPoints R C B` is all the R-Linear Maps C →ₗ[R] B where C is R-Coalgbra - and B is R-Algebra -- `HopfPoints.mul_id_val`: id_H * S = linone under linear convolution product -- `HopfPoints.id_mul_val`: S * id_H = linone under linear convolution product -- `HopfPoints.UniquenessAnti` : Any T : H →ₗ H, if T * id_H = id_H * T = linone, then - T = antipode (uniqueness of antipode). -- `HopfPoints.comul_repr` is the seedler notation for comultiplication for R-Coalgebras, that is - ∀ x ∈ C, comul x can be expressed as ∑ i in I, x1 i ⊗ x2 i -- `HopfPoints.αmul_eqone`: α * m = linone -- `HopfPoints.mulβ_eqone`: m * β = linone -- `HopfPoints.antihom` : S(ab) = S(b) * S(a) -- `HopfPoints.antipodemul` : Under a Commutative Hopf Algebra H, S(ab) = S(a) * S(b) -- `HopfPoints.S2isid` : S² = id_H -- `HopfPoints.bijectiveAntipode` : S is bijection. - -## References -* -* Christian Kassel "Quantum Groups" (Springer GTM), around Prop III.3.1, Theorem III.3.4 etc. -* Dr.Adrian de Jesus Celestino Rodriguez "Cumulants in Non-commutative Probability via Hopf - Algebras", 2022 --/ -variable (R : Type)[CommRing R] -variable (A : Type)[Ring A][Bialgebra R A] -variable (L : Type)[CommRing L][Algebra R L] - -variable {ψ φ ρ : A →ₐ[R] L} --- Goal of the First Part is to Prove Points R A L is a monoid -namespace Points --- Define Points to be all the algebra homomorphisms from a R-Bialgebra A to a --- Commutative R-Algebra L -def Points := A →ₐ[R] L -noncomputable section -variable {R A L}{x : A} -instance : Coalgebra R A := by infer_instance --- Define the multiplication for Points to be convolution product -def mul (ψ φ : Points R A L) : Points R A L := - (Algebra.TensorProduct.lmul' (S := L) R).comp - ((Algebra.TensorProduct.map ψ φ).comp (Bialgebra.comulAlgHom R A)) - -lemma mul1(ψ φ : Points R A L) : mul ψ φ = - (Algebra.TensorProduct.lmul' (S := L) R).comp - ((Algebra.TensorProduct.map ψ φ).comp (Bialgebra.comulAlgHom R A)) := by rfl -variable {a b c : A} - -instance : Mul (Points R A L) := ⟨mul⟩ -instance : HMul (Points R A L) (Points R A L) (Points R A L) := ⟨mul⟩ - -lemma hmul1(ψ φ : Points R A L) : ψ * φ = - (Algebra.TensorProduct.lmul' (S := L) R).comp - ((Algebra.TensorProduct.map ψ φ).comp (Bialgebra.comulAlgHom R A)) := by rfl - --- The identity element in this monoid is unit comp counit which maps from --- A -> R -> L -def one : Points R A L := - (Algebra.ofId R L).comp - (Bialgebra.counitAlgHom R A) -- counit and then map from R to L - -lemma oneval: one = (Algebra.ofId R L).comp - (Bialgebra.counitAlgHom R A) := by rfl - -instance : One (Points R A L) := ⟨one⟩ - --- The purpose of these two instances are to prove the 'ext' lemma for elements --- in Points such that we could use the 'ext' tactic -instance : FunLike (Points R A L) A L := by unfold Points; infer_instance - -instance : AlgHomClass (Points R A L) R A L := by - unfold Points - infer_instance - -@[ext] -lemma Pointext (ψ φ : Points R A L) (hx : ∀ x, ψ x = φ x): ψ = φ := - AlgHom.ext hx --- 3 commutative R-algeberas A,B,C --- two maps A ⊗ B -> C, R-algebra maps --- if they're equal on all elements of the form a ⊗ₜ b --- then they're equal - -@[ext] -lemma AlgTensorExt (A1 A2 B : Type)[Ring B][Ring A2][Ring A1][Algebra R A1][Algebra R A2] - [Algebra R B](F : A1 ⊗[R] A2 →ₐ[R] B) - (G : A1 ⊗[R] A2 →ₐ[R] B) (h : ∀ a b, F (a ⊗ₜ b) = G (a ⊗ₜ b)) : F = G := by - ext x <;> simp [h] - --- Breaking down the commutative diagram into small parts : this lemma shows that --- (ψ * φ) ⊗ ρ = (m ⊗ id) ∘ (ψ ⊗ φ) ⊗ ρ ∘ (Δ ⊗ id) where m is the multiplication --- of L and Δ is the comultiplication of A -lemma left_block_comm (ψ φ ρ : Points R A L) : - Algebra.TensorProduct.map (ψ * φ) ρ = (Algebra.TensorProduct.map - (Algebra.TensorProduct.lmul' (S := L) R) (AlgHom.id R L)).comp - ((Algebra.TensorProduct.map (Algebra.TensorProduct.map ψ φ) ρ).comp - (Algebra.TensorProduct.map (Bialgebra.comulAlgHom R A) (AlgHom.id R A))) := by - symm - rw [hmul1 ψ φ] - ext x <;> simp - --- This lemma shows ψ ⊗ (φ * ρ) = (id ⊗ Δ) ∘ ψ ⊗ (φ ⊗ ρ) ∘ (id ⊗ m) -lemma right_block_comm (ψ φ ρ : Points R A L) : - Algebra.TensorProduct.map ψ (φ * ρ) = (Algebra.TensorProduct.map - (AlgHom.id R L) (Algebra.TensorProduct.lmul' (S := L) R)).comp - ((Algebra.TensorProduct.map ψ (Algebra.TensorProduct.map φ ρ)).comp - (Algebra.TensorProduct.map (AlgHom.id R A) (Bialgebra.comulAlgHom R A))) := by - symm ; rw [hmul1 φ ρ] - ext x <;> simp - --- We define maps that idetify the associativity of tensor products of A and L --- respectively (here I should have used abbrev instead of def as kevin has pointed --- out, but when I realized this it's already too many lines :))) -def assoc_a : (A ⊗[R] A) ⊗[R] A →ₐ[R] A ⊗[R] (A ⊗[R] A) := - (Algebra.TensorProduct.assoc R A A A).toAlgHom - -def assoc_l : (L ⊗[R] L) ⊗[R] L →ₐ[R] L ⊗[R] (L ⊗[R] L) := - (Algebra.TensorProduct.assoc R L L L).toAlgHom - --- After decomposing the commutative diagram into small parts, we prove the upper --- half first, which is: (Δ ⊗ id) ∘ Δ = (id ⊗ Δ) ∘ Δ which is the variation of one --- of the axioms of Coalgebra. -lemma Coassoc : assoc_a ((Algebra.TensorProduct.map (Bialgebra.comulAlgHom R A) - (AlgHom.id R A)).comp (Bialgebra.comulAlgHom R A) x) = - (Algebra.TensorProduct.map (AlgHom.id R A) (Bialgebra.comulAlgHom R A)).comp - (Bialgebra.comulAlgHom R A) x := by - repeat rw [AlgHom.comp_apply] - simp_all only [Bialgebra.comulAlgHom_apply] - have h0 := Coalgebra.coassoc_apply (R := R) (A := A) x - change assoc_a ((LinearMap.rTensor A Coalgebra.comul) (Coalgebra.comul x)) = - (LinearMap.lTensor A Coalgebra.comul) (Coalgebra.comul x) at h0 - exact h0 - --- This is the middle part of the commutative diagram that explains the associativity --- of maps which is : (ψ ⊗ φ) ⊗ ρ = ψ ⊗ (φ ⊗ ρ) -lemma Mapassoc' (ψ φ ρ : Points R A L): - assoc_l.comp ((Algebra.TensorProduct.map (Algebra.TensorProduct.map ψ φ) ρ)) - = (Algebra.TensorProduct.map ψ (Algebra.TensorProduct.map φ ρ)).comp assoc_a := by - ext x <;> rfl - --- This is the lemma above applied on elements in A ⊗ A ⊗ A -lemma Mapassoc (ψ φ ρ : Points R A L) (aaa : (A ⊗[R] A) ⊗[R] A): - assoc_l (((Algebra.TensorProduct.map (Algebra.TensorProduct.map ψ φ) ρ)) aaa) - = (Algebra.TensorProduct.map ψ (Algebra.TensorProduct.map φ ρ)) (assoc_a aaa) - := by apply AlgHom.ext_iff.1 (Mapassoc' ψ φ ρ) aaa - -open BigOperators --- This is the lower part of the commutative diagram which is a variation of one --- of the axioms of an Algebra : m ∘ (m ⊗ id) = m ∘ (id ⊗ m) -lemma Al_assoc : (Algebra.TensorProduct.lmul' R).comp ((Algebra.TensorProduct.map - (Algebra.TensorProduct.lmul' R) (AlgHom.id R L))) = - (Algebra.TensorProduct.lmul' R).comp ((Algebra.TensorProduct.map (AlgHom.id R L) - (Algebra.TensorProduct.lmul' R)).comp assoc_l) := by - ext x - · delta assoc_l ; simp - · delta assoc_l ; simp - · delta assoc_l ; simp only [AlgHom.coe_comp, AlgHom.coe_restrictScalars', comp_apply, - Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.map_tmul, map_one, - AlgHom.coe_id, id_eq, Algebra.TensorProduct.lmul'_apply_tmul, one_mul, - AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_coe] - rw [show (1 : L ⊗[R] L) = (1 ⊗ₜ[R] 1) by rfl] - simp - --- The lemma above applied on elements of L ⊗ L ⊗ L -lemma Al_assoc_apply (lll : (L ⊗[R] L) ⊗[R] L) : (Algebra.TensorProduct.lmul' R) - ((Algebra.TensorProduct.map (Algebra.TensorProduct.lmul' R) (AlgHom.id R L)) lll) = - (Algebra.TensorProduct.lmul' R) ((Algebra.TensorProduct.map (AlgHom.id R L) - (Algebra.TensorProduct.lmul' R)) (assoc_l lll)) := by - have := Al_assoc (R := R) (L := L) - exact congrFun (congrArg DFunLike.coe this) lll - --- Finally one of the big theorem! The associativity of the elements in Points under --- convolution product! -lemma Pointmul_assoc (ψ φ ρ : Points R A L) : (ψ * φ) * ρ = ψ * (φ * ρ) := by - rw [hmul1 (ψ*φ) ρ, hmul1 ψ (φ*ρ), left_block_comm, right_block_comm] - ext x - set aaa := (Algebra.TensorProduct.map (Bialgebra.comulAlgHom R A) (AlgHom.id R A)).comp - (Bialgebra.comulAlgHom R A) x with aaa_eq - have h0 : assoc_a aaa = (Algebra.TensorProduct.map (AlgHom.id R A) - (Bialgebra.comulAlgHom R A)) ((Bialgebra.comulAlgHom R A) x) := by - rw [Coassoc (R:=R) (A:=A) (x:=x)]; dsimp - repeat rw [AlgHom.comp_apply] - rw [AlgHom.comp_apply] at aaa_eq - rw [←aaa_eq, ← h0] - set lll := (Algebra.TensorProduct.map (Algebra.TensorProduct.map ψ φ) ρ) aaa - have h1 : ((Algebra.TensorProduct.map ψ (Algebra.TensorProduct.map φ ρ)) - (assoc_a aaa)) = assoc_l lll := by rw [Mapassoc] - rw [h1, Al_assoc_apply] - --- Next we started to prove the other axioms for a monoid : one_mul and mul_one. -/- Again, we decompose the (ψ * one) into a few small steps, and this lemma shows -(id ⊗ ε) ∘ Δ = - ⊗ (1 : R) where ε is counit of A and "-" is any element in A. -/ -lemma Pointmul_onel1 : (Algebra.TensorProduct.map (AlgHom.id R A) - (Bialgebra.counitAlgHom R A)).comp (Bialgebra.comulAlgHom R A) = - Algebra.TensorProduct.includeLeft := by - ext x ; simp only [AlgHom.comp_apply, Bialgebra.comulAlgHom_apply, - Algebra.TensorProduct.includeLeft_apply] - exact Coalgebra.lTensor_counit_comul (R := R) (A := A) x - -/- This lemma decomposes ψ ⊗ one = (id ⊗ η) ∘ (ψ ⊗ id) ∘ (id ⊗ ε) where η is unit of L -/ -lemma Pointmul_onel2 : (Algebra.TensorProduct.map ψ one) = - (Algebra.TensorProduct.map (AlgHom.id R L) - (Algebra.ofId R L)).comp ((Algebra.TensorProduct.map ψ (AlgHom.id R R)).comp - ((Algebra.TensorProduct.map (AlgHom.id R A) - (Bialgebra.counitAlgHom R A)))) := by - rw [oneval] ; ext aa <;> simp - -/- This is the mul_one axiom of the monoid Points R A L-/ -lemma Pointmul_one (ψ : Points R A L) : ψ * one = ψ := by - rw [hmul1, Pointmul_onel2] - have h1 := Pointmul_onel1 (R := R) (A := A) ; ext x - have := congrFun (congrArg DFunLike.coe h1) x - rw [AlgHom.comp_apply, AlgHom.comp_apply, AlgHom.comp_apply, AlgHom.comp_apply] at * - rw [this] ; simp - -/- This lemma shows (ε ⊗ id) ∘ Δ = (1 : R) ⊗ - where "-" is any element of A -/ -lemma Pointone_mul1 : (Algebra.TensorProduct.map (Bialgebra.counitAlgHom R A) - (AlgHom.id R A)).comp (Bialgebra.comulAlgHom R A) = - Algebra.TensorProduct.includeRight := by - ext x ; simp only [AlgHom.comp_apply, Bialgebra.comulAlgHom_apply, - Algebra.TensorProduct.includeRight_apply] - exact Coalgebra.rTensor_counit_comul (R := R) (A := A) x - -/- This lemma decomposes (one ⊗ ψ) = (η ⊗ id) ∘ (id ⊗ ψ) ∘ (ε ⊗ id) -/ -lemma Pointone_mul2 : (Algebra.TensorProduct.map one ψ) = - (Algebra.TensorProduct.map (Algebra.ofId R L) (AlgHom.id R L)).comp - ((Algebra.TensorProduct.map (AlgHom.id R R) ψ).comp - (Algebra.TensorProduct.map (Bialgebra.counitAlgHom R A) (AlgHom.id R A))) - := by rw [oneval] ; ext aa <;> simp - -/- This is the one_mul axiom of the monoid Points R A L-/ -lemma Pointone_mul (ψ : Points R A L) : one * ψ = ψ := by - rw [hmul1, Pointone_mul2] - have h0 := Pointone_mul1 (R := R) (A := A) - ext x ; have := congrFun (congrArg DFunLike.coe h0) x - repeat rw [AlgHom.comp_apply] at * - rw [this] ; simp - -/- Finally we proved Points R A L is indeed a monoid! -/ -instance : Monoid (Points R A L) := -{ mul := mul, - one := one, - mul_assoc := Pointmul_assoc, - one_mul := Pointone_mul, - mul_one := Pointmul_one } --- End of Part I -end -end Points - -namespace HopfPoints -noncomputable section --- This is the second part where I realized not only all Algebra Homomorphisms forms --- a monoid, all the R-Linear Maps from a R-Coalgebra to an R-Algebra also forms a monoid. -variable (H : Type)[CommRing H][HopfAlgebra R H] -variable (L : Type)[CommRing L][Algebra R L] -variable (C : Type)[Ring C][Module R C][Coalgebra R C] -variable (B : Type)[Ring B][Algebra R B] -variable {H L} -variable (A1 A2 : Type)[Ring A1][Ring A2][Bialgebra R A1][Bialgebra R A2] -open HopfAlgebra -open Points -open BigOperators -set_option synthInstance.maxHeartbeats 500000 -instance : Bialgebra R H := inferInstance --- Proving for a Coalgebra C, Lin(C, A) is a monoid (actually it's an algebra) - -/- LinPoints R C B are all the R-LinearMaps from C → B -/ -abbrev LinPoints := C →ₗ[R] B -def linmul (a b : LinPoints R C B) : LinPoints R C B := (LinearMap.mul' R B).comp - ((TensorProduct.map a b).comp (Coalgebra.comul)) - -instance : Mul (LinPoints R C B) := ⟨linmul R C B⟩ -instance : HMul (LinPoints R C B) (LinPoints R C B) (LinPoints R C B) := ⟨linmul R C B⟩ - -/- Definition of multiplication and identity element is the same as the algebra ones - but just in linear version. -/ -lemma linmul1 (a b : LinPoints R C B) : a * b = (LinearMap.mul' R B).comp - ((TensorProduct.map a b).comp (Coalgebra.comul)) := rfl - -def linone : LinPoints R C B := - ((Algebra.ofId R B).toLinearMap.comp (Coalgebra.counit)) -instance : One (LinPoints R C B) := ⟨linone R C B⟩ - -lemma linone' : linone R C B = (Algebra.ofId R B).toLinearMap.comp (Coalgebra.counit) := rfl - -lemma onedef (h : H) : (Algebra.ofId R H) (Coalgebra.counit h) = (linone R H H) h := rfl - -/- The proofs are all similar, first decompose then prove each small block commutes - individually-/ -lemma lblockcomm (ψ φ ρ : LinPoints R C B) : - TensorProduct.map (ψ * φ) ρ = (TensorProduct.map - (LinearMap.mul' R B) (LinearMap.id)).comp - ((TensorProduct.map (TensorProduct.map ψ φ) ρ).comp - (TensorProduct.map (Coalgebra.comul) (LinearMap.id))) := by - symm ; rw [linmul1] ; ext x y ; simp - -lemma rblockcomm (ψ φ ρ : LinPoints R C B) : - TensorProduct.map ψ (φ * ρ) = (TensorProduct.map - (LinearMap.id) (LinearMap.mul' R B)).comp - ((TensorProduct.map ψ (TensorProduct.map φ ρ)).comp - (TensorProduct.map (LinearMap.id) (Coalgebra.comul))) := by - symm ; rw [linmul1] ; ext x y ; simp - -/- We also have the linear version of tensor-associativity maps -/ -abbrev l_assoc_b := (TensorProduct.assoc R B B B).toLinearMap -abbrev l_assoc_c := (TensorProduct.assoc R C C C).toLinearMap - -lemma linCoassoc (x : C): (l_assoc_c R C) ((TensorProduct.map (R := R) (Coalgebra.comul) - (LinearMap.id)).comp (Coalgebra.comul) x) = - (TensorProduct.map (LinearMap.id) (Coalgebra.comul)).comp - (Coalgebra.comul) x := by - repeat rw [LinearMap.comp_apply] ; simp_all only [LinearEquiv.coe_coe] - exact Coalgebra.coassoc_apply (R := R) (A := C) x - -lemma linMapassoc' (ψ φ ρ : LinPoints R C B): - (l_assoc_b R B).comp ((TensorProduct.map (TensorProduct.map ψ φ) ρ)) - = (TensorProduct.map ψ (TensorProduct.map φ ρ)).comp (l_assoc_c R C) := by - ext x ; rfl - -lemma linMapassoc (ψ φ ρ : LinPoints R C B) (ccc : (C ⊗[R] C) ⊗[R] C): - (l_assoc_b R B) (((TensorProduct.map (TensorProduct.map ψ φ) ρ)) ccc) - = (TensorProduct.map ψ (TensorProduct.map φ ρ)) ((l_assoc_c R C) ccc) := by - apply LinearMap.ext_iff.1 (linMapassoc' R C B ψ φ ρ) ccc - -lemma linten_assoc : (LinearMap.mul' R B).comp ((TensorProduct.map - (LinearMap.mul' R B) (LinearMap.id))) = - (LinearMap.mul' R B).comp ((TensorProduct.map (R := R) (LinearMap.id (M := B)) - (LinearMap.mul' R B)).comp (l_assoc_b R B)) := by - ext x1 x2 x3 - simp only [TensorProduct.AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, - LinearMap.coe_restrictScalars, LinearMap.comp_apply, TensorProduct.map_tmul, - LinearMap.mul'_apply, LinearMap.id_coe, id_eq, LinearEquiv.coe_coe, TensorProduct.assoc_tmul] - rw [mul_assoc] - -lemma linten_assoc_apply (bbb : (B ⊗[R] B) ⊗[R] B) : (LinearMap.mul' R B) - ((TensorProduct.map (LinearMap.mul' R B) (LinearMap.id)) bbb) = - (LinearMap.mul' R B) ((TensorProduct.map (LinearMap.id) - (LinearMap.mul' R B)) ((l_assoc_b R B) bbb)) := by - have := linten_assoc (R := R) (B := B) - rw [DFunLike.ext_iff] at this ; apply this - -/- Associativity law of R-linear maps under convolution product-/ -lemma lin_assoc (ψ φ ρ : LinPoints R C B) : (ψ * φ) * ρ = ψ * (φ * ρ) := by - rw [linmul1 R C B (ψ*φ) ρ, linmul1 R C B ψ (φ*ρ), lblockcomm, rblockcomm] - ext x ; simp only [LinearMap.comp_apply] - set ccc := ((TensorProduct.map Coalgebra.comul LinearMap.id) - (Coalgebra.comul (R := R) x)) with ccc_eq - have h0 : (l_assoc_c R C) ccc = ((TensorProduct.map LinearMap.id Coalgebra.comul) - (Coalgebra.comul x)) := linCoassoc R C x - rw [←h0] ; set bbb := (TensorProduct.map (TensorProduct.map ψ φ) ρ) ccc - have h1 : (l_assoc_b R B) bbb = (TensorProduct.map ψ (TensorProduct.map φ ρ)) - ((l_assoc_c R C) ccc) := linMapassoc R C B ψ φ ρ ccc - rw [←h1, linten_assoc_apply] - -lemma linmul_one1 (ψ : LinPoints R C B): (TensorProduct.map ψ (linone R C B)) = - (TensorProduct.map (LinearMap.id (M := B)) (Algebra.ofId R B).toLinearMap).comp - ((TensorProduct.map ψ (LinearMap.id)).comp - ((TensorProduct.map (LinearMap.id) (Coalgebra.counit (A := C))))) := by - unfold linone ; ext c1 c2 ; simp - -/- mul_one lemma for R-linear maps -/ -lemma linmul_one (ψ : LinPoints R C B) : ψ * linone R C B = ψ := by - rw [linmul1 , linmul_one1] - ext x - have := (Coalgebra.lTensor_counit_comul (R := R) (A := C)) x - simp only [LinearMap.comp_apply] - have h1 : (TensorProduct.map LinearMap.id Coalgebra.counit) (Coalgebra.comul x) - = x ⊗ₜ[R] 1 := by exact this - rw [h1] ; simp - -lemma linone_mull1 (ψ : LinPoints R C B): (TensorProduct.map (linone R C B) ψ) = - (TensorProduct.map (Algebra.ofId R B).toLinearMap LinearMap.id).comp - ((TensorProduct.map LinearMap.id ψ).comp - (TensorProduct.map (Coalgebra.counit (A := C)) LinearMap.id)):= by - unfold linone ; ext c1 c2 ;simp - -/- one_mul lemma for R-linear maps -/ -lemma linone_mul (ψ : LinPoints R C B) : linone R C B * ψ = ψ := by - rw [linmul1 , linone_mull1] ; ext x - have counitac := Coalgebra.rTensor_counit_comul (R := R) (A := C) x - simp only [LinearMap.comp_apply] - have h1 : (TensorProduct.map Coalgebra.counit LinearMap.id) (Coalgebra.comul x) - = 1 ⊗ₜ[R] x := by exact counitac - rw [h1] ; simp - -instance : Monoid (LinPoints R C B) where - mul := linmul R C B - mul_assoc := lin_assoc R C B - one := linone R C B - one_mul := linone_mul R C B - mul_one := linmul_one R C B - -instance : Monoid (LinPoints R H H) := inferInstance ---End of Part II - --- Part III is some preparation for the final big theorem (Hom(H, A) forms a group) which is --- mainly proving tensor product of R-Bialgebras is still a R-Bialgebra. - -lemma repr (x : C) (ι : Type*) (I : Finset ι) (x1 x2 : ι → C) - (h : Coalgebra.comul x = ∑ i in I, x1 i ⊗ₜ[R] x2 i) - (f g: LinPoints R C B) : (f * g) x = ∑ i in I, f (x1 i) * g (x2 i) := by - rw [linmul1] - simp only [LinearMap.comp_apply] ; symm ; rw [h] - simp only [map_sum, TensorProduct.map_tmul, LinearMap.mul'_apply] - -/-This is the sweedler notation of comultiplication, which is writing - Δ x = ∑ i , x1 i ⊗ x2 i where Δ is comul of C -/ -lemma comul_repr (x : C) : ∃ (I : Finset (C ⊗[R] C)) (x1 : C ⊗[R] C → C) (x2 : C ⊗[R] C → C), - Coalgebra.comul (R := R) x = ∑ i in I, x1 i ⊗ₜ[R] x2 i := by - -- make if ... then ... else work - classical - set cc := Coalgebra.comul (R := R) x with cc_eq - have mem1 : cc ∈ (⊤ : Submodule R (C ⊗[R] C)) := ⟨⟩ - -- Use the fact that tensorproduct space is spanned by pure tensors - rw [← TensorProduct.span_tmul_eq_top, mem_span_set] at mem1 - obtain ⟨r, hr, (eq1 : ∑ i in r.support, (_ • _) = _)⟩ := mem1 - choose a a' haa' using hr - replace eq1 := calc _ - cc = ∑ i in r.support, r i • i := eq1.symm - _ = ∑ i in r.support.attach, (r i : R) • (i : (C ⊗[R] C)) - := Finset.sum_attach _ _ |>.symm - _ = ∑ i in r.support.attach, (r i • a i.2 ⊗ₜ[R] a' i.2) := by - apply Finset.sum_congr rfl - intro i hi - rw [haa' i.2] - _ = ∑ i in r.support.attach, ((r i • a i.2) ⊗ₜ[R] a' i.2) := by - apply Finset.sum_congr rfl - intro i hi - rw [TensorProduct.smul_tmul'] - use r.support - use fun i => if h : i ∈ r.support then r i • a h else 0 - use fun i => if h : i ∈ r.support then a' h else 0 - rw [eq1] ; conv_rhs => rw [← Finset.sum_attach] - refine Finset.sum_congr rfl fun _ _ ↦ (by split_ifs with h <;> aesop) - --- This is used to define the Comul of A1 ⊗[R] A2 -def Bialg_tensorequiv : (A1 ⊗[R] A1) ⊗[R] (A2 ⊗[R] A2) →ₗ[R] (A1 ⊗[R] A2) ⊗[R] (A1 ⊗[R] A2) := - (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ - LinearMap.rTensor A2 - ((TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ - LinearMap.lTensor A1 (TensorProduct.comm _ _ _).toLinearMap ∘ₗ - (TensorProduct.assoc _ _ _ _).toLinearMap) ∘ₗ - (TensorProduct.assoc _ _ _ _).symm.toLinearMap - --- Define the linear equivalence of (A1 ⊗[R] A1) ⊗[R] (A2 ⊗[R] A2) and --- (A1 ⊗[R] A2) ⊗[R] (A1 ⊗[R] A2) -private noncomputable def reorder4 : (A1 ⊗[R] A1) ⊗[R] A2 ⊗[R] A2 ≃ₗ[R] - (A1 ⊗[R] A2) ⊗[R] A1 ⊗[R] A2 := - LinearEquiv.ofLinear - ((TensorProduct.assoc R A1 A2 (A1 ⊗[R] A2)).symm.toLinearMap ∘ₗ - (TensorProduct.assoc R A2 A1 A2).toLinearMap.lTensor A1 ∘ₗ - ((TensorProduct.comm R A1 A2).rTensor A2).lTensor A1 ∘ₗ - (TensorProduct.assoc R A1 A2 A2).symm.toLinearMap.lTensor A1 ∘ₗ - (TensorProduct.assoc R A1 A1 (A2 ⊗[R] A2)).toLinearMap) - ((TensorProduct.assoc R A1 A1 (A2 ⊗[R] A2)).symm.toLinearMap ∘ₗ - (TensorProduct.assoc R A1 A2 A2).toLinearMap.lTensor A1 ∘ₗ - ((TensorProduct.comm R A2 A1).rTensor A2).lTensor A1 ∘ₗ - (TensorProduct.assoc R A2 A1 A2).symm.toLinearMap.lTensor A1 ∘ₗ - (TensorProduct.assoc R A1 A2 (A1 ⊗[R] A2)).toLinearMap) - (by aesop) (by aesop) - --- Define the linear equivalence of (A1 ⊗[R] A2) ⊗[R] (A1 ⊗[R] A2) ⊗[R] A1 ⊗[R] A2 --- and (A1 ⊗[R] A1 ⊗[R] A1) ⊗[R] A2 ⊗[R] A2 ⊗[R] A2 -private noncomputable def reorder6 : - (A1 ⊗[R] A2) ⊗[R] (A1 ⊗[R] A2) ⊗[R] A1 ⊗[R] A2 ≃ₗ[R] - (A1 ⊗[R] A1 ⊗[R] A1) ⊗[R] A2 ⊗[R] A2 ⊗[R] A2 := - LinearEquiv.ofLinear - ((TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ - (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ - (((TensorProduct.assoc _ _ _ _).toLinearMap.rTensor A2).rTensor A2 ∘ₗ - (TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ - (TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ - (TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ - (((TensorProduct.comm R (A2 ⊗[R] A2) A1).lTensor A1).lTensor A1) ∘ₗ - (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ - (TensorProduct.assoc _ _ _ _).toLinearMap).rTensor A2 ∘ₗ - (TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ - ((reorder4 R A1 A2).symm.rTensor (A1 ⊗[R] A2)) ∘ₗ - (TensorProduct.assoc _ _ _ _).symm.toLinearMap) - ((TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ - ((reorder4 R A1 A2).rTensor (A1 ⊗[R] A2)) ∘ₗ - (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ - LinearMap.rTensor A2 - ((TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ - (TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ - ((TensorProduct.comm R A1 (A2 ⊗[R] A2)).lTensor A1).lTensor A1 ∘ₗ - (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ - (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ - (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ - ((TensorProduct.assoc _ _ _ _).symm.toLinearMap.rTensor A2).rTensor A2) ∘ₗ - (TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ - (TensorProduct.assoc _ _ _ _).symm.toLinearMap) - (by aesop) (by aesop) - --- How reorder acts elementwise -lemma reorder6_tmul (a1 a2 a3 : A1) (b1 b2 b3 : A2) : - reorder6 R A1 A2 ((a1 ⊗ₜ[R] b1) ⊗ₜ[R] (a2 ⊗ₜ[R] b2) ⊗ₜ[R] (a3 ⊗ₜ[R] b3)) = - (a1 ⊗ₜ[R] a2 ⊗ₜ[R] a3) ⊗ₜ[R] (b1 ⊗ₜ[R] b2 ⊗ₜ[R] b3) := rfl - --- Since comul is not allowed before proving that A1 ⊗[R] A2 is a bialgebra, --- in order to fasten the speed, we had to define the comul map manually. -abbrev tcomul := (Bialg_tensorequiv R A1 A2).comp - (TensorProduct.map (M := A1) (N := A2) (Bialgebra.comulAlgHom R (A := A1)) - (Bialgebra.comulAlgHom R (A := A2))) - -lemma tcomul_eq : tcomul R A1 A2 = - (Bialg_tensorequiv R A1 A2).comp - (TensorProduct.map (M := A1) (N := A2) (Coalgebra.comul (R := R) (A := A1)) - (Coalgebra.comul (R := R) (A := A2))) := rfl - --- How tcomul acts elementwise -lemma tcomul_tmul (x : A1) (y : A2) : - tcomul R A1 A2 (x ⊗ₜ y) = Bialg_tensorequiv R A1 A2 - (Coalgebra.comul x ⊗ₜ Coalgebra.comul y) := rfl - -/- Same as comul_repr, we wrote our own sweedler notation for comul of A1 ⊗[R] A2 -/ -lemma tcomul_repr (x : A1) (y : A2) {ι1 ι2 : Type*} (s1 : Finset ι1) (s2 : Finset ι2) - (a1 a2 : ι1 → A1) (b1 b2 : ι2 → A2) - (eq1 : Coalgebra.comul (R := R) x = ∑ i in s1, a1 i ⊗ₜ a2 i) - (eq2 : Coalgebra.comul (R := R) y = ∑ i in s2, b1 i ⊗ₜ b2 i) : - tcomul R A1 A2 (x ⊗ₜ y) = - ∑ i in s1, ∑ j in s2, (a1 i ⊗ₜ b1 j) ⊗ₜ (a2 i ⊗ₜ b2 j) := by - rw [tcomul_eq] - simp only [LinearMap.coe_comp, comp_apply, TensorProduct.map_tmul, eq1, eq2, - TensorProduct.tmul_sum, TensorProduct.sum_tmul, map_sum, Bialg_tensorequiv, - TensorProduct.assoc_symm_tmul, LinearMap.rTensor_tmul, LinearEquiv.coe_coe, - TensorProduct.assoc_tmul, LinearMap.lTensor_tmul, TensorProduct.comm_tmul] - rw [Finset.sum_comm] - - -lemma Equiv_apply (x1 x1' : A1) (x2 x2' : A2) : Bialg_tensorequiv R A1 A2 - ((x1 ⊗ₜ[R] x1') ⊗ₜ[R] (x2 ⊗ₜ[R] x2')) = (x1 ⊗ₜ[R] x2) ⊗ₜ[R] (x1' ⊗ₜ[R] x2') := by - simp [Bialg_tensorequiv] - -/- As te introduction of this axiom of Bialgebra says, this is a weird way that lean uses to - check the "map_mul" property of comul of (A1 ⊗ A2) by checking two bilinear maps are the - same-/ -lemma mul_comp₂_tencomul : LinearMap.compr₂ (LinearMap.mul R (A1 ⊗[R] A2)) (tcomul R A1 A2) = - LinearMap.compl₁₂ (LinearMap.mul R ((A1 ⊗[R] A2) ⊗[R] A1 ⊗[R] A2)) - (tcomul R A1 A2) (tcomul R A1 A2) := by - ext x1 x2 x1' x2' ; simp only [tcomul, AlgHom.toNonUnitalAlgHom_eq_coe, - NonUnitalAlgHom.toDistribMulActionHom_eq_coe, TensorProduct.AlgebraTensorModule.curry_apply, - TensorProduct.curry_apply, LinearMap.coe_restrictScalars, LinearMap.compr₂_apply, - LinearMap.mul_apply', Algebra.TensorProduct.tmul_mul_tmul, LinearMap.coe_comp, comp_apply, - TensorProduct.map_tmul, DistribMulActionHom.coe_toLinearMap, - NonUnitalAlgHom.coe_to_distribMulActionHom, map_mul, NonUnitalAlgHom.coe_coe, - Bialgebra.comulAlgHom_apply, LinearMap.compl₁₂_apply] - obtain ⟨I1, x11, x12, h1⟩ := comul_repr R A1 x1 - obtain ⟨I1', x11', x12', h1'⟩ := comul_repr R A1 x1' - obtain ⟨I2, x21, x22, h2⟩ := comul_repr R A2 x2 - obtain ⟨I2', x21', x22', h2'⟩ := comul_repr R A2 x2' - rw [h1, h1', h2, h2', Finset.sum_mul_sum, Finset.sum_mul_sum] - simp_rw [Algebra.TensorProduct.tmul_mul_tmul] - rw [TensorProduct.sum_tmul, TensorProduct.sum_tmul, TensorProduct.sum_tmul] - simp_rw [TensorProduct.tmul_sum]; simp_rw [TensorProduct.sum_tmul] - simp_rw [map_sum, Equiv_apply R A1 A2] ; rw [Finset.sum_mul_sum] - simp_rw [Finset.sum_mul_sum, Algebra.TensorProduct.tmul_mul_tmul] - refine Finset.sum_congr rfl fun i1 hi1 ↦ ?_ - symm ; rw [Finset.sum_comm] ; refine Finset.sum_congr rfl fun _ _ ↦ Finset.sum_comm - -/- Again, since counit of A1 ⊗ A2 can't be used, we use ten_counit just for convenience -/ -abbrev ten_counit: A1 ⊗[R] A2 →ₐ[R] R := (Algebra.TensorProduct.lmul' R (S := R)).comp - (Algebra.TensorProduct.map (Bialgebra.counitAlgHom R A1) (Bialgebra.counitAlgHom R A2)) - --- The following three lemmas are the lemmas designed to help prove --- "lTensor_counit_comp_comul" axiom of Bialgebra. - -/- This is saying a * one(b) = ε(b) • a -/ -lemma one_eq (a b : A1) : a * (Algebra.ofId R A1) - (Coalgebra.counit (R := R) (A := A1) (b)) = - Coalgebra.counit (R := R) (A := A1) (b) • a := by - rw [← mul_one (Coalgebra.counit (R := R) (A := A1) (b)), ← Algebra.id.smul_eq_mul, map_smul, - map_one, Algebra.mul_smul_comm, mul_one, smul_eq_mul, mul_one] - -/- This lemma is one side of the sweedler notation of x which is: - x = ∑ i ε(x2 i) • x1 i -/ -lemma tensorId_eq (I1: Finset (A1 ⊗[R] A1)) (x1 x2 : A1 ⊗[R] A1 → A1) (x : A1) - (hx: Coalgebra.comul x = ∑ i in I1, x1 i ⊗ₜ[R] x2 i): - ∑ i in I1, (Coalgebra.counit (R := R) (A := A1) (x2 i)) • x1 i = x := by - symm ; calc _ - x = (LinearMap.id (R := R) (M := A1)) x := rfl - _ = ((LinearMap.id (R := R) (M := A1)) * linone R A1 A1) x := by rw [linmul_one] - _ = (LinearMap.mul' R A1) ((TensorProduct.map - (LinearMap.id (R := R) (M := A1)) (linone R A1 A1)) (Coalgebra.comul x)) := by - rw [linmul1] ; simp only [LinearMap.comp_apply] - rw [hx, linone'] ; simp only [map_sum, TensorProduct.map_tmul, LinearMap.id_coe, id_eq, - LinearMap.comp_apply, AlgHom.toLinearMap_apply, LinearMap.mul'_apply] - simp_rw [one_eq] - -/- This is just one of the sub-result I need for lTensor, I copied this from the goal -/ -lemma swap_equiv (I2: Finset (A2 ⊗[R] A2)) (I1: Finset (A1 ⊗[R] A1)) (x1 x2 : A1 ⊗[R] A1 → A1) - (y1 y2 : A2 ⊗[R] A2 → A2) (x : A1) (y : A2) (hy: Coalgebra.comul y = ∑ i in I2, y1 i ⊗ₜ[R] y2 i) - (hx: Coalgebra.comul x = ∑ i in I1, x1 i ⊗ₜ[R] x2 i): - ∑ x in I2, ∑ x_1 in I1, (((Coalgebra.counit (R := R) (A := A1) (x2 x_1)) * - (Coalgebra.counit (R := R) (A := A2) (y2 x))) • x1 x_1) ⊗ₜ[R] y1 x ⊗ₜ[R] (1 : R) = - x ⊗ₜ[R] y ⊗ₜ[R] 1 := by - have : ∑ x in I2, ∑ x_1 in I1, (((Coalgebra.counit (R := R) (A := A1) (x2 x_1)) * - (Coalgebra.counit (R := R) (A := A2) (y2 x))) • x1 x_1) ⊗ₜ[R] y1 x ⊗ₜ[R] (1 : R) = - ∑ x in I2, ∑ x_1 in I1, (((Coalgebra.counit (R := R) (A := A2) (y2 x)) * - (Coalgebra.counit (R := R) (A := A1) (x2 x_1))) • x1 x_1) ⊗ₜ[R] y1 x ⊗ₜ[R] (1 : R) := by - apply Finset.sum_congr rfl ; intro x hx - apply Finset.sum_congr rfl ; intro x_1 hx_1 - rw [mul_comm] - rw [this] ; simp_rw [← smul_smul, ← TensorProduct.sum_tmul, ← Finset.smul_sum] - rw [tensorId_eq R A1 I1 x1 x2 x hx]; simp_rw [TensorProduct.smul_tmul] - simp_rw [TensorProduct.smul_tmul', ← TensorProduct.tmul_sum, ← TensorProduct.sum_tmul] - rw [tensorId_eq R A2 I2 y1 y2 y hy] - -/- This is one of the axioms of Bialgebra : (id ⊗ ε) ∘ Δ = id ⊗ (1 : R) where ε is the - counit of A1 ⊗ A2 -/ -lemma lTensor_tensor : LinearMap.lTensor (A1 ⊗[R] A2) (ten_counit R A1 A2) ∘ₗ (tcomul R A1 A2) = - (LinearMap.flip (TensorProduct.mk R (A1 ⊗[R] A2) R)) 1 := by - ext x y ; simp only [ten_counit, tcomul, Bialg_tensorequiv,AlgHom.toNonUnitalAlgHom_eq_coe, - NonUnitalAlgHom.toDistribMulActionHom_eq_coe, TensorProduct.AlgebraTensorModule.curry_apply, - TensorProduct.curry_apply, LinearMap.coe_restrictScalars, LinearMap.coe_comp, - LinearEquiv.coe_coe, comp_apply, TensorProduct.map_tmul, DistribMulActionHom.coe_toLinearMap, - NonUnitalAlgHom.coe_to_distribMulActionHom, NonUnitalAlgHom.coe_coe, - Bialgebra.comulAlgHom_apply, LinearMap.flip_apply, TensorProduct.mk_apply] - obtain ⟨I1, x1, x2, hx⟩ := comul_repr R A1 x - obtain ⟨I2, y1, y2, hy⟩ := comul_repr R A2 y ; rw [hx, hy] - rw [TensorProduct.tmul_sum] ; simp_rw [TensorProduct.sum_tmul] - simp only [map_sum, TensorProduct.assoc_symm_tmul, LinearMap.rTensor_tmul, LinearMap.coe_comp, - LinearEquiv.coe_coe, comp_apply, TensorProduct.assoc_tmul, LinearMap.lTensor_tmul, - TensorProduct.comm_tmul, DistribMulActionHom.coe_toLinearMap, - NonUnitalAlgHom.coe_to_distribMulActionHom, NonUnitalAlgHom.coe_coe, AlgHom.coe_comp, - Algebra.TensorProduct.map_tmul, Bialgebra.counitAlgHom_apply, - Algebra.TensorProduct.lmul'_apply_tmul] - simp_rw [← TensorProduct.assoc_symm_tmul, ← map_sum, ← Algebra.id.smul_eq_mul, - TensorProduct.tmul_smul] - calc _ - (LinearEquiv.symm (TensorProduct.assoc R A1 A2 R)) (∑ x in I2, ∑ x_1 in I1, - (Coalgebra.counit (R := R) (A := A1) (x2 x_1)) • x1 x_1 ⊗ₜ[R] y1 x ⊗ₜ[R] - (Coalgebra.counit (R := R) (A := A2) (y2 x))) = - (LinearEquiv.symm (TensorProduct.assoc R A1 A2 R)) (∑ x in I2, ∑ x_1 in I1, - (Coalgebra.counit (R := R) (A := A1) (x2 x_1)) • x1 x_1 ⊗ₜ[R] y1 x ⊗ₜ[R] - (Coalgebra.counit (y2 x) * (1 : R))) := by simp only [mul_one] - simp_rw [← Algebra.id.smul_eq_mul, TensorProduct.tmul_smul, TensorProduct.smul_tmul', smul_smul] - rw [swap_equiv R A1 A2 I2 I1 x1 x2 y1 y2 x y hy hx] - --- The following two lemmas are designed to help improve my proof of "rTensor_counit_comp_comul" -/- This is saying one(a) * b = ε(a) • b -/ -lemma eq_one (a b : A1) : - (Algebra.ofId R A1) (Coalgebra.counit (R := R) (A := A1) (a)) * b = - (Coalgebra.counit (R := R) (A := A1) (a)) • b := by - rw [← mul_one (Coalgebra.counit (R := R) (A := A1) (a)), ← Algebra.id.smul_eq_mul, map_smul, - map_one, Algebra.smul_mul_assoc, one_mul, smul_eq_mul, mul_one] - -/- This lemma shows another side of the sweedler notation of x which is: - x = ∑ i ε(x1 i) • x2 i -/ -lemma tensorEq_id (I1 : Finset (A1 ⊗[R] A1)) (x1 x2 : A1 ⊗[R] A1 → A1) (x : A1) - (hx: Coalgebra.comul x = ∑ i in I1, x1 i ⊗ₜ[R] x2 i): - ∑ a in I1, (Coalgebra.counit (R := R) (A := A1) (x1 a)) • x2 a = x := by - symm ; calc _ - x = (LinearMap.id (R := R) (M := A1)) x := rfl - _ = ((linone R A1 A1) * (LinearMap.id (R := R) (M := A1))) x := by rw [linone_mul] - _ = (LinearMap.mul' R A1) ((TensorProduct.map - (linone R A1 A1) (LinearMap.id (R := R) (M := A1))) (Coalgebra.comul x)) := by - rw [linmul1] ; simp only [LinearMap.comp_apply] - rw [hx, linone'] ; simp only [map_sum, TensorProduct.map_tmul, LinearMap.coe_comp, comp_apply, - AlgHom.toLinearMap_apply, LinearMap.id_coe, id_eq, LinearMap.mul'_apply] - simp_rw [eq_one R A1] - -/- Again, this is another axiom of Bialgebra which is just a opposite direction of - lTensor : (ε ⊗ id) ∘ Δ = (1 : R) ⊗ id -/ -lemma rTensor_tensor : LinearMap.rTensor (A1 ⊗[R] A2) - (ten_counit R A1 A2) ∘ₗ (tcomul R A1 A2) = - (TensorProduct.mk R R (A1 ⊗[R] A2)) 1 := by - ext x y ; unfold ten_counit ; unfold tcomul ; unfold Bialg_tensorequiv - simp only [AlgHom.toNonUnitalAlgHom_eq_coe, NonUnitalAlgHom.toDistribMulActionHom_eq_coe, - TensorProduct.AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, - LinearMap.coe_restrictScalars, LinearMap.coe_comp, LinearEquiv.coe_coe, comp_apply, - TensorProduct.map_tmul, DistribMulActionHom.coe_toLinearMap, - NonUnitalAlgHom.coe_to_distribMulActionHom, NonUnitalAlgHom.coe_coe, - Bialgebra.comulAlgHom_apply, TensorProduct.mk_apply] - obtain ⟨I1, x1, x2, hx⟩ := comul_repr R A1 x - obtain ⟨I2, y1, y2, hy⟩ := comul_repr R A2 y ; rw [hx, hy] - rw [TensorProduct.tmul_sum] ; simp_rw [TensorProduct.sum_tmul] - simp only [map_sum, TensorProduct.assoc_symm_tmul, LinearMap.rTensor_tmul, LinearMap.coe_comp, - LinearEquiv.coe_coe, comp_apply, TensorProduct.assoc_tmul, LinearMap.lTensor_tmul, - TensorProduct.comm_tmul, DistribMulActionHom.coe_toLinearMap, - NonUnitalAlgHom.coe_to_distribMulActionHom, NonUnitalAlgHom.coe_coe, AlgHom.coe_comp, - Algebra.TensorProduct.map_tmul, Bialgebra.counitAlgHom_apply, - Algebra.TensorProduct.lmul'_apply_tmul] - simp_rw [← Algebra.id.smul_eq_mul, TensorProduct.smul_tmul, TensorProduct.smul_tmul'] - simp_rw [← TensorProduct.tmul_sum, ← TensorProduct.sum_tmul] - rw [tensorEq_id R A1 I1 x1 x2 x hx] - calc _ - ∑ x_1 in I2, (Coalgebra.counit (R := R) (A := A2) (y1 x_1)) ⊗ₜ[R] x ⊗ₜ[R] y2 x_1 = - ∑ x_1 in I2, ((Coalgebra.counit (R := R) (A := A2) (y1 x_1)) * - (1 : R)) ⊗ₜ[R] x ⊗ₜ[R] y2 x_1 := by simp only [mul_one] - simp_rw [← Algebra.id.smul_eq_mul, TensorProduct.smul_tmul, TensorProduct.smul_tmul'] - simp_rw [← TensorProduct.tmul_sum, TensorProduct.smul_tmul, ← TensorProduct.tmul_sum] - rw [tensorEq_id R A2 I2 y1 y2 y hy] - -open TensorProduct in - -/- This is the coassoc axiom for Bialgebra(I probably should put a Coalgebra instance - first because the proof of this is really complicated...) Jujiang helped a lot with - this proof :)) -/ - -set_option tactic.skipAssignedInstances false -lemma tensor_coassoc : ↑(TensorProduct.assoc R (A1 ⊗[R] A2) (A1 ⊗[R] A2) (A1 ⊗[R] A2)) ∘ₗ - LinearMap.rTensor (A1 ⊗[R] A2) (tcomul R A1 A2) ∘ₗ (tcomul R A1 A2) = - LinearMap.lTensor (A1 ⊗[R] A2) (tcomul R A1 A2) ∘ₗ (tcomul R A1 A2) := by - set LL := _; set RR := _; change LL = RR -- LL and RR are left and right hand side repectively - - -- This is using the property that reorder6 is a linear equivalence (actually injective would - -- probably be enough ...?) - suffices (reorder6 R A1 A2).toLinearMap ∘ₗ LL = (reorder6 R A1 A2).toLinearMap ∘ₗ RR by - rw [← LinearEquiv.toLinearMap_symm_comp_eq, ← LinearMap.comp_assoc] at this - simp [← this] - - -- This is just the tensor product of the coassoc property of each of A1 and A2 - -- (Tensor product of the equation) - have EQ := congr_arg₂ TensorProduct.map - (Coalgebra.coassoc (R := R) (A := A1)) (Coalgebra.coassoc (R := R) (A := A2)) - - -- Again, setting LLEQ and RREQ to be the left and right hand side of EQ - set LLEQ := _; set RREQ := _; change LLEQ = RREQ at EQ - - -- The proof is done by proving the left and right hand side of the goal is in fact - -- the left and right hand side of EQ (tensor product of individual coassocs) - have eq1 : LLEQ = (reorder6 R A1 A2).toLinearMap ∘ₗ LL - -- Proving left hand side equality - · ext x y - obtain ⟨I1, x1, x2, hx⟩ := comul_repr R A1 x - obtain ⟨I2, y1, y2, hy⟩ := comul_repr R A2 y - simp (config := - { zetaDelta := true, zeta := false }) only [TensorProduct.AlgebraTensorModule.curry_apply, - TensorProduct.curry_apply, LinearMap.coe_restrictScalars, TensorProduct.map_tmul, - LinearMap.coe_comp, LinearEquiv.coe_coe, comp_apply, hx, map_sum, LinearMap.rTensor_tmul, hy, - TensorProduct.tmul_sum, TensorProduct.sum_tmul, AlgHom.toNonUnitalAlgHom_eq_coe, - NonUnitalAlgHom.toDistribMulActionHom_eq_coe, DistribMulActionHom.coe_toLinearMap, - NonUnitalAlgHom.coe_to_distribMulActionHom, NonUnitalAlgHom.coe_coe, - Bialgebra.comulAlgHom_apply] - -- [TensorProduct.curry_apply, - -- LinearMap.coe_restrictScalars, map_tmul, LinearMap.coe_comp, LinearEquiv.coe_coe, comp_apply, - -- hx, map_sum, LinearMap.rTensor_tmul, hy, tmul_sum, sum_tmul, AlgHom.toNonUnitalAlgHom_eq_coe, - -- NonUnitalAlgHom.toDistribMulActionHom_eq_coe, DistribMulActionHom.coe_toLinearMap, - -- NonUnitalAlgHom.coe_to_distribMulActionHom, NonUnitalAlgHom.coe_coe, - -- Bialgebra.comulAlgHom_apply, Bialg_tensorequiv, assoc_symm_tmul, assoc_tmul, - -- LinearMap.lTensor_tmul, comm_tmul] - refine Finset.sum_congr rfl fun i1 hi1 ↦ Finset.sum_congr rfl fun i2 hi2 ↦ ?_ - obtain ⟨I, x11, x12, hx1⟩ := comul_repr R A1 (x1 i2) - obtain ⟨J, y11, y12, hy1⟩ := comul_repr R A2 (y1 i1) - simp only [hx1, TensorProduct.sum_tmul, map_sum, TensorProduct.assoc_tmul, hy1, - TensorProduct.tmul_sum, Bialg_tensorequiv, LinearMap.coe_comp, LinearEquiv.coe_coe, - comp_apply, TensorProduct.assoc_symm_tmul, LinearMap.rTensor_tmul, LinearMap.lTensor_tmul, - TensorProduct.comm_tmul, AlgHom.toNonUnitalAlgHom_eq_coe, - NonUnitalAlgHom.toDistribMulActionHom_eq_coe, TensorProduct.map_tmul, - DistribMulActionHom.coe_toLinearMap, NonUnitalAlgHom.coe_to_distribMulActionHom, - NonUnitalAlgHom.coe_coe, Bialgebra.comulAlgHom_apply, reorder6_tmul, - NonUnitalAlgHom.toDistribMulActionHom_eq_coe, TensorProduct.map_tmul, - DistribMulActionHom.coe_toLinearMap, NonUnitalAlgHom.coe_to_distribMulActionHom, - NonUnitalAlgHom.coe_coe, Bialgebra.comulAlgHom_apply, reorder6_tmul] - - have eq2 : RREQ = (reorder6 R A1 A2).toLinearMap ∘ₗ RR - -- Proving right hand side equality - · ext x y - obtain ⟨I1, x1, x2, hx⟩ := comul_repr R A1 x - obtain ⟨I2, y1, y2, hy⟩ := comul_repr R A2 y - simp (config := - { zetaDelta := true, zeta := false }) only [TensorProduct.AlgebraTensorModule.curry_apply, - TensorProduct.curry_apply, LinearMap.coe_restrictScalars, TensorProduct.map_tmul, - LinearMap.coe_comp, comp_apply, hx, map_sum, LinearMap.lTensor_tmul, hy, - TensorProduct.tmul_sum, TensorProduct.sum_tmul, LinearEquiv.coe_coe, Bialg_tensorequiv, - AlgHom.toNonUnitalAlgHom_eq_coe, NonUnitalAlgHom.toDistribMulActionHom_eq_coe, - DistribMulActionHom.coe_toLinearMap, NonUnitalAlgHom.coe_to_distribMulActionHom, - NonUnitalAlgHom.coe_coe, Bialgebra.comulAlgHom_apply, TensorProduct.assoc_symm_tmul, - LinearMap.rTensor_tmul, TensorProduct.assoc_tmul, TensorProduct.comm_tmul] - -- [AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, - -- LinearMap.coe_restrictScalars, map_tmul, LinearMap.coe_comp, LinearEquiv.coe_coe, comp_apply, - -- hx, map_sum, LinearMap.rTensor_tmul, hy, tmul_sum, sum_tmul, AlgHom.toNonUnitalAlgHom_eq_coe, - -- NonUnitalAlgHom.toDistribMulActionHom_eq_coe, DistribMulActionHom.coe_toLinearMap, - -- NonUnitalAlgHom.coe_to_distribMulActionHom, NonUnitalAlgHom.coe_coe, - -- Bialgebra.comulAlgHom_apply, Bialg_tensorequiv, assoc_symm_tmul, assoc_tmul, - -- LinearMap.lTensor_tmul, comm_tmul] - refine Finset.sum_congr rfl fun i1 hi1 ↦ Finset.sum_congr rfl fun i2 hi2 ↦ ?_ - obtain ⟨I, x11, x12, hx1⟩ := comul_repr R A1 (x2 i2) - obtain ⟨J, y11, y12, hy1⟩ := comul_repr R A2 (y2 i1) - simp only [hx1, TensorProduct.sum_tmul, map_sum, TensorProduct.assoc_tmul, hy1, - TensorProduct.tmul_sum, TensorProduct.assoc_symm_tmul, - LinearMap.rTensor_tmul, LinearMap.coe_comp, LinearEquiv.coe_coe, comp_apply, - LinearMap.lTensor_tmul, TensorProduct.comm_tmul, reorder6_tmul] - - rw [← eq1, ← eq2, EQ] - -/- Big Thoerem! Tensor product of Bialgebra is indeed a Bialgebra! -/ -instance : Bialgebra R (A1 ⊗[R] A2) where - comul := tcomul R A1 A2 - counit := ten_counit R A1 A2 - coassoc := tensor_coassoc R A1 A2 - rTensor_counit_comp_comul := rTensor_tensor R A1 A2 - lTensor_counit_comp_comul := lTensor_tensor R A1 A2 - -- this shows ε(1) = (1 : R) for 1 ∈ A1 ⊗ A2 - counit_one := by simp only [AlgHom.toNonUnitalAlgHom_eq_coe, - NonUnitalAlgHom.toDistribMulActionHom_eq_coe, DistribMulActionHom.coe_toLinearMap, - NonUnitalAlgHom.coe_to_distribMulActionHom, NonUnitalAlgHom.coe_coe, map_one] - -- showing counit is indeed an algebra homomorphism ε(ab) = ε(a) * ε(b) - mul_compr₂_counit := by - simp only [AlgHom.toNonUnitalAlgHom_eq_coe, - NonUnitalAlgHom.toDistribMulActionHom_eq_coe] - ext x1 x2 x1' x2' - simp only [TensorProduct.AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, - LinearMap.coe_restrictScalars, LinearMap.compr₂_apply, LinearMap.mul_apply', - Algebra.TensorProduct.tmul_mul_tmul, DistribMulActionHom.coe_toLinearMap, - NonUnitalAlgHom.coe_to_distribMulActionHom, NonUnitalAlgHom.coe_coe, AlgHom.comp_apply, - Algebra.TensorProduct.map_tmul, map_mul, Bialgebra.counitAlgHom_apply, - Algebra.TensorProduct.lmul'_apply_tmul, LinearMap.compl₁₂_apply] - rw [← mul_assoc, ← mul_assoc]; congr 1; - rw [mul_assoc, mul_assoc, mul_comm] - symm; rw [mul_comm] ; congr 1; rw [mul_comm] - -- This shows Δ (1 : A1 ⊗ A2) = (1 : (A1 ⊗ A2) ⊗ (A1 ⊗ A2)) - comul_one := by - rw [show (1 : A1 ⊗[R] A2) = (1 ⊗ₜ[R] 1) by rfl] - rw [show (1 : (A1 ⊗[R] A2) ⊗[R] A1 ⊗[R] A2) = (1 ⊗ₜ[R] 1) ⊗ₜ[R] (1 ⊗ₜ[R] 1) by rfl] - simp only [AlgHom.toNonUnitalAlgHom_eq_coe, NonUnitalAlgHom.toDistribMulActionHom_eq_coe, - LinearMap.comp_apply, TensorProduct.map_tmul, DistribMulActionHom.coe_toLinearMap, - NonUnitalAlgHom.coe_to_distribMulActionHom, NonUnitalAlgHom.coe_coe, map_one] - rw [show (1 : A1 ⊗[R] A1) = (1 ⊗ₜ[R] 1) by rfl] - rw [show (1 : A2 ⊗[R] A2) = (1 ⊗ₜ[R] 1) by rfl]; unfold Bialg_tensorequiv - simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, comp_apply, TensorProduct.assoc_symm_tmul, - LinearMap.rTensor_tmul, TensorProduct.assoc_tmul, LinearMap.lTensor_tmul, - TensorProduct.comm_tmul] - mul_compr₂_comul := mul_comp₂_tencomul R A1 A2 --- End of Prat III - --- Part IV is proving result from the TODO list like S is unique, an anti-homomorphism, etc. --- as well as the final big theorem: Points H L is a group! (for H be a commutative Hopf Algebra --- and L is a Commutative R-Algebra) - -/- α and β is the R-linear maps from H ⊗ H → H where α maps a ⊗ b to S(a*b) and β maps - a ⊗ b to S(b)*S(a), we show that the antipode S is an anti-homomorphism by showing - α = β -/ -abbrev α : LinPoints R (H ⊗[R] H) H := (antipode (R := R) (A := H)).comp (LinearMap.mul' R H) -abbrev β : LinPoints R (H ⊗[R] H) H := (LinearMap.mul' R H).comp - ((TensorProduct.map (antipode (A := H)) (antipode (A := H))).comp - (TensorProduct.comm R H H).toLinearMap) - -/- These instances are made by kevin in order to improve the speed of compiling my - codes since typechecking takes forever and obviously even after the improvements - it's still slow :( sorry I did my best-/ -instance : AddMonoidHomClass ((H ⊗[R] H) ⊗[R] H ⊗[R] H ≃ₗ[R] ((H ⊗[R] H) ⊗[R] H) ⊗[R] H) - ((H ⊗[R] H) ⊗[R] H ⊗[R] H) (((H ⊗[R] H) ⊗[R] H) ⊗[R] H) := - inferInstance - -instance : AddMonoidHomClass ((H ⊗[R] H) ⊗[R] H ⊗[R] H →ₗ[R] H ⊗[R] H) - ((H ⊗[R] H) ⊗[R] H ⊗[R] H) (H ⊗[R] H) := - inferInstance - -instance : AddMonoidHomClass (((H ⊗[R] H) ⊗[R] H) ⊗[R] H →ₗ[R] ((H ⊗[R] H) ⊗[R] H) ⊗[R] H) - (((H ⊗[R] H) ⊗[R] H) ⊗[R] H) (((H ⊗[R] H) ⊗[R] H) ⊗[R] H) := - inferInstance - -/- id_H * S = linone -/ -lemma mul_id_val : (antipode (A := H)) * LinearMap.id - = linone R H H := by - ext x ; unfold linone - simp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply] - have h0 := HopfAlgebra.mul_antipode_rTensor_comul (R := R) (A := H) - have h2 : (LinearMap.mul' R H ∘ₗ antipode.rTensor H ∘ₗ Coalgebra.comul) x - = (Algebra.linearMap R H ∘ₗ Coalgebra.counit) x := - congrFun (congrArg DFunLike.coe h0) x - simp only [LinearMap.comp_apply] at h2 ; exact h2 - -/- id_H * S = linone -/ -lemma id_mul_val : LinearMap.id * (antipode (R := R) (A := H)) - = linone R H H := by - ext x ; unfold linone ; simp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply] - have h1 := HopfAlgebra.mul_antipode_lTensor_comul (R := R) (A := H) - have h2 : (LinearMap.mul' R H ∘ₗ LinearMap.lTensor H antipode ∘ₗ Coalgebra.comul) x - = (Algebra.linearMap R H ∘ₗ Coalgebra.counit) x := - congrFun (congrArg DFunLike.coe h1) x - simp only [LinearMap.comp_apply] at h2 ; exact h2 - -/- S * id_H = id_H * S -/ -lemma idcomp : (antipode (R := R) (A := H)) * LinearMap.id = - LinearMap.id * (antipode (R := R) (A := H)):= by - rw [mul_id_val, id_mul_val] - ---Uniqueness -theorem anti_unique (T : LinPoints R H H): T * LinearMap.id = linone R H H ∧ - LinearMap.id * T = linone R H H → T = (antipode (A := H) : LinPoints R H H) := by - rintro ⟨h1, h2⟩ ; ext x ; symm - calc antipode (A := H) x = - ((antipode (R := R) (A := H)) * (linone R H H)) x := by rw [linmul_one] - _ = ((antipode (A := H) : LinPoints R H H) * - ((LinearMap.id (R := R) (M := H)) * T)) x := by rw [← h2] - _ = (((antipode (R := R) (A := H)) * (LinearMap.id (R := R) - (M := H))) * T) x := by rw [←lin_assoc] - _ = ((linone R H H) * T) x := by rw [mul_id_val R (H := H)] - _ = T x := by rw [linone_mul] - --- S(1) = 1 -lemma antione : (antipode (R := R) (A := H)) (1 : H) = 1 := by - have h0 : (LinearMap.mul' R H ∘ₗ (antipode.rTensor H) ∘ₗ Coalgebra.comul) 1 = 1 := by - rw [mul_antipode_rTensor_comul (R := R) (A := H), LinearMap.comp_apply, Bialgebra.counit_one, - Algebra.linearMap_apply, map_one] - simp at h0 ; rw [Algebra.TensorProduct.one_def] at h0 ; simp at h0 - exact h0 - --- linone is also algebra homomorphism -def linone_alg : Points R H H where - toFun := linone R H H - map_one' := by unfold linone ; simp - map_mul' := by intro x y; unfold linone; simp - map_zero' := LinearMap.map_zero (linone R H H) - map_add' := fun x y => LinearMap.map_add (linone R H H) x y - commutes' := by intro r; unfold linone; simp ; rfl - -lemma linoneval (h : H) : linone R H H h = linone_alg R h := by rfl - -/- This is showing α * m = linone where m is the multplication of H -/ -lemma αmul_eqone : (α R) * (LinearMap.mul' R H) = linone R (H ⊗[R] H) H := by - rw [linmul1]; ext a b - simp only [TensorProduct.AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, - LinearMap.coe_restrictScalars, LinearMap.comp_apply]; - have comuldef : Coalgebra.comul (R := R) (A:= H ⊗[R] H) = (Bialg_tensorequiv R H H).comp (TensorProduct.map - (Bialgebra.comulAlgHom R H) (Bialgebra.comulAlgHom R H)) := by rfl - rw [comuldef] ; simp only [AlgHom.toNonUnitalAlgHom_eq_coe, - NonUnitalAlgHom.toDistribMulActionHom_eq_coe, LinearMap.comp_apply, - TensorProduct.map_tmul, DistribMulActionHom.coe_toLinearMap, - NonUnitalAlgHom.coe_to_distribMulActionHom, NonUnitalAlgHom.coe_coe, - Bialgebra.comulAlgHom_apply] ; clear comuldef - obtain ⟨I1, a1, a2, ha⟩ := comul_repr R H a - obtain ⟨I2, b1, b2, hb⟩ := comul_repr R H b - rw [ha, hb]; unfold Bialg_tensorequiv - repeat rw [LinearMap.comp_apply] - dsimp only [LinearEquiv.coe_coe] ; rw [TensorProduct.tmul_sum]; rw [map_sum] - simp_rw [TensorProduct.sum_tmul]; simp_rw [map_sum] - simp only [TensorProduct.assoc_symm_tmul, LinearMap.rTensor_tmul, LinearMap.coe_comp, - LinearEquiv.coe_coe, comp_apply, TensorProduct.assoc_tmul, LinearMap.lTensor_tmul, - TensorProduct.comm_tmul, TensorProduct.map_tmul, LinearMap.mul'_apply] - symm; unfold linone - have tencounit : Coalgebra.counit (R := R) (A := H ⊗[R] H) = - (Algebra.TensorProduct.lmul' R (S := R)).comp (Algebra.TensorProduct.map - (Bialgebra.counitAlgHom R H) (Bialgebra.counitAlgHom R H)) := rfl - rw [tencounit] ; simp only [AlgHom.toNonUnitalAlgHom_eq_coe, - NonUnitalAlgHom.toDistribMulActionHom_eq_coe, LinearMap.coe_comp, - DistribMulActionHom.coe_toLinearMap, NonUnitalAlgHom.coe_to_distribMulActionHom, - NonUnitalAlgHom.coe_coe, AlgHom.coe_comp, comp_apply, Algebra.TensorProduct.map_tmul, - Bialgebra.counitAlgHom_apply, Algebra.TensorProduct.lmul'_apply_tmul, - AlgHom.toLinearMap_apply, map_mul] ; clear tencounit - rw [onedef R a, onedef R b, linoneval, linoneval] - rw [← map_mul, ← linoneval, ← mul_id_val, linmul1]; simp only [LinearMap.comp_apply, - Bialgebra.comul_mul] - rw [ha, hb]; rw [Finset.sum_mul_sum]; repeat rw [map_sum] - simp_rw [Algebra.TensorProduct.tmul_mul_tmul]; simp_rw [map_sum] - simp only [TensorProduct.map_tmul, LinearMap.id_coe, id_eq, LinearMap.mul'_apply] - exact Finset.sum_comm - -/- This is a sweedler notation for one (or linone, their value are the same) : - one(b) = ∑ i b1 i * S(b2 i) (actually = ∑ i S(b1 i) * b2 i as well, but that's - secretly included in the previous lemma) -/ -lemma sum_idS_eqone (I2: Finset (H ⊗[R] H)) (b1 b2 : H ⊗[R] H → H) (b : H) - (hb: Coalgebra.comul b = ∑ i in I2, b1 i ⊗ₜ[R] b2 i) : - ∑ i in I2, b1 i * (antipode (R := R) (A := H)) (b2 i) = linone R H H b := by - symm ; rw [← id_mul_val, linmul1, LinearMap.comp_apply, LinearMap.comp_apply, hb] - simp only [map_sum, TensorProduct.map_tmul, LinearMap.id_coe, id_eq, - LinearMap.mul'_apply] - -/- This is m * β = linone, now we have all the ingredient -/ -lemma mulβ_eqone : (LinearMap.mul' R H) * (β R) = linone R (H ⊗[R] H) H:= by - rw [linmul1]; ext a b - simp only [TensorProduct.AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, - LinearMap.coe_restrictScalars, LinearMap.coe_comp, comp_apply] - change (LinearMap.mul' R H) ((TensorProduct.map (LinearMap.mul' R H) (β R)) - ((Bialg_tensorequiv R H H).comp (TensorProduct.map - (Bialgebra.comulAlgHom R H) (Bialgebra.comulAlgHom R H)) (a ⊗ₜ[R] b))) = - (linone R (H ⊗[R] H) H) (a ⊗ₜ[R] b) - unfold Bialg_tensorequiv; simp only [AlgHom.toNonUnitalAlgHom_eq_coe, - NonUnitalAlgHom.toDistribMulActionHom_eq_coe, LinearMap.coe_comp, LinearEquiv.coe_coe, - comp_apply, TensorProduct.map_tmul, DistribMulActionHom.coe_toLinearMap, - NonUnitalAlgHom.coe_to_distribMulActionHom, NonUnitalAlgHom.coe_coe, - Bialgebra.comulAlgHom_apply] - repeat rw [LinearMap.comp_apply] - obtain ⟨I1, a1, a2, ha⟩ := comul_repr R H a - obtain ⟨I2, b1, b2, hb⟩ := comul_repr R H b - rw [ha, hb]; repeat rw [LinearMap.comp_apply] - rw [TensorProduct.tmul_sum]; repeat rw [map_sum] - simp_rw [TensorProduct.sum_tmul]; simp_rw [map_sum] - simp only [TensorProduct.assoc_symm_tmul, LinearMap.rTensor_tmul, LinearMap.coe_comp, - LinearEquiv.coe_coe, comp_apply, TensorProduct.assoc_tmul, LinearMap.lTensor_tmul, - TensorProduct.comm_tmul, TensorProduct.map_tmul, LinearMap.mul'_apply] - symm ; unfold linone ; rw [LinearMap.comp_apply] - change (AlgHom.toLinearMap (Algebra.ofId R H)) ( - (Algebra.TensorProduct.lmul' R (S := R)).comp (Algebra.TensorProduct.map - (Bialgebra.counitAlgHom R H) (Bialgebra.counitAlgHom R H)) (a ⊗ₜ[R] b)) = - ∑ x in I2, ∑ x_1 in I1, - a1 x_1 * b1 x * ((antipode (R :=R) (A := H)) (b2 x) * (antipode (R := R) (A := H)) (a2 x_1)) - simp only [AlgHom.comp_apply, Algebra.TensorProduct.map_tmul, Bialgebra.counitAlgHom_apply, - Algebra.TensorProduct.lmul'_apply_tmul, AlgHom.toLinearMap_apply, map_mul] - symm ; simp_rw [mul_assoc] ; rw [Finset.sum_comm] ; simp_rw [← Finset.mul_sum] - simp_rw [← mul_assoc] ; simp_rw [← Finset.sum_mul] - rw [sum_idS_eqone R I2 b1 b2 b hb] ; rw [linone', LinearMap.comp_apply] - rw [← mul_one (Coalgebra.counit b), ← Algebra.id.smul_eq_mul] - rw [map_smul (AlgHom.toLinearMap (Algebra.ofId R H)) (Coalgebra.counit b) (1 : R)] - simp only [AlgHom.toLinearMap_apply, map_one, Algebra.smul_mul_assoc, one_mul, - Algebra.mul_smul_comm, smul_eq_mul, mul_one] ; simp_rw [← Finset.smul_sum] - rw [sum_idS_eqone R I1 a1 a2 a ha] ; rw [← mul_one (Coalgebra.counit b)] - rw [← Algebra.id.smul_eq_mul, map_smul (Algebra.ofId R H) (Coalgebra.counit b) (1 : R)] - rw [linone'] ; simp only [smul_eq_mul, mul_one, LinearMap.coe_comp, comp_apply, - AlgHom.toLinearMap_apply, map_one, Algebra.mul_smul_comm] - -/- This theorem is done by calculation which is : - α = α * one = α * (m * β) = (α * m) * β = one * β = β -/ -theorem αβ_eq : α R (H := H) = β R := by - ext x1 x2 ; simp only [TensorProduct.AlgebraTensorModule.curry_apply, - TensorProduct.curry_apply, LinearMap.coe_restrictScalars] - calc _ - (α R) (x1 ⊗ₜ[R] x2) = ((α R (H := H)) * - (linone R (H ⊗[R] H) H)) (x1 ⊗ₜ[R] x2) := by rw [linmul_one] - _ = ((α R (H := H)) * ((LinearMap.mul' R H) * - (β R (H := H)))) (x1 ⊗ₜ[R] x2) := by rw [← mulβ_eqone] - _ = ((α R (H := H)) * (LinearMap.mul' R H) * - (β R (H := H))) (x1 ⊗ₜ[R] x2) := by rw [mul_assoc] - _ = (linone R (H ⊗[R] H) H * (β R (H := H))) (x1 ⊗ₜ[R] x2) := by rw [αmul_eqone] - _ = (β R (H := H)) (x1 ⊗ₜ[R] x2) := by rw [linone_mul] - -/- S(a * b) = S(b) * S(a), S is an antihomomorphism -/ -theorem antihom (h l : H) : (antipode (R := R) (A := H)) (h * l) = - (antipode (R := R) (A := H)) l * (antipode (R := R) (A := H)) h := by - calc _ - (antipode (R := R) (A := H)) (h * l) = - ((antipode (R := R) (A := H)).comp (LinearMap.mul' R H)) (h ⊗ₜ[R] l) := by rfl - _ = α R (H := H) (h ⊗ₜ[R] l) := by rfl - _ = β R (H := H) (h ⊗ₜ[R] l) := by rw [αβ_eq] - _ = (LinearMap.mul' R H).comp - ((TensorProduct.map (antipode (A := H)) (antipode (A := H))).comp - (TensorProduct.comm R H H).toLinearMap) (h ⊗ₜ[R] l):= by rfl - _ = (antipode (R := R) (A := H)) l * (antipode (R := R) (A := H)) h := by - simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, comp_apply, - TensorProduct.comm_tmul, TensorProduct.map_tmul, LinearMap.mul'_apply] - -/- S is an algebra homomorphism under the assumption of S being commutative -/ -lemma antipodemul (h l: H): (antipode (R := R) (A := H)) (h*l) = - (antipode (R := R) (A := H)) h * (antipode (R := R) (A := H)) l := by - rw [antihom, mul_comm] - -lemma antipode_commute(r : R): (antipode (R := R) (A := H)) ((algebraMap R H) r) = - (algebraMap R H) r := by - rw [Algebra.algebraMap_eq_smul_one, LinearMap.map_smul, antione] - -def S : Points R H H where - toFun := (antipode (R := R) (A := H)) - map_one' := antione R - map_mul' := by simp only; intro x y; exact antipodemul R x y - map_zero' := (antipode (R := R) (A := H)).map_zero - map_add' := by simp - commutes' := antipode_commute R - -lemma Antival (h : H) : S R h = (antipode (R := R) (A := H)) h := by rfl - --- Define the inverse of elements in Points to be ∀ f ∈ Points, f⁻¹ = (S ∘ f) -def inv (f : Points R H L) : Points R H L := f.comp (S R) -instance : Inv (Points R H L) := ⟨inv R L⟩ -lemma invval (f : Points R H L) : f⁻¹ = f.comp (S R) := rfl - -lemma tensordecomp (f : Points R H L) : Algebra.TensorProduct.map (AlgHom.comp f - (S R)) f = (Algebra.TensorProduct.map f f).comp (Algebra.TensorProduct.map (S R) - (AlgHom.id R H)) := by - ext x - · rw [Algebra.TensorProduct.map_comp_includeLeft] - repeat rw [AlgHom.comp_apply] - repeat rw [Algebra.TensorProduct.includeLeft_apply] - rw [Algebra.TensorProduct.map_tmul, map_one] - simp only [Algebra.TensorProduct.map_tmul, map_one] - · repeat rw [AlgHom.comp_apply] - simp only [Algebra.TensorProduct.includeRight_apply, AlgHom.coe_restrictScalars', - Algebra.TensorProduct.map_tmul, map_one, AlgHom.comp_apply, AlgHom.coe_id, id_eq] - - -lemma lemmainv3 (ψ: Points R H L): AlgHom.comp (Algebra.TensorProduct.lmul' R) - (AlgHom.comp (Algebra.TensorProduct.map ψ ψ) - (Algebra.TensorProduct.map (S R) (AlgHom.id R H))) = - AlgHom.comp ψ (AlgHom.comp (Algebra.TensorProduct.lmul' R) - (Algebra.TensorProduct.map (S R) (AlgHom.id R H))) := by - ext x <;> simp - -lemma lemmainv4 (ψ: Points R H L): AlgHom.comp (AlgHom.comp - (Algebra.TensorProduct.lmul' R) - (Algebra.TensorProduct.map (S R) (AlgHom.id R H))) (Bialgebra.comulAlgHom R H) = - linone_alg R := by - ext h ; rw [← linoneval R (H := H) h, ← mul_id_val, linmul1, LinearMap.comp_apply, - LinearMap.comp_apply] - simp only [AlgHom.comp_apply, Bialgebra.comulAlgHom_apply] - obtain ⟨I1, h1, h2, h0⟩ := comul_repr R H h - simp only [h0, map_sum, map_smul, Algebra.TensorProduct.map_tmul, AlgHom.coe_id, - id_eq, Algebra.TensorProduct.lmul'_apply_tmul, TensorProduct.map_tmul, LinearMap.id_coe, - LinearMap.mul'_apply] - refine Finset.sum_congr rfl fun _ _ ↦ rfl - -lemma Algoneval : linone_alg R = one (R := R) (A := H) (L := H) := by rfl - -/- f ∘ one = one -/ -lemma compone_eq_one (f : Points R H L): f.comp one = (one : Points R H L) := by - ext x; rw [AlgHom.comp_apply] - have h0 := f.commutes - unfold one; rw [AlgHom.comp_apply, AlgHom.comp_apply, Bialgebra.counitAlgHom_apply] - exact h0 (Coalgebra.counit x) - -/- f⁻¹ * f = one -/ -lemma leftinv(f: Points R H L) : f⁻¹ * f = one := by - rw [hmul1, invval, oneval, tensordecomp, ← AlgHom.comp_assoc, lemmainv3, - AlgHom.comp_assoc , lemmainv4 R H, Algoneval, compone_eq_one, ← oneval] - exact S R - -instance : Group (Points R H L) where - mul := mul (R := R) (A := H) (L := L) - mul_assoc := Pointmul_assoc - one := one - one_mul := Pointone_mul - mul_one := Pointmul_one - inv := inv R L - mul_left_inv := leftinv R L - -instance: Group (Points R H H) := inferInstance - -/- Since the inverse in a group is unique, S⁻¹ must equal id !-/ -lemma anti_inverseunique: (S R (H := H))⁻¹ = AlgHom.id R H := by - rw [inv_eq_iff_mul_eq_one] - exact mul_eq_one_iff_eq_inv.mpr rfl - -/- Since S² also satisfies S² * S is also one, by the uniqueness of inverse - S² must be equal to id -/ -lemma antisquare_is_id: (S R (H := H)).comp (S R (H := H)) = AlgHom.id R H := by - rw [← anti_inverseunique] - exact rfl - -/- If H is commutative, S is a bijection (Co-commutative should work as well, - but I got tired :)) -/ -lemma anti_bijection: Bijective (S R (H := H)) := by - constructor - · intro x y h ; rw [← id_eq x, ← id_eq y, ← AlgHom.coe_id R, ← antisquare_is_id, - AlgHom.comp_apply, h]; rfl - · intro x ; use (S R (H := H)) x - refine by rw [← AlgHom.comp_apply, antisquare_is_id] ; rfl - --- Thanks for reading! I know it's long and takes long time to compile :(, hope you found our --- work intersting ! :)) -end -end HopfPoints diff --git a/FLT/for_mathlib/Coalgebra/Monoid.lean b/FLT/for_mathlib/Coalgebra/Monoid.lean new file mode 100644 index 00000000..74aad359 --- /dev/null +++ b/FLT/for_mathlib/Coalgebra/Monoid.lean @@ -0,0 +1,218 @@ +/- +Copyright (c) 2024 Yunzhou Xie. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yunzhou Xie, Yichen Feng, Yanqiao Zhou, Jujian Zhang +-/ + +import Mathlib.RingTheory.TensorProduct +import FLT.for_mathlib.Coalgebra.Sweedler +import Mathlib.RingTheory.HopfAlgebra + +/-! +# Monoid structure on linear maps and algebra homomorphism + +Let `A` be an `R`-coalgebra and `L` and `R`-algebra, then the set of `R`-linear maps `Hom(A, L)` +can be endowed a monoid structure where +- unit is defined as `A -counit-> R -algebraMap-> L` +- multiplication is defined as `A -comul-> A ⊗ A -f ⊗ g-> L ⊗ L -multiplication-> L` for any linear + maps `f` and `g`. + +Since `comul x = ∑ x ⊗ y` implies `(f * g) x = ∑ f(x) g(y)`, this multiplication is often called +convolution. + +If furter `A` is an `R`-bialgebra, then the set of `R`-agelrab homomorphism `Hom(A, L)` can also +be endowed with a monoid structure where multiplication is convolution and unit is the same in the +linear case. + +## References +* +* Christian Kassel "Quantum Groups" (Springer GTM), around Prop III.3.1, Theorem III.3.4 etc. +* Dr.Adrian de Jesus Celestino Rodriguez "Cumulants in Non-commutative Probability via Hopf + Algebras", 2022 +-/ + +open TensorProduct BigOperators LinearMap + +section Coalgebra + +/-- +A linear point is a linear map from `A` to `L` where `A` is an `R`-colagebra and `L` an `R`-algebra. +We introduce this abbreviation is to prevent instance clashing when we put a monnoid structure on +these linear points with convolution product. + +The confusion arise when we consider automorphism, for example `A →ₗ[R] A` already has a `mul` by +composition. +-/ +abbrev LinearPoint (R A L : Type*) + [CommSemiring R] [AddCommMonoid A] [Module R A] + [AddCommMonoid L] [Module R L] := + A →ₗ[R] L + +namespace LinearPoint + +variable {R A L : Type*} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] +variable [Semiring L] [Algebra R L] + +instance : FunLike (LinearPoint R A L) A L := + inferInstanceAs <| FunLike (A →ₗ[R] L) A L + +instance : LinearMapClass (LinearPoint R A L) R A L := + inferInstanceAs <| LinearMapClass (A →ₗ[R] L) R A L + +variable (φ ψ χ : LinearPoint R A L) + +/-- +`A -comul-> A ⊗ A -φ ⊗ ψ-> L ⊗ L -mul> L` is convolution product of `φ` and `ψ`. +If `comul x = ∑ aᵢ ⊗ bᵢ`, then `(φ ⋆ ψ)(x) = ∑ φ(aᵢ) × ψ(bᵢ)`, hence the name convolution. +-/ +noncomputable def mul : LinearPoint R A L := + LinearMap.mul' _ _ ∘ₗ TensorProduct.map φ ψ ∘ₗ Coalgebra.comul + +lemma mul_repr' {ι : Type* } (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A) + (repr : Coalgebra.comul (R := R) a = ∑ i in ℐ, Δ₁ i ⊗ₜ Δ₂ i) : + φ.mul ψ a = ∑ i in ℐ, φ (Δ₁ i) * ψ (Δ₂ i) := by + simp only [mul, comp_apply, repr, map_sum, map_tmul, mul'_apply] + +/-- +`A -counit-> R -algebraMap-> L` is the unit with respect to convolution product. +-/ +def one : LinearPoint R A L := + Algebra.linearMap R L ∘ₗ Coalgebra.counit + +instance : One (LinearPoint R A L) where + one := one + +lemma one_def : (1 : LinearPoint R A L) = Algebra.linearMap R L ∘ₗ Coalgebra.counit := rfl + +noncomputable instance : Mul (LinearPoint R A L) where + mul := mul + +lemma mul_repr {ι : Type* } (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A) + (repr : Coalgebra.comul (R := R) a = ∑ i in ℐ, Δ₁ i ⊗ₜ Δ₂ i) : + (φ * ψ) a = ∑ i in ℐ, φ (Δ₁ i) * ψ (Δ₂ i) := + mul_repr' _ _ a ℐ Δ₁ Δ₂ repr + +lemma mul_assoc' : φ * ψ * χ = φ * (ψ * χ) := LinearMap.ext fun x ↦ by + simp only [show + (φ * ψ) * χ = + LinearMap.mul' _ _ ∘ₗ + (LinearMap.mul' _ _).rTensor _ ∘ₗ + (map (map _ _) _) ∘ₗ Coalgebra.comul.rTensor _ ∘ₗ Coalgebra.comul + by simp only [← comp_assoc, map_comp_rTensor, rTensor_comp_map]; rfl, + mul', comp_apply, Coalgebra.comul_repr, map_sum, rTensor_tmul, sum_tmul, map_tmul, lift.tmul, + mul_apply', mul_assoc, + show + φ * (ψ * χ) = + LinearMap.mul' _ _ ∘ₗ + (LinearMap.mul' _ _).lTensor _ ∘ₗ + (map _ (map _ _)) ∘ₗ Coalgebra.comul.lTensor _ ∘ₗ Coalgebra.comul + by simp only [← comp_assoc, map_comp_lTensor, lTensor_comp_map]; rfl, + ← Coalgebra.coassoc, LinearEquiv.coe_coe, assoc_tmul, lTensor_tmul] + +lemma mul_one' : φ * 1 = φ := show mul φ one = φ from LinearMap.ext fun _ ↦ by + simp [show φ.mul one = + LinearMap.mul' _ _ ∘ₗ φ.rTensor _ ∘ₗ (Algebra.linearMap _ _).lTensor _ ∘ₗ + Coalgebra.counit.lTensor _ ∘ₗ Coalgebra.comul by + delta one mul + simp [← comp_assoc, ← map_comp, comp_id, id_comp]] + +lemma one_mul' : 1 * φ = φ := show mul one φ = φ from LinearMap.ext fun _ ↦ by + simp [show one.mul φ = + LinearMap.mul' _ _ ∘ₗ φ.lTensor _ ∘ₗ (Algebra.linearMap _ _).rTensor _ ∘ₗ + Coalgebra.counit.rTensor _ ∘ₗ Coalgebra.comul by + delta one mul + simp [← comp_assoc, ← map_comp, comp_id, id_comp]] + +noncomputable instance instMonoid : Monoid (LinearPoint R A L) where + mul_assoc := mul_assoc' + one_mul := one_mul' + mul_one := mul_one' + +attribute [deprecated] mul_assoc' mul_one' one_mul' mul_repr' + +end LinearPoint + +end Coalgebra + +section Bialgebra + +/-- +An algebra homomorphism point is an algebra homorphism from `A` to `L` where `A` is an `R`-biagebra +and `L` an `R`-algebra. We introduce this abbreviation is to prevent instance clashing when we put a +monnoid structure on these algebra homomorphism points with convolution product. + +This confusion happens when `A` and `L` are the same where default multiplication is composition. +-/ +abbrev AlgHomPoint (R A L : Type*) [CommSemiring R] [Semiring A] [Bialgebra R A] + [CommSemiring L] [Algebra R L] := + A →ₐ[R] L + +namespace AlgHomPoint + +variable {R A L : Type*} [CommSemiring R] [Semiring A] [Bialgebra R A] +variable [CommSemiring L] [Algebra R L] + +variable (φ ψ χ : AlgHomPoint R A L) + +/-- +An algebra homomorphism is also a linear map +-/ +abbrev toLinearPoint : LinearPoint R A L := φ.toLinearMap + +/-- +`A -comul-> A ⊗ A -φ ⊗ ψ-> L ⊗ L -mul> L` is convolution product of `φ` and `ψ`. +If `comul x = ∑ aᵢ ⊗ bᵢ`, then `(φ ⋆ ψ)(x) = ∑ φ(aᵢ) × ψ(bᵢ)`, hence the name convolution. +-/ +noncomputable def mul : AlgHomPoint R A L := + Algebra.TensorProduct.lmul' R (S := L) |>.comp <| + Algebra.TensorProduct.map φ ψ |>.comp <| Bialgebra.comulAlgHom R A +/-- +`A -counit-> R -algebraMap-> L` is the unit with respect to convolution product. +-/ +noncomputable def one : AlgHomPoint R A L := + Algebra.ofId R L |>.comp <| Bialgebra.counitAlgHom R A + +noncomputable instance : One (AlgHomPoint R A L) where + one := one + +lemma one_def : (1 : AlgHomPoint R A L) = (Algebra.ofId R L).comp (Bialgebra.counitAlgHom R A) := + rfl + +noncomputable instance : Mul (AlgHomPoint R A L) where + mul := mul + +lemma mul_assoc' : φ * ψ * χ = φ * (ψ * χ) := by + ext + exact congr($(mul_assoc φ.toLinearPoint ψ.toLinearPoint χ.toLinearPoint) _) + +lemma mul_one' : φ * 1 = φ := by + ext; exact congr($(mul_one φ.toLinearPoint) _) + +lemma one_mul' : 1 * φ = φ := show mul one φ = φ by + ext; exact congr($(one_mul φ.toLinearPoint) _) + +noncomputable instance instMonoid : Monoid (AlgHomPoint R A L) where + mul_assoc := mul_assoc' + one_mul := one_mul' + mul_one := mul_one' + +lemma mul_repr {ι : Type* } (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A) + (repr : Coalgebra.comul (R := R) a = ∑ i in ℐ, Δ₁ i ⊗ₜ Δ₂ i) : + (φ * ψ) a = ∑ i in ℐ, φ (Δ₁ i) * ψ (Δ₂ i) := + LinearPoint.mul_repr _ _ a ℐ Δ₁ Δ₂ repr + +attribute [deprecated] mul_assoc' mul_one' one_mul' + +section commutative_bialgebra + +variable {A' : Type*} [CommSemiring A'] [Bialgebra R A'] + +lemma comp_one {A' : Type*} [CommSemiring A'] [Bialgebra R A'] + (f : AlgHomPoint R A' L) : + f.comp (1 : AlgHomPoint R A' A') = 1 := by + ext + simp [one_def, Algebra.ofId_apply, Algebra.algebraMap_eq_smul_one, f.map_smul, f.map_one] + +end commutative_bialgebra + +end AlgHomPoint diff --git a/FLT/for_mathlib/Coalgebra/Sweedler.lean b/FLT/for_mathlib/Coalgebra/Sweedler.lean new file mode 100644 index 00000000..992d449e --- /dev/null +++ b/FLT/for_mathlib/Coalgebra/Sweedler.lean @@ -0,0 +1,64 @@ +/- +Copyright (c) 2024 Yunzhou Xie. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yunzhou Xie, Yichen Feng, Yanqiao Zhou, Jujian Zhang +-/ + +import Mathlib.RingTheory.Bialgebra + +set_option autoImplicit false + +open BigOperators TensorProduct + +namespace Coalgebra + +variable {R A : Type*} [CommSemiring R] +variable [AddCommMonoid A] [Module R A] [Coalgebra R A] + +lemma exists_repr (x : A) : + ∃ (I : Finset (A ⊗[R] A)) (x1 : A ⊗[R] A → A) (x2 : A ⊗[R] A → A), + Coalgebra.comul (R := R) x = ∑ i in I, x1 i ⊗ₜ[R] x2 i := by + classical + have mem1 : comul x ∈ (⊤ : Submodule R (A ⊗[R] A)) := ⟨⟩ + rw [← TensorProduct.span_tmul_eq_top, mem_span_set] at mem1 + obtain ⟨r, hr, (eq1 : ∑ i in r.support, (_ • _) = _)⟩ := mem1 + choose a a' haa' using hr + replace eq1 := calc _ + comul x = ∑ i in r.support, r i • i := eq1.symm + _ = ∑ i in r.support.attach, (r i : R) • i.1 := Finset.sum_attach _ _ |>.symm + _ = ∑ i in r.support.attach, (r i • a i.2 ⊗ₜ[R] a' i.2) := + Finset.sum_congr rfl fun i _ ↦ congr(r i.1 • $(haa' i.2)).symm + _ = ∑ i in r.support.attach, ((r i • a i.2) ⊗ₜ[R] a' i.2) := + Finset.sum_congr rfl fun i _ ↦ TensorProduct.smul_tmul' _ _ _ + refine ⟨r.support, fun i ↦ if h : i ∈ r.support then r i • a h else 0, + fun i ↦ if h : i ∈ r.support then a' h else 0, eq1 ▸ ?_⟩ + conv_rhs => rw [← Finset.sum_attach] + exact Finset.sum_congr rfl fun _ _ ↦ (by aesop) + + +/-- an arbitrarily chosen indexing set for comul(a) = ∑ a₁ ⊗ a₂. -/ +noncomputable def ℐ (a : A) : Finset (A ⊗[R] A) := exists_repr a |>.choose + +/-- an arbitrarily chosen first coordinate for comul(a) = ∑ a₁ ⊗ a₂. -/ +noncomputable def Δ₁ (a : A) : A ⊗[R] A → A := exists_repr a |>.choose_spec.choose + +/-- an arbitrarily chosen second coordinate for comul(a) = ∑ a₁ ⊗ a₂. -/ +noncomputable def Δ₂ (a : A) : A ⊗[R] A → A := + exists_repr a |>.choose_spec.choose_spec.choose + +lemma comul_repr (a : A) : + Coalgebra.comul a = ∑ i in ℐ a, Δ₁ a i ⊗ₜ[R] Δ₂ (R := R) a i := + exists_repr a |>.choose_spec.choose_spec.choose_spec + +lemma sum_counit_tmul (a : A) {ι : Type*} (s : Finset ι) (x y : ι → A) + (repr : comul a = ∑ i in s, x i ⊗ₜ[R] y i) : + ∑ i in s, counit (R := R) (x i) ⊗ₜ y i = 1 ⊗ₜ[R] a := by + simpa [repr, map_sum] using congr($(rTensor_counit_comp_comul (R := R) (A := A)) a) + + +lemma sum_tmul_counit (a : A) {ι : Type*} (s : Finset ι) (x y : ι → A) + (repr : comul a = ∑ i in s, x i ⊗ₜ[R] y i) : + ∑ i in s, (x i) ⊗ₜ counit (R := R) (y i) = a ⊗ₜ[R] 1 := by + simpa [repr, map_sum] using congr($(lTensor_counit_comp_comul (R := R) (A := A)) a) + +end Coalgebra diff --git a/FLT/for_mathlib/Coalgebra/TensorProduct.lean b/FLT/for_mathlib/Coalgebra/TensorProduct.lean new file mode 100644 index 00000000..9b71e545 --- /dev/null +++ b/FLT/for_mathlib/Coalgebra/TensorProduct.lean @@ -0,0 +1,136 @@ +/- +Copyright (c) 2024 Yunzhou Xie. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yunzhou Xie, Yichen Feng, Yanqiao Zhou, Jujian Zhang +-/ + +import Mathlib.RingTheory.TensorProduct +import Mathlib.RingTheory.Bialgebra +import FLT.for_mathlib.Coalgebra.Sweedler + +/-! +# Tensor Product of Coalgebras + +Suppose `A, B` are `R`-coalgebras, then `A ⊗ B` has a natural `R`-coalgebra strucutre +induced by those of `A` and `B`. + +-/ + +open TensorProduct BigOperators + +namespace Coalgebra + +variable (R A B : Type*) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] +variable [AddCommMonoid B] [Module R B] [Coalgebra R B] + +set_option maxHeartbeats 500000 in +noncomputable instance : Coalgebra R (A ⊗[R] B) := +let e : (A ⊗[R] B) ⊗[R] (A ⊗[R] B) ⊗[R] A ⊗[R] B ≃ₗ[R] (A ⊗[R] A ⊗[R] A) ⊗[R] B ⊗[R] B ⊗[R] B := + congr (.refl R _) (tensorTensorTensorComm R _ _ _ _) ≪≫ₗ tensorTensorTensorComm R _ _ _ _ +{ comul := tensorTensorTensorComm R A A B B ∘ₗ map comul comul + counit := TensorProduct.lid R R ∘ₗ map counit counit + coassoc := by + convert congr_arg e.symm.toLinearMap.comp + congr(TensorProduct.map $(coassoc (R := R) (A := A)) $(coassoc (R := R) (A := B))) <;> + ext <;> + simpa [comul_repr, tmul_sum, sum_tmul, map_sum] using + Finset.sum_congr rfl fun _ _ ↦ Finset.sum_comm + rTensor_counit_comp_comul := by + have EQ := congr_arg ((TensorProduct.assoc R R A B).toLinearMap ∘ₗ + ((TensorProduct.lid R B).toLinearMap.lTensor _)).comp + congr(TensorProduct.map + $(rTensor_counit_comp_comul (R := R) (A := A)) + $(rTensor_counit_comp_comul (R := R) (A := B))) + convert EQ <;> + ext <;> + simp [comul_repr, tmul_sum, sum_tmul, map_sum, tmul_smul, Finset.smul_sum, smul_tmul', mul_comm] + lTensor_counit_comp_comul := by + have EQ := + congr_arg ((TensorProduct.assoc R A B R).symm.toLinearMap ∘ₗ + (TensorProduct.rid R A).toLinearMap.rTensor _).comp + congr(TensorProduct.map + $(lTensor_counit_comp_comul (R := R) (A := A)) + $(lTensor_counit_comp_comul (R := R) (A := B))) + convert EQ <;> + ext <;> + simp [comul_repr, tmul_sum, sum_tmul, map_sum, Finset.smul_sum, smul_tmul', smul_tmul, + mul_comm] } + +lemma TensorProduct.comul_def : + Coalgebra.comul (R := R) (A := A ⊗[R] B) = + tensorTensorTensorComm R A A B B ∘ₗ map comul comul := + rfl + +lemma TensorProduct.counit_def : + Coalgebra.counit (R := R) (A := A ⊗[R] B) = TensorProduct.lid R R ∘ₗ map counit counit := + rfl + +variable {R A B} + +lemma TensorProduct.comul_apply_repr (a : A) (b : B) {ιA ιB : Type*} + (sA : Finset ιA) (sB : Finset ιB) + (xA yA : ιA → A) (repr_a : comul a = ∑ i in sA, xA i ⊗ₜ[R] yA i) + (xB yB : ιB → B) (repr_b : comul b = ∑ i in sB, xB i ⊗ₜ[R] yB i) : + comul (a ⊗ₜ[R] b) = ∑ i in sA, ∑ j in sB, (xA i ⊗ₜ xB j) ⊗ₜ[R] (yA i ⊗ₜ yB j) := by + simpa [TensorProduct.comul_def, repr_a, repr_b, map_sum, sum_tmul, tmul_sum] using Finset.sum_comm + +lemma TensorProduct.comul_apply_repr' (a : A) (b : B) {ιA ιB : Type*} + (sA : Finset ιA) (sB : Finset ιB) + (xA yA : ιA → A) (repr_a : comul a = ∑ i in sA, xA i ⊗ₜ[R] yA i) + (xB yB : ιB → B) (repr_b : comul b = ∑ i in sB, xB i ⊗ₜ[R] yB i) : + comul (a ⊗ₜ[R] b) = ∑ j in sB, ∑ i in sA, (xA i ⊗ₜ xB j) ⊗ₜ[R] (yA i ⊗ₜ yB j) := by + simp [TensorProduct.comul_def, repr_a, repr_b, map_sum, sum_tmul, tmul_sum] + +lemma TensorProduct.comul_apply_repr'' (a : A) (b : B) {ιA ιB : Type*} + (sA : Finset ιA) (sB : Finset ιB) + (xA yA : ιA → A) (repr_a : comul a = ∑ i in sA, xA i ⊗ₜ[R] yA i) + (xB yB : ιB → B) (repr_b : comul b = ∑ i in sB, xB i ⊗ₜ[R] yB i) : + comul (a ⊗ₜ[R] b) = ∑ i in sA ×ˢ sB, (xA i.1 ⊗ₜ xB i.2) ⊗ₜ[R] (yA i.1 ⊗ₜ yB i.2) := by + rw [TensorProduct.comul_apply_repr (repr_a := repr_a) (repr_b := repr_b), Finset.sum_product] + +end Coalgebra + +namespace Bialgebra + +variable (R A B : Type*) [CommSemiring R] +variable [Semiring A] [Bialgebra R A] +variable [Semiring B] [Bialgebra R B] + +noncomputable instance : Bialgebra R (A ⊗[R] B) where + counit_one := by simp [show (1 : A ⊗[R] B) = 1 ⊗ₜ 1 from rfl, Coalgebra.TensorProduct.counit_def] + mul_compr₂_counit := by + ext + simp only [Coalgebra.TensorProduct.counit_def, AlgebraTensorModule.curry_apply, curry_apply, + LinearMap.coe_restrictScalars, LinearMap.compr₂_apply, LinearMap.mul_apply', + Algebra.TensorProduct.tmul_mul_tmul, LinearMap.coe_comp, LinearEquiv.coe_coe, + Function.comp_apply, map_tmul, counit_mul, lid_tmul, smul_eq_mul, LinearMap.compl₁₂_apply] + ring + comul_one := by + rw [show (1 : A ⊗[R] B) = 1 ⊗ₜ 1 from rfl, Coalgebra.TensorProduct.comul_def, + LinearMap.comp_apply, map_tmul, comul_one, comul_one] + rfl + mul_compr₂_comul := by + let e : (A →ₗ[R] A ⊗[R] A) ⊗[R] (B →ₗ[R] B ⊗[R] B) →ₗ[R] + A ⊗[R] B →ₗ[R] (A ⊗[R] B) ⊗[R] A ⊗[R] B := + (tensorTensorTensorComm R A A B B).toLinearMap.compRight ∘ₗ homTensorHomMap _ _ _ _ _ + + convert congr_arg e.comp + congr(map $(mul_compr₂_comul (R := R) (A := A)) $(mul_compr₂_comul (R := R) (A := B))) + · ext a b a' b' + simpa only [AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars, + LinearMap.compr₂_apply, LinearMap.mul_apply', Algebra.TensorProduct.tmul_mul_tmul, + LinearMap.coe_comp, Function.comp_apply, map_tmul, homTensorHomMap_apply, + LinearMap.compRight_apply, LinearEquiv.coe_coe, Coalgebra.comul_repr (a := a * a'), + Coalgebra.comul_repr (a := b * b'), tmul_sum, sum_tmul, map_sum, + tensorTensorTensorComm_tmul, e] using Coalgebra.TensorProduct.comul_apply_repr' + (repr_a := Coalgebra.comul_repr _) (repr_b := Coalgebra.comul_repr _) + + · ext a b a' b' + simpa only [Coalgebra.TensorProduct.comul_def, AlgebraTensorModule.curry_apply, curry_apply, + LinearMap.coe_restrictScalars, LinearMap.compl₁₂_apply, LinearMap.coe_comp, + LinearEquiv.coe_coe, Function.comp_apply, map_tmul, Coalgebra.comul_repr, tmul_sum, + sum_tmul, map_sum, tensorTensorTensorComm_tmul, LinearMap.coeFn_sum, Finset.sum_apply, + LinearMap.mul_apply', Algebra.TensorProduct.tmul_mul_tmul, homTensorHomMap_apply, + LinearMap.compRight_apply, e] using Finset.sum_congr rfl fun _ _ ↦ Finset.sum_comm + +end Bialgebra diff --git a/FLT/for_mathlib/HopfAlgebra/Basic.lean b/FLT/for_mathlib/HopfAlgebra/Basic.lean new file mode 100644 index 00000000..3be9ca67 --- /dev/null +++ b/FLT/for_mathlib/HopfAlgebra/Basic.lean @@ -0,0 +1,170 @@ +/- +Copyright (c) 2024 Yunzhou Xie. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yunzhou Xie, Yichen Feng, Yanqiao Zhou, Jujian Zhang +-/ + +import Mathlib.RingTheory.HopfAlgebra +import FLT.for_mathlib.Coalgebra.Monoid +import FLT.for_mathlib.Coalgebra.TensorProduct + +/-! +# Basic properties of Hopf algebra + +For an `R`-hopf algebra `A`, we prove in this file the following basic properties: +- the antipodal map is anticommutative; +- the antipodal map is unique linear map whose convolution inverse is the identity `𝟙 A`. + (Note that, confusingly, the indeity linear map `x ↦ x` is not acutally the unit in the monoid + structure of linear maps. See `for_mathlib/Coalgebra/Monoid.lean`) +if we further assume `A` is commutative then +- the `R`-algebra homorphisms from `A` to `L` has a group structure where multiplication is + convolution, and inverse of `f `is `f ∘ antipode` +- in particular, `antipode ∘ antipode = 1` +-/ + +open TensorProduct BigOperators + +namespace HopfAlgebra + +variable (R : Type*) [CommSemiring R] + +section noncommutative + +variable (A : Type*) [Semiring A] [HopfAlgebra R A] + +variable {R A} + +lemma antipode_repr {ι : Type*} (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A) + (repr : Coalgebra.comul a = ∑ i in ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) : + ∑ i in ℐ, antipode (R := R) (Δ₁ i) * Δ₂ i = algebraMap R A (Coalgebra.counit a) := by + have := mul_antipode_rTensor_comul_apply (R := R) a + rw [repr, map_sum, map_sum] at this + exact this + +lemma antipode_repr_eq_smul {ι : Type*} (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A) + (repr : Coalgebra.comul a = ∑ i in ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) : + ∑ i in ℐ, antipode (R := R) (Δ₁ i) * Δ₂ i = (Coalgebra.counit a : R) • (1 : A) := by + rw [antipode_repr (repr := repr), Algebra.smul_def, mul_one] + +lemma antipode_repr' {ι : Type*} (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A) + (repr : Coalgebra.comul a = ∑ i in ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) : + ∑ i in ℐ, Δ₁ i * antipode (R := R) (Δ₂ i) = algebraMap R A (Coalgebra.counit a) := by + have := mul_antipode_lTensor_comul_apply (R := R) a + rw [repr, map_sum, map_sum] at this + exact this + +lemma antipode_repr_eq_smul' {ι : Type*} (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A) + (repr : Coalgebra.comul a = ∑ i in ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) : + ∑ i in ℐ, Δ₁ i * antipode (R := R) (Δ₂ i) = (Coalgebra.counit a : R) • 1 := by + rw [antipode_repr' (repr := repr), Algebra.smul_def, mul_one] + +lemma antipode_mul_id : antipode (R := R) (A := A) * LinearMap.id = 1 := by + ext x + simpa [LinearPoint.mul_repr (repr := Coalgebra.comul_repr x)] using + antipode_repr (repr := Coalgebra.comul_repr x) + +lemma id_mul_antipode : LinearMap.id * antipode (R := R) (A := A) = 1 := by + ext x + simpa [LinearPoint.mul_repr (repr := Coalgebra.comul_repr x)] using + antipode_repr' (repr := Coalgebra.comul_repr x) + +lemma antipode_unique {T : LinearPoint R A A} (h : T * LinearMap.id = 1) : + T = antipode := + left_inv_eq_right_inv (M := LinearPoint R A A) h id_mul_antipode + + +lemma antipode_unique' {T : LinearPoint R A A} (h : LinearMap.id * T = 1) : + T = antipode := + left_inv_eq_right_inv (M := LinearPoint R A A) antipode_mul_id h |>.symm + +lemma antipode_one : antipode (R := R) (A := A) 1 = 1 := by + simpa using antipode_repr (R := R) (A := A) 1 {0} (fun _ ↦ 1) (fun _ ↦ 1) + (by simp only [Bialgebra.comul_one, Finset.sum_const, Finset.card_singleton, one_smul]; rfl) + +lemma antipode_anticommute (a b : A) : + antipode (R := R) (a * b) = antipode (R := R) b * antipode (R := R) a := by + let α : LinearPoint R (A ⊗[R] A) A := antipode ∘ₗ (LinearMap.mul' R A) + let β : LinearPoint R (A ⊗[R] A) A := LinearMap.mul' R A ∘ₗ map antipode antipode ∘ₗ + TensorProduct.comm R A A + + suffices α = β from congr($this (a ⊗ₜ b)) + + apply left_inv_eq_right_inv (a := LinearMap.mul' R A) + · ext a b + simp only [AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars, + LinearPoint.mul_repr (repr := + Coalgebra.TensorProduct.comul_apply_repr'' (repr_a := Coalgebra.comul_repr (R := R) a) + (repr_b := Coalgebra.comul_repr (R := R) b)), + LinearMap.coe_comp, Function.comp_apply, LinearMap.mul'_apply, LinearPoint.one_def, + Coalgebra.TensorProduct.counit_def, LinearEquiv.coe_coe, map_tmul, lid_tmul, smul_eq_mul, + Algebra.linearMap_apply, α, ← Bialgebra.counit_mul, Coalgebra.TensorProduct.comul_def] + apply antipode_repr + simpa only [Bialgebra.comul_mul, Coalgebra.comul_repr (a := a), Coalgebra.comul_repr (a := b), + Finset.mul_sum, Finset.sum_mul, Algebra.TensorProduct.tmul_mul_tmul, Finset.sum_product] using + Finset.sum_comm + + · ext a b + simp only [AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars, + LinearPoint.mul_repr (repr := + Coalgebra.TensorProduct.comul_apply_repr'' (repr_a := Coalgebra.comul_repr (R := R) a) + (repr_b := Coalgebra.comul_repr (R := R) b)), + LinearMap.mul'_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, comm_tmul, + map_tmul, show ∀ a b c d : A, a * b * (c * d) = a * (b * c) * d by intros; group, + Finset.sum_product, ← Finset.sum_mul, ← Finset.mul_sum, + antipode_repr_eq_smul' (repr := Coalgebra.comul_repr b), LinearPoint.one_def, + Coalgebra.TensorProduct.counit_def, lid_tmul, smul_eq_mul, Algebra.linearMap_apply, + _root_.map_mul, β, Algebra.mul_smul_comm, mul_one, Algebra.smul_mul_assoc, ← Finset.smul_sum, + antipode_repr_eq_smul' (repr := Coalgebra.comul_repr a), ← mul_smul, mul_comm] + simp [Algebra.smul_def] + +lemma antipode_algebraMap (r : R) : antipode (R := R) (algebraMap R A r) = algebraMap R A r := by + rw [Algebra.algebraMap_eq_smul_one, LinearMap.map_smul, antipode_one] + +end noncommutative + +section commutative + +variable (A L : Type*) [CommSemiring A] [HopfAlgebra R A] [CommSemiring L] [Algebra R L] + +variable {R A} + +/-- +If `A` is a commutative `R`=hopf algebra, then antipodal map is an algebra homomorphism +-/ +@[simps!] +def antipodeAlgHom : A →ₐ[R] A := AlgHom.ofLinearMap antipode antipode_one fun a b ↦ by + rw [antipode_anticommute, mul_comm] + +namespace AlgHomPoint + +noncomputable instance instGroup : Group (AlgHomPoint R A L) where + inv f := f.comp antipodeAlgHom + mul_left_inv f := AlgHom.ext fun x ↦ by + simp only [AlgHomPoint.mul_repr (repr := Coalgebra.comul_repr x), AlgHom.comp_apply, + antipodeAlgHom_apply, ← f.map_mul, ← map_sum, f.commutes, Algebra.ofId_apply, + antipode_repr (repr := Coalgebra.comul_repr x), AlgHomPoint.one_def, + Bialgebra.counitAlgHom_apply] + +end AlgHomPoint + +lemma antipodeAlgHom_inv : antipodeAlgHom⁻¹ = AlgHom.id R A := + inv_eq_iff_mul_eq_one.mpr <| mul_eq_one_iff_eq_inv.mpr rfl + +lemma antipodeAlgHom_mul_id : antipodeAlgHom * AlgHom.id R A = 1 := + AlgHom.ext fun _ ↦ congr($(antipode_mul_id) _) + +lemma id_mul_antipodeAlgHom : AlgHom.id R A * antipodeAlgHom = 1 := + AlgHom.ext fun _ ↦ congr($(id_mul_antipode) _) + +lemma antipodeAlgHom_square : antipodeAlgHom.comp antipodeAlgHom = AlgHom.id R A := + antipodeAlgHom_inv + +/-- +Then antipode map is an algebra equivalence. +-/ +lemma antipodeAlgEquiv : A ≃ₐ[R] A := + AlgEquiv.ofAlgHom antipodeAlgHom antipodeAlgHom antipodeAlgHom_square antipodeAlgHom_square + +end commutative + +end HopfAlgebra