|
| 1 | +/- |
| 2 | +Copyright (c) 2024 Amelia Livingston. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Amelia Livingston |
| 5 | +-/ |
| 6 | +import Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence |
| 7 | + |
| 8 | +/-! |
| 9 | +# Tensor products of coalgebras |
| 10 | +
|
| 11 | +Given two `R`-coalgebras `M, N`, we can define a natural comultiplication map |
| 12 | +`Δ : M ⊗[R] N → (M ⊗[R] N) ⊗[R] (M ⊗[R] N)` and counit map `ε : M ⊗[R] N → R` induced by |
| 13 | +the comultiplication and counit maps of `M` and `N`. These `Δ, ε` are declared as linear maps |
| 14 | +in `TensorProduct.instCoalgebraStruct` in `Mathlib.RingTheory.Coalgebra.Basic`. |
| 15 | +
|
| 16 | +In this file we show that `Δ, ε` satisfy the axioms of a coalgebra, and also define other data |
| 17 | +in the monoidal structure on `R`-coalgebras, like the tensor product of two coalgebra morphisms |
| 18 | +as a coalgebra morphism. |
| 19 | +
|
| 20 | +## Implementation notes |
| 21 | +
|
| 22 | +We keep the linear maps underlying `Δ, ε` and other definitions in this file syntactically equal |
| 23 | +to the corresponding definitions for tensor products of modules in the hope that this makes |
| 24 | +life easier. However, to fill in prop fields, we use the API in |
| 25 | +`Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence`. That file defines the monoidal category |
| 26 | +structure on coalgebras induced by an equivalence with comonoid objects in the category of modules, |
| 27 | +`CoalgebraCat.instMonoidalCategoryAux`, but we do not declare this as an instance - we just use it |
| 28 | +to prove things. Then, we use the definitions in this file to make a monoidal category instance on |
| 29 | +`CoalgebraCat R` in `Mathlib.Algebra.Category.CoalgebraCat.Monoidal` that has simpler data. |
| 30 | +
|
| 31 | +However, this approach forces our coalgebras to be in the same universe as the base ring `R`, |
| 32 | +since it relies on the monoidal category structure on `ModuleCat R`, which is currently |
| 33 | +universe monomorphic. Any contribution that achieves universe polymorphism would be welcome. For |
| 34 | +instance, the tensor product of coalgebras in the |
| 35 | +[FLT repo](https://github.com/ImperialCollegeLondon/FLT/blob/eef74b4538c8852363936dfaad23e6ffba72eca5/FLT/mathlibExperiments/Coalgebra/TensorProduct.lean) |
| 36 | +is already universe polymorphic since it does not go via category theory. |
| 37 | +
|
| 38 | +-/ |
| 39 | + |
| 40 | +universe v u |
| 41 | + |
| 42 | +open CategoryTheory |
| 43 | +open scoped TensorProduct |
| 44 | + |
| 45 | +section |
| 46 | + |
| 47 | +variable {R M N P Q : Type u} [CommRing R] |
| 48 | + [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Coalgebra R M] [Coalgebra R N] |
| 49 | + |
| 50 | +open MonoidalCategory in |
| 51 | +noncomputable instance TensorProduct.instCoalgebra : Coalgebra R (M ⊗[R] N) := |
| 52 | + let I := Monoidal.transport ((CoalgebraCat.comonEquivalence R).symm) |
| 53 | + CoalgEquiv.toCoalgebra |
| 54 | + (A := (CoalgebraCat.of R M ⊗ CoalgebraCat.of R N : CoalgebraCat R)) |
| 55 | + { LinearEquiv.refl R _ with |
| 56 | + counit_comp := rfl |
| 57 | + map_comp_comul := by |
| 58 | + rw [CoalgebraCat.ofComonObjCoalgebraStruct_comul] |
| 59 | + simp [-Mon_.monMonoidalStruct_tensorObj_X, |
| 60 | + ModuleCat.MonoidalCategory.instMonoidalCategoryStruct_tensorHom, |
| 61 | + ModuleCat.comp_def, ModuleCat.of, ModuleCat.ofHom, |
| 62 | + ModuleCat.MonoidalCategory.tensor_μ_eq_tensorTensorTensorComm] } |
| 63 | + |
| 64 | +end |
| 65 | + |
| 66 | +namespace Coalgebra |
| 67 | +namespace TensorProduct |
| 68 | + |
| 69 | +open CoalgebraCat.MonoidalCategoryAux MonoidalCategory |
| 70 | + |
| 71 | +variable {R M N P Q : Type u} [CommRing R] |
| 72 | + [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup Q] [Module R M] [Module R N] |
| 73 | + [Module R P] [Module R Q] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] [Coalgebra R Q] |
| 74 | + |
| 75 | +attribute [local instance] CoalgebraCat.instMonoidalCategoryAux in |
| 76 | +section |
| 77 | + |
| 78 | +/-- The tensor product of two coalgebra morphisms as a coalgebra morphism. -/ |
| 79 | +noncomputable def map (f : M →ₗc[R] N) (g : P →ₗc[R] Q) : |
| 80 | + M ⊗[R] P →ₗc[R] N ⊗[R] Q where |
| 81 | + toLinearMap := _root_.TensorProduct.map f.toLinearMap g.toLinearMap |
| 82 | + counit_comp := by |
| 83 | + simp_rw [← tensorHom_toLinearMap] |
| 84 | + apply (CoalgebraCat.ofHom f ⊗ CoalgebraCat.ofHom g).1.counit_comp |
| 85 | + map_comp_comul := by |
| 86 | + simp_rw [← tensorHom_toLinearMap, ← comul_tensorObj] |
| 87 | + apply (CoalgebraCat.ofHom f ⊗ CoalgebraCat.ofHom g).1.map_comp_comul |
| 88 | + |
| 89 | +@[simp] |
| 90 | +theorem map_tmul (f : M →ₗc[R] N) (g : P →ₗc[R] Q) (x : M) (y : P) : |
| 91 | + map f g (x ⊗ₜ y) = f x ⊗ₜ g y := |
| 92 | + rfl |
| 93 | + |
| 94 | +@[simp] |
| 95 | +theorem map_toLinearMap (f : M →ₗc[R] N) (g : P →ₗc[R] Q) : |
| 96 | + map f g = _root_.TensorProduct.map (f : M →ₗ[R] N) (g : P →ₗ[R] Q) := rfl |
| 97 | + |
| 98 | +variable (R M N P) |
| 99 | + |
| 100 | +/-- The associator for tensor products of R-coalgebras, as a coalgebra equivalence. -/ |
| 101 | +protected noncomputable def assoc : |
| 102 | + (M ⊗[R] N) ⊗[R] P ≃ₗc[R] M ⊗[R] (N ⊗[R] P) := |
| 103 | + { _root_.TensorProduct.assoc R M N P with |
| 104 | + counit_comp := by |
| 105 | + simp_rw [← associator_hom_toLinearMap, ← counit_tensorObj_tensorObj_right, |
| 106 | + ← counit_tensorObj_tensorObj_left] |
| 107 | + apply CoalgHom.counit_comp (α_ (CoalgebraCat.of R M) (CoalgebraCat.of R N) |
| 108 | + (CoalgebraCat.of R P)).hom.1 |
| 109 | + map_comp_comul := by |
| 110 | + simp_rw [← associator_hom_toLinearMap, ← comul_tensorObj_tensorObj_left, |
| 111 | + ← comul_tensorObj_tensorObj_right] |
| 112 | + exact CoalgHom.map_comp_comul (α_ (CoalgebraCat.of R M) |
| 113 | + (CoalgebraCat.of R N) (CoalgebraCat.of R P)).hom.1 } |
| 114 | + |
| 115 | +variable {R M N P} |
| 116 | + |
| 117 | +@[simp] |
| 118 | +theorem assoc_tmul (x : M) (y : N) (z : P) : |
| 119 | + Coalgebra.TensorProduct.assoc R M N P ((x ⊗ₜ y) ⊗ₜ z) = x ⊗ₜ (y ⊗ₜ z) := |
| 120 | + rfl |
| 121 | + |
| 122 | +@[simp] |
| 123 | +theorem assoc_symm_tmul (x : M) (y : N) (z : P) : |
| 124 | + (Coalgebra.TensorProduct.assoc R M N P).symm (x ⊗ₜ (y ⊗ₜ z)) = (x ⊗ₜ y) ⊗ₜ z := |
| 125 | + rfl |
| 126 | + |
| 127 | +@[simp] |
| 128 | +theorem assoc_toLinearEquiv : |
| 129 | + Coalgebra.TensorProduct.assoc R M N P = _root_.TensorProduct.assoc R M N P := rfl |
| 130 | + |
| 131 | +variable (R M) |
| 132 | + |
| 133 | +/-- The base ring is a left identity for the tensor product of coalgebras, up to |
| 134 | +coalgebra equivalence. -/ |
| 135 | +protected noncomputable def lid : R ⊗[R] M ≃ₗc[R] M := |
| 136 | + { _root_.TensorProduct.lid R M with |
| 137 | + counit_comp := by |
| 138 | + simp only [← leftUnitor_hom_toLinearMap] |
| 139 | + apply CoalgHom.counit_comp (λ_ (CoalgebraCat.of R M)).hom.1 |
| 140 | + map_comp_comul := by |
| 141 | + simp_rw [← leftUnitor_hom_toLinearMap, ← comul_tensorObj] |
| 142 | + apply CoalgHom.map_comp_comul (λ_ (CoalgebraCat.of R M)).hom.1 } |
| 143 | + |
| 144 | +variable {R M} |
| 145 | + |
| 146 | +@[simp] |
| 147 | +theorem lid_toLinearEquiv : |
| 148 | + (Coalgebra.TensorProduct.lid R M) = _root_.TensorProduct.lid R M := rfl |
| 149 | + |
| 150 | +@[simp] |
| 151 | +theorem lid_tmul (r : R) (a : M) : Coalgebra.TensorProduct.lid R M (r ⊗ₜ a) = r • a := rfl |
| 152 | + |
| 153 | +@[simp] |
| 154 | +theorem lid_symm_apply (a : M) : (Coalgebra.TensorProduct.lid R M).symm a = 1 ⊗ₜ a := rfl |
| 155 | + |
| 156 | +variable (R M) |
| 157 | + |
| 158 | +/-- The base ring is a right identity for the tensor product of coalgebras, up to |
| 159 | +coalgebra equivalence. -/ |
| 160 | +protected noncomputable def rid : M ⊗[R] R ≃ₗc[R] M := |
| 161 | + { _root_.TensorProduct.rid R M with |
| 162 | + counit_comp := by |
| 163 | + simp only [← rightUnitor_hom_toLinearMap] |
| 164 | + apply CoalgHom.counit_comp (ρ_ (CoalgebraCat.of R M)).hom.1 |
| 165 | + map_comp_comul := by |
| 166 | + simp_rw [← rightUnitor_hom_toLinearMap, ← comul_tensorObj] |
| 167 | + apply CoalgHom.map_comp_comul (ρ_ (CoalgebraCat.of R M)).hom.1 } |
| 168 | + |
| 169 | +variable {R M} |
| 170 | + |
| 171 | +@[simp] |
| 172 | +theorem rid_toLinearEquiv : |
| 173 | + (Coalgebra.TensorProduct.rid R M) = _root_.TensorProduct.rid R M := rfl |
| 174 | + |
| 175 | +@[simp] |
| 176 | +theorem rid_tmul (r : R) (a : M) : Coalgebra.TensorProduct.rid R M (a ⊗ₜ r) = r • a := rfl |
| 177 | + |
| 178 | +@[simp] |
| 179 | +theorem rid_symm_apply (a : M) : (Coalgebra.TensorProduct.rid R M).symm a = a ⊗ₜ 1 := rfl |
| 180 | + |
| 181 | +end |
| 182 | + |
| 183 | +end TensorProduct |
| 184 | +end Coalgebra |
| 185 | +namespace CoalgHom |
| 186 | + |
| 187 | +variable {R M N P : Type u} [CommRing R] |
| 188 | + [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] |
| 189 | + [Module R P] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] |
| 190 | + |
| 191 | +variable (M) |
| 192 | + |
| 193 | +/-- `lTensor M f : M ⊗ N →ₗc M ⊗ P` is the natural coalgebra morphism induced by `f : N →ₗc P`. -/ |
| 194 | +noncomputable abbrev lTensor (f : N →ₗc[R] P) : M ⊗[R] N →ₗc[R] M ⊗[R] P := |
| 195 | + Coalgebra.TensorProduct.map (CoalgHom.id R M) f |
| 196 | + |
| 197 | +/-- `rTensor M f : N ⊗ M →ₗc P ⊗ M` is the natural coalgebra morphism induced by `f : N →ₗc P`. -/ |
| 198 | +noncomputable abbrev rTensor (f : N →ₗc[R] P) : N ⊗[R] M →ₗc[R] P ⊗[R] M := |
| 199 | + Coalgebra.TensorProduct.map f (CoalgHom.id R M) |
| 200 | + |
| 201 | +end CoalgHom |
0 commit comments