(Coalgebra/Monoid): more tinkering

Author: kbuzzard

FLT/for_mathlib/Coalgebra/Monoid.lean

@@ -36,8 +36,8 @@ open TensorProduct BigOperators LinearMap
 section Coalgebra
 
 -- Note that using an `abbrev` here creates a diamond in the case `A = L`, when there
--- is already a multiplication on `A →ₗ[R] A`
--- a multiplication, defined by composition.
+-- is already a multiplication on `A →ₗ[R] A`, defined by composition.
+
 /--
 Let `A` be an `R`-coalgebra and `L` an `R`-algebra. An `L`-linear point of `A`
 is an `R`-linear map from `A` to `L`.
@@ -61,46 +61,47 @@ If `comul x = ∑ aᵢ ⊗ bᵢ`, then `(φ ⋆ ψ)(x) = ∑ φ(aᵢ) × ψ(bᵢ
 noncomputable def mul : LinearPoint R A L :=
   LinearMap.mul' _ _ ∘ₗ TensorProduct.map φ ψ ∘ₗ Coalgebra.comul
 
+noncomputable instance : Mul (LinearPoint R A L) where
+  mul := mul
+
+lemma mul_def (φ ψ : LinearPoint R A L) :
+    φ * ψ = LinearMap.mul' _ _ ∘ₗ TensorProduct.map φ ψ ∘ₗ Coalgebra.comul := rfl
+
 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
-      (φ * ψ) * χ =
+  rw [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
-      φ * (ψ * χ) =
+      by simp only [← comp_assoc, map_comp_rTensor, rTensor_comp_map]; rfl]
+  rw [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]
+      by simp only [← comp_assoc, map_comp_lTensor, lTensor_comp_map]; rfl]
+  simp only [mul', comp_apply, Coalgebra.comul_repr, map_sum, rTensor_tmul, sum_tmul, map_tmul,
+    lift.tmul, mul_apply', mul_assoc, ← Coalgebra.coassoc, LinearEquiv.coe_coe, assoc_tmul,
+    lTensor_tmul]
+
+/--
+`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
 
 lemma mul_one' : φ * 1 = φ := show mul φ one = φ from LinearMap.ext fun _ ↦ by
   simp [show φ.mul one =
@@ -159,6 +160,23 @@ If `comul x = ∑ aᵢ ⊗ bᵢ`, then `(φ ⋆ ψ)(x) = ∑ φ(aᵢ) × ψ(bᵢ
 noncomputable def mul : AlgHomPoint R A L :=
   Algebra.TensorProduct.lmul' R (S := L) |>.comp <|
     Algebra.TensorProduct.map φ ψ |>.comp <| Bialgebra.comulAlgHom R A
+
+noncomputable instance : Mul (AlgHomPoint R A L) where
+  mul := mul
+
+lemma mul_def (φ ψ : AlgHomPoint R A L) :
+    φ * ψ = (Algebra.TensorProduct.lmul' R (S := L) |>.comp <|
+      Algebra.TensorProduct.map φ ψ |>.comp <| Bialgebra.comulAlgHom R A) := rfl
+
+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
+
+lemma mul_assoc' : φ * ψ * χ = φ * (ψ * χ) := by
+  ext
+  exact congr($(mul_assoc φ.toLinearPoint ψ.toLinearPoint χ.toLinearPoint) _)
+
 /--
 `A -counit-> R -algebraMap-> L` is the unit with respect to convolution product.
 -/
@@ -171,13 +189,6 @@ noncomputable instance : One (AlgHomPoint R A L) where
 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) _)
 
@@ -189,11 +200,6 @@ noncomputable instance instMonoid : Monoid (AlgHomPoint R A L) where
   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