feat(RingTheory/Coalgebra): product of coalgebras (#8822)

This also splits out a `CoalgebraStruct` typeclass, to allow defining the operators and their definitional properties before committing to proving coassociativity.

These proofs are extremely painful, as you're fighting associativity all the time (and `LinearMap.comp` is very verbose in the goal view)

Mathlib/LinearAlgebra/Prod.lean

@@ -172,6 +172,14 @@ theorem ker_fst : ker (fst R M M₂) = range (inr R M M₂) :=
   Eq.symm <| range_inr R M M₂
 #align linear_map.ker_fst LinearMap.ker_fst
 
+@[simp] theorem fst_comp_inl : fst R M M₂ ∘ₗ inl R M M₂ = id := rfl
+
+@[simp] theorem snd_comp_inl : snd R M M₂ ∘ₗ inl R M M₂ = 0 := rfl
+
+@[simp] theorem fst_comp_inr : fst R M M₂ ∘ₗ inr R M M₂ = 0 := rfl
+
+@[simp] theorem snd_comp_inr : snd R M M₂ ∘ₗ inr R M M₂ = id := rfl
+
 end
 
 @[simp]

Mathlib/LinearAlgebra/TensorProduct.lean

@@ -41,9 +41,10 @@ section Semiring
 variable {R : Type*} [CommSemiring R]
 variable {R' : Type*} [Monoid R']
 variable {R'' : Type*} [Semiring R'']
-variable {M : Type*} {N : Type*} {P : Type*} {Q : Type*} {S : Type*}
-variable [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S]
-variable [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S]
+variable {M : Type*} {N : Type*} {P : Type*} {Q : Type*} {S : Type*} {T : Type*}
+variable [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P]
+variable [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T]
+variable [Module R M] [Module R N] [Module R P] [Module R Q] [Module R S] [Module R T]
 variable [DistribMulAction R' M]
 variable [Module R'' M]
 variable (M N)
@@ -796,11 +797,42 @@ theorem map_tmul (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (m : M) (n : N) : map f
   rfl
 #align tensor_product.map_tmul TensorProduct.map_tmul
 
+/-- Given linear maps `f : M → P`, `g : N → Q`, if we identify `M ⊗ N` with `N ⊗ M` and `P ⊗ Q`
+with `Q ⊗ P`, then this lemma states that `f ⊗ g = g ⊗ f`. -/
 lemma map_comp_comm_eq (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
-    map f g ∘ₗ TensorProduct.comm R N M =
-      TensorProduct.comm R Q P ∘ₗ map g f :=
+    map f g ∘ₗ TensorProduct.comm R N M = TensorProduct.comm R Q P ∘ₗ map g f :=
   ext rfl
 
+lemma map_comm (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : N ⊗[R] M):
+    map f g (TensorProduct.comm R N M x) = TensorProduct.comm R Q P (map g f x) :=
+  FunLike.congr_fun (map_comp_comm_eq _ _) _
+
+/-- Given linear maps `f : M → Q`, `g : N → S`, and `h : P → T`, if we identify `(M ⊗ N) ⊗ P`
+with `M ⊗ (N ⊗ P)` and `(Q ⊗ S) ⊗ T` with `Q ⊗ (S ⊗ T)`, then this lemma states that
+`f ⊗ (g ⊗ h) = (f ⊗ g) ⊗ h`. -/
+lemma map_map_comp_assoc_eq (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) :
+    map f (map g h) ∘ₗ TensorProduct.assoc R M N P =
+      TensorProduct.assoc R Q S T ∘ₗ map (map f g) h :=
+  ext <| ext <| LinearMap.ext fun _ => LinearMap.ext fun _ => LinearMap.ext fun _ => rfl
+
+lemma map_map_assoc (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : (M ⊗[R] N) ⊗[R] P) :
+    map f (map g h) (TensorProduct.assoc R M N P x) =
+      TensorProduct.assoc R Q S T (map (map f g) h x) :=
+  FunLike.congr_fun (map_map_comp_assoc_eq _ _ _) _
+
+/-- Given linear maps `f : M → Q`, `g : N → S`, and `h : P → T`, if we identify `M ⊗ (N ⊗ P)`
+with `(M ⊗ N) ⊗ P` and `Q ⊗ (S ⊗ T)` with `(Q ⊗ S) ⊗ T`, then this lemma states that
+`(f ⊗ g) ⊗ h = f ⊗ (g ⊗ h)`. -/
+lemma map_map_comp_assoc_symm_eq (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) :
+    map (map f g) h ∘ₗ (TensorProduct.assoc R M N P).symm =
+      (TensorProduct.assoc R Q S T).symm ∘ₗ map f (map g h) :=
+  ext <| LinearMap.ext fun _ => ext <| LinearMap.ext fun _ => LinearMap.ext fun _ => rfl
+
+lemma map_map_assoc_symm (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : M ⊗[R] (N ⊗[R] P)) :
+    map (map f g) h ((TensorProduct.assoc R M N P).symm x) =
+      (TensorProduct.assoc R Q S T).symm (map f (map g h) x) :=
+  FunLike.congr_fun (map_map_comp_assoc_symm_eq _ _ _) _
+
 theorem map_range_eq_span_tmul (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
     range (map f g) = Submodule.span R { t | ∃ m n, f m ⊗ₜ g n = t } := by
   simp only [← Submodule.map_top, ← span_tmul_eq_top, Submodule.map_span, Set.mem_image,
@@ -933,6 +965,14 @@ theorem homTensorHomMap_apply (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
   rfl
 #align tensor_product.hom_tensor_hom_map_apply TensorProduct.homTensorHomMap_apply
 
+@[simp]
+theorem map_zero_left (g : N →ₗ[R] Q) : map (0 : M →ₗ[R] P) g = 0 :=
+  (mapBilinear R M N P Q).map_zero₂ _
+
+@[simp]
+theorem map_zero_right (f : M →ₗ[R] P) : map f (0 : N →ₗ[R] Q) = 0 :=
+  (mapBilinear R M N P Q _).map_zero
+
 end
 
 /-- If `M` and `P` are linearly equivalent and `N` and `Q` are linearly equivalent
@@ -1070,6 +1110,16 @@ theorem rTensor_tmul (m : M) (n : N) : f.rTensor M (n ⊗ₜ m) = f n ⊗ₜ m :
   rfl
 #align linear_map.rtensor_tmul LinearMap.rTensor_tmul
 
+@[simp]
+theorem lTensor_comp_mk (m : M) :
+    f.lTensor M ∘ₗ TensorProduct.mk R M N m = TensorProduct.mk R M P m ∘ₗ f :=
+  rfl
+
+@[simp]
+theorem rTensor_comp_flip_mk (m : M) :
+    f.rTensor M ∘ₗ (TensorProduct.mk R N M).flip m = (TensorProduct.mk R P M).flip m ∘ₗ f :=
+  rfl
+
 lemma comm_comp_rTensor_comp_comm_eq (g : N →ₗ[R] P) :
     TensorProduct.comm R P Q ∘ₗ rTensor Q g ∘ₗ TensorProduct.comm R Q N =
       lTensor Q g :=

Mathlib/RingTheory/Coalgebra.lean

@@ -3,14 +3,17 @@ Copyright (c) 2023 Ali Ramsey. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ali Ramsey
 -/
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.LinearAlgebra.Finsupp
+import Mathlib.LinearAlgebra.Prod
+import Mathlib.LinearAlgebra.TensorProduct
 
 /-!
 # Coalgebras
 
 In this file we define `Coalgebra`, and provide instances for:
 
 * Commutative semirings: `CommSemiring.toCoalgebra`
+* Binary products: `Prod.instCoalgebra`
 * Finitely supported functions: `Finsupp.instCoalgebra`
 
 ## References
@@ -20,17 +23,28 @@ In this file we define `Coalgebra`, and provide instances for:
 
 suppress_compilation
 
-universe u v
+universe u v w
 
 open scoped TensorProduct
 
-/-- A coalgebra over a commutative (semi)ring `R` is an `R`-module equipped with a coassociative
-comultiplication `Δ` and a counit `ε` obeying the left and right conunitality laws. -/
-class Coalgebra (R : Type u) (A : Type v) [CommSemiring R] [AddCommMonoid A] [Module R A] where
+/-- Data fields for `Coalgebra`, to allow API to be constructed before proving `Coalgebra.coassoc`.
+
+See `Coalgebra` for documentation. -/
+class CoalgebraStruct (R : Type u) (A : Type v)
+    [CommSemiring R] [AddCommMonoid A] [Module R A] where
   /-- The comultiplication of the coalgebra -/
   comul : A →ₗ[R] A ⊗[R] A
   /-- The counit of the coalgebra -/
   counit : A →ₗ[R] R
+
+namespace Coalgebra
+export CoalgebraStruct (comul counit)
+end Coalgebra
+
+/-- A coalgebra over a commutative (semi)ring `R` is an `R`-module equipped with a coassociative
+comultiplication `Δ` and a counit `ε` obeying the left and right conunitality laws. -/
+class Coalgebra (R : Type u) (A : Type v)
+    [CommSemiring R] [AddCommMonoid A] [Module R A] extends CoalgebraStruct R A where
   /-- The comultiplication is coassociative -/
   coassoc : TensorProduct.assoc R A A A ∘ₗ comul.rTensor A ∘ₗ comul = comul.lTensor A ∘ₗ comul
   /-- The counit satisfies the left counitality law -/
@@ -90,6 +104,83 @@ theorem counit_apply (r : R) : counit r = r := rfl
 
 end CommSemiring
 
+namespace Prod
+variable (R : Type u) (A : Type v) (B : Type w)
+variable [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B]
+variable [Coalgebra R A] [Coalgebra R B]
+
+open LinearMap
+
+instance instCoalgebraStruct : CoalgebraStruct R (A × B) where
+  comul := .coprod
+    (TensorProduct.map (.inl R A B) (.inl R A B) ∘ₗ comul)
+    (TensorProduct.map (.inr R A B) (.inr R A B) ∘ₗ comul)
+  counit := .coprod counit counit
+
+@[simp]
+theorem comul_apply (r : A × B) :
+    comul r =
+      TensorProduct.map (.inl R A B) (.inl R A B) (comul r.1) +
+      TensorProduct.map (.inr R A B) (.inr R A B) (comul r.2) := rfl
+
+@[simp]
+theorem counit_apply (r : A × B) : (counit r : R) = counit r.1 + counit r.2 := rfl
+
+theorem comul_comp_inl :
+    comul ∘ₗ inl R A B = TensorProduct.map (.inl R A B) (.inl R A B) ∘ₗ comul := by
+  ext; simp
+
+theorem comul_comp_inr :
+    comul ∘ₗ inr R A B = TensorProduct.map (.inr R A B) (.inr R A B) ∘ₗ comul := by
+  ext; simp
+
+theorem comul_comp_fst :
+    comul ∘ₗ .fst R A B = TensorProduct.map (.fst R A B) (.fst R A B) ∘ₗ comul := by
+  ext : 1
+  · rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc,
+      ← TensorProduct.map_comp, fst_comp_inl, TensorProduct.map_id, id_comp]
+  · rw [comp_assoc, fst_comp_inr, comp_zero, comp_assoc, comul_comp_inr, ← comp_assoc,
+      ← TensorProduct.map_comp, fst_comp_inr, TensorProduct.map_zero_left, zero_comp]
+
+theorem comul_comp_snd :
+    comul ∘ₗ .snd R A B = TensorProduct.map (.snd R A B) (.snd R A B) ∘ₗ comul := by
+  ext : 1
+  · rw [comp_assoc, snd_comp_inl, comp_zero, comp_assoc, comul_comp_inl, ← comp_assoc,
+      ← TensorProduct.map_comp, snd_comp_inl, TensorProduct.map_zero_left, zero_comp]
+  · rw [comp_assoc, snd_comp_inr, comp_id, comp_assoc, comul_comp_inr, ← comp_assoc,
+      ← TensorProduct.map_comp, snd_comp_inr, TensorProduct.map_id, id_comp]
+
+@[simp] theorem counit_comp_inr : counit ∘ₗ inr R A B = counit := by ext; simp
+
+@[simp] theorem counit_comp_inl : counit ∘ₗ inl R A B = counit := by ext; simp
+
+instance instCoalgebra : Coalgebra R (A × B) where
+  rTensor_counit_comp_comul := by
+    ext : 1
+    · rw [comp_assoc, comul_comp_inl, ← comp_assoc, rTensor_comp_map, counit_comp_inl,
+        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
+    · rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr,
+        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
+  lTensor_counit_comp_comul := by
+    ext : 1
+    · rw [comp_assoc, comul_comp_inl, ← comp_assoc, lTensor_comp_map, counit_comp_inl,
+        ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
+    · rw [comp_assoc, comul_comp_inr, ← comp_assoc, lTensor_comp_map, counit_comp_inr,
+        ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
+  coassoc := by
+    dsimp only [instCoalgebraStruct]
+    ext x : 2 <;> dsimp only [comp_apply, LinearEquiv.coe_coe, coe_inl, coe_inr, coprod_apply]
+    · simp only [map_zero, add_zero]
+      simp_rw [← comp_apply, ← comp_assoc, rTensor_comp_map, lTensor_comp_map, coprod_inl,
+        ← map_comp_rTensor, ← map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc,
+        TensorProduct.map_map_comp_assoc_eq, comp_apply, LinearEquiv.coe_coe]
+    · simp only [map_zero, zero_add]
+      simp_rw [← comp_apply, ← comp_assoc, rTensor_comp_map, lTensor_comp_map, coprod_inr,
+        ← map_comp_rTensor, ← map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc,
+        TensorProduct.map_map_comp_assoc_eq, comp_apply, LinearEquiv.coe_coe]
+
+end Prod
+
 namespace Finsupp
 variable (ι : Type v)
 
@@ -108,7 +199,7 @@ instance instCoalgebra : Coalgebra R (ι →₀ R) where
 @[simp]
 theorem comul_single (i : ι) (r : R) :
     comul (Finsupp.single i r) = (Finsupp.single i r) ⊗ₜ[R] (Finsupp.single i 1) := by
-  unfold comul instCoalgebra
+  unfold comul instCoalgebra toCoalgebraStruct
   rw [total_single, TensorProduct.smul_tmul', smul_single_one i r]
 
 @[simp]