@[reducible, inline]

abbrev Definition_1_20_1 (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] : Type (max u v)

structure Subcoalgebra (R : Type u) (A : Type v) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] extends Submodule R A : Type v

• carrier : Set A
• add_mem' {a b : A} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• smul_mem' (c : R) {x : A} : x ∈ self.carrier → c • x ∈ self.carrier
• comul_mem (a : A) : a ∈ self.toSubmodule → CoalgebraStruct.comul a ∈ Submodule.map₂ (TensorProduct.mk R A A) self.toSubmodule self.toSubmodule

@[implicit_reducible]

instance Subcoalgebra.instSetLike {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] : SetLike (Subcoalgebra R A) A

class Comodule (R : Type u) (C : Type v) (M : Type u_1) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] : Type (max u_1 v)

• coact : M →ₗ[R] TensorProduct R C M
• coassoc : ↑(TensorProduct.assoc R C C M) ∘ₗ LinearMap.rTensor M CoalgebraStruct.comul ∘ₗ coact = LinearMap.lTensor C coact ∘ₗ coact
• counit_coact : LinearMap.rTensor M CoalgebraStruct.counit ∘ₗ coact = (TensorProduct.mk R R M) 1

@[reducible, inline]

abbrev LeftComodule_def_1_20_2 (R : Type u) (C : Type v) (M : Type u_1) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] : Type (max u_1 v)

@[reducible, inline]

abbrev Definition_1_20_2 (R : Type u) (C : Type v) (M : Type u_1) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] : Type (max u_1 v)

@[implicit_reducible]

instance Coalgebra.regularComodule (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : Comodule R C C

class RightComodule (R : Type u) (C : Type v) (M : Type u_1) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] : Type (max u_1 v)

• coact : M →ₗ[R] TensorProduct R M C
• coassoc : ↑(TensorProduct.assoc R M C C) ∘ₗ LinearMap.rTensor C coact ∘ₗ coact = LinearMap.lTensor M CoalgebraStruct.comul ∘ₗ coact
• counit_coact : LinearMap.lTensor M CoalgebraStruct.counit ∘ₗ coact = (TensorProduct.mk R M R).flip 1

@[reducible, inline]

abbrev RightComodule_def_1_20_2 (R : Type u) (C : Type v) (M : Type u_1) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] : Type (max u_1 v)

@[implicit_reducible]

instance Coalgebra.regularRightComodule (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : RightComodule R C C

theorem unit_endo_comp_eval (k : Type u) [CommRing k] (f g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat k) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat k)) : (ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g)) 1 = (ModuleCat.Hom.hom f) 1 * (ModuleCat.Hom.hom g) 1

noncomputable def endF_counit_def (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] : CategoryTheory.End F →ₗ[k] k

The counit End(F) → k of the bialgebra End(F) of a fiber functor F: evaluate the natural transformation at the unit object and read off its action on 1 ∈ k.

noncomputable def functorSelfTensor (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] (F : CategoryTheory.Functor C (ModuleCat k)) : CategoryTheory.Functor (C × C) (ModuleCat k)

The bifunctor (X, Y) ↦ F(X) ⊗ F(Y) from C × C to ModuleCat k, used to express the multiplicative structure on End(F).

@[implicit_reducible]

noncomputable instance instSemiringEndTensor (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] (F : CategoryTheory.Functor C (ModuleCat k)) : Semiring (TensorProduct k (CategoryTheory.End F) (CategoryTheory.End F))

The tensor product End(F) ⊗_k End(F) is itself a (semi)ring via the tensor product of algebras.

@[implicit_reducible]

noncomputable instance instAlgebraEndTensor (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] (F : CategoryTheory.Functor C (ModuleCat k)) : Algebra k (TensorProduct k (CategoryTheory.End F) (CategoryTheory.End F))

The tensor product End(F) ⊗_k End(F) is a k-algebra.

noncomputable def prop_1_18_3_algEquiv (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] (F : CategoryTheory.Functor C (ModuleCat k)) : TensorProduct k (CategoryTheory.End F) (CategoryTheory.End F) ≃ₐ[k] CategoryTheory.End (functorSelfTensor k C F)

Proposition 1.18.3: the canonical algebra isomorphism End(F₁) ⊗ End(F₂) ≅ End(F₁ ⊗ F₂), here specialized to F₁ = F₂ = F.

def evalAtHom (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] (F : CategoryTheory.Functor C (ModuleCat k)) (Z : C) : CategoryTheory.End F →ₗ[k] ↑(F.obj Z) →ₗ[k] ↑(F.obj Z)

Evaluation map sending an endomorphism η ∈ End F to its component at Z, viewed as a k-linear endomorphism of F.obj Z.

def wrapEnd (k : Type u) [CommRing k] (M : ModuleCat k) : (↑M →ₗ[k] ↑M) →ₗ[k] CategoryTheory.End M

Wrap a k-linear endomorphism of the underlying module into the corresponding endomorphism in ModuleCat k.

noncomputable def endF_tensor_hom (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] (F : CategoryTheory.Functor C (ModuleCat k)) (X Y : C) : TensorProduct k (CategoryTheory.End F) (CategoryTheory.End F) →ₗ[k] CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))

The canonical map End(F) ⊗ End(F) → End(F(X) ⊗ F(Y)) sending η₁ ⊗ η₂ to η₁ ⊗ η₂ evaluated component-wise.

theorem endF_tensor_hom_tmul (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] (X Y : C) (η₁ η₂ : CategoryTheory.End F) : (endF_tensor_hom k C F X Y) (η₁ ⊗ₜ[k] η₂) = CategoryTheory.MonoidalCategoryStruct.tensorHom (η₁.app X) (η₂.app Y)

On a simple tensor η₁ ⊗ η₂, endF_tensor_hom returns the tensor product of the component morphisms η₁.app X ⊗ₘ η₂.app Y.

theorem prop_1_18_3 (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : ∃ (Δ : CategoryTheory.End F →ₗ[k] TensorProduct k (CategoryTheory.End F) (CategoryTheory.End F)), ∀ (X Y : C) (η : CategoryTheory.End F), (endF_tensor_hom k C F X Y) (Δ η) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.Monoidal.μIso F X Y).hom (CategoryTheory.CategoryStruct.comp (η.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) (CategoryTheory.Functor.Monoidal.μIso F X Y).inv)

Existence half of Proposition 1.18.3: there is a comultiplication Δ : End(F) → End(F) ⊗ End(F) whose image under endF_tensor_hom recovers the "conjugated" component-wise action of η on F(X ⊗ Y).

theorem prop_1_18_3_injective (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] (t : TensorProduct k (CategoryTheory.End F) (CategoryTheory.End F)) : (∀ (X Y : C), (endF_tensor_hom k C F X Y) t = 0) → t = 0

Faithfulness consequence of Proposition 1.18.3: the system of maps endF_tensor_hom across all X, Y jointly separates elements of End(F) ⊗ End(F).

theorem prop_1_18_3_mul (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] (X Y : C) (a b : TensorProduct k (CategoryTheory.End F) (CategoryTheory.End F)) : (endF_tensor_hom k C F X Y) (a * b) = (endF_tensor_hom k C F X Y) a * (endF_tensor_hom k C F X Y) b

The map endF_tensor_hom k C F X Y is multiplicative on End(F) ⊗ End(F).

noncomputable def endF_comul (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : CategoryTheory.End F →ₗ[k] TensorProduct k (CategoryTheory.End F) (CategoryTheory.End F)

The comultiplication on End(F) produced by Proposition 1.18.3.

theorem prop_1_18_3_coassoc (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : ↑(TensorProduct.assoc k (CategoryTheory.End F) (CategoryTheory.End F) (CategoryTheory.End F)) ∘ₗ LinearMap.rTensor (CategoryTheory.End F) (endF_comul k C F) ∘ₗ endF_comul k C F = LinearMap.lTensor (CategoryTheory.End F) (endF_comul k C F) ∘ₗ endF_comul k C F

Coassociativity of the comultiplication endF_comul.

theorem prop_1_18_3_left_counit (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : LinearMap.rTensor (CategoryTheory.End F) (endF_counit_def k C F) ∘ₗ endF_comul k C F = (TensorProduct.mk k k (CategoryTheory.End F)) 1

Left counit axiom: applying endF_counit_def to the first tensor factor of endF_comul returns the canonical embedding.

theorem prop_1_18_3_right_counit (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : LinearMap.lTensor (CategoryTheory.End F) (endF_counit_def k C F) ∘ₗ endF_comul k C F = (TensorProduct.mk k (CategoryTheory.End F) k).flip 1

Right counit axiom: applying endF_counit_def to the second tensor factor of endF_comul returns the canonical embedding.

theorem endF_comul_spec (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] (X Y : C) (η : CategoryTheory.End F) : (endF_tensor_hom k C F X Y) ((endF_comul k C F) η) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.Monoidal.μIso F X Y).hom (CategoryTheory.CategoryStruct.comp (η.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) (CategoryTheory.Functor.Monoidal.μIso F X Y).inv)

Specification property of endF_comul: under endF_tensor_hom, the comultiplication of η is the conjugate of η.app (X ⊗ Y) by the monoidal multiplication isomorphism.

theorem endF_tensor_eq_of_eval_eq (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] (t₁ t₂ : TensorProduct k (CategoryTheory.End F) (CategoryTheory.End F)) (h : ∀ (X Y : C), (endF_tensor_hom k C F X Y) t₁ = (endF_tensor_hom k C F X Y) t₂) : t₁ = t₂

Two elements of End(F) ⊗ End(F) agreeing under all endF_tensor_hom maps must be equal, by the injectivity of the joint evaluation.

theorem thm_1_21_1_coalgebra_properties (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : ↑(TensorProduct.assoc k (CategoryTheory.End F) (CategoryTheory.End F) (CategoryTheory.End F)) ∘ₗ LinearMap.rTensor (CategoryTheory.End F) (endF_comul k C F) ∘ₗ endF_comul k C F = LinearMap.lTensor (CategoryTheory.End F) (endF_comul k C F) ∘ₗ endF_comul k C F ∧ LinearMap.rTensor (CategoryTheory.End F) (endF_counit_def k C F) ∘ₗ endF_comul k C F = (TensorProduct.mk k k (CategoryTheory.End F)) 1 ∧ LinearMap.lTensor (CategoryTheory.End F) (endF_counit_def k C F) ∘ₗ endF_comul k C F = (TensorProduct.mk k (CategoryTheory.End F) k).flip 1 ∧ (endF_comul k C F) 1 = 1 ∧ (LinearMap.mul k (CategoryTheory.End F)).compr₂ (endF_comul k C F) = (LinearMap.mul k (TensorProduct k (CategoryTheory.End F) (CategoryTheory.End F))).compl₁₂ (endF_comul k C F) (endF_comul k C F)

Theorem 1.21.1: The endomorphism algebra End(F) of a fiber functor is a bialgebra, i.e. its comultiplication and counit are unital algebra homomorphisms satisfying the coassociativity, counit, and multiplicativity properties.

theorem endF_comul_coassoc (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : ↑(TensorProduct.assoc k (CategoryTheory.End F) (CategoryTheory.End F) (CategoryTheory.End F)) ∘ₗ LinearMap.rTensor (CategoryTheory.End F) (endF_comul k C F) ∘ₗ endF_comul k C F = LinearMap.lTensor (CategoryTheory.End F) (endF_comul k C F) ∘ₗ endF_comul k C F

Coassociativity component of thm_1_21_1_coalgebra_properties.

theorem endF_comul_left_counit (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : LinearMap.rTensor (CategoryTheory.End F) (endF_counit_def k C F) ∘ₗ endF_comul k C F = (TensorProduct.mk k k (CategoryTheory.End F)) 1

Left counit component of thm_1_21_1_coalgebra_properties.

theorem endF_comul_right_counit (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : LinearMap.lTensor (CategoryTheory.End F) (endF_counit_def k C F) ∘ₗ endF_comul k C F = (TensorProduct.mk k (CategoryTheory.End F) k).flip 1

Right counit component of thm_1_21_1_coalgebra_properties.

theorem endF_comul_one (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : (endF_comul k C F) 1 = 1

The comultiplication is unital: Δ(1) = 1.

theorem endF_comul_mul (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : (LinearMap.mul k (CategoryTheory.End F)).compr₂ (endF_comul k C F) = (LinearMap.mul k (TensorProduct k (CategoryTheory.End F) (CategoryTheory.End F))).compl₁₂ (endF_comul k C F) (endF_comul k C F)

The comultiplication is multiplicative: Δ(ab) = Δ(a) · Δ(b).

theorem endF_counit_one_proof (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : (endF_counit_def k C F) 1 = 1

The counit is unital: ε(1) = 1.

theorem endF_mul_compr₂_counit_proof (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : (LinearMap.mul k (CategoryTheory.End F)).compr₂ (endF_counit_def k C F) = (LinearMap.mul k k).compl₁₂ (endF_counit_def k C F) (endF_counit_def k C F)

The counit is multiplicative: ε(a · b) = ε(a) · ε(b).

@[implicit_reducible]

noncomputable instance endF_coalgebraInstance (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : Coalgebra k (CategoryTheory.End F)

The coalgebra structure on End(F) arising from endF_comul and endF_counit_def.

@[reducible]

noncomputable def thm_1_21_1_endF_bialgebra (k : Type u) [CommRing k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Monoidal] [F.Faithful] : Bialgebra k (CategoryTheory.End F)

Theorem 1.21.1: The bialgebra structure on End(F) of a fiber functor F, combining the coalgebra structure with the unit/multiplicativity axioms.

@[reducible]

def thm_1_21_1_converse (R' : Type u_1) (H' : Type u_2) [CommSemiring R'] [Semiring H'] [Algebra R' H'] (Δ : H' →ₐ[R'] TensorProduct R' H' H') (ε : H' →ₐ[R'] R') (h_coassoc : (↑(Algebra.TensorProduct.assoc R' R' R' H' H' H')).comp ((Algebra.TensorProduct.map Δ (AlgHom.id R' H')).comp Δ) = (Algebra.TensorProduct.map (AlgHom.id R' H') Δ).comp Δ) (h_rTensor : (Algebra.TensorProduct.map ε (AlgHom.id R' H')).comp Δ = ↑(Algebra.TensorProduct.lid R' H').symm) (h_lTensor : (Algebra.TensorProduct.map (AlgHom.id R' H') ε).comp Δ = ↑(Algebra.TensorProduct.rid R' R' H').symm) : Bialgebra R' H'

Converse direction for Theorem 1.21.1: a k-algebra equipped with algebra maps Δ, ε satisfying the coassociativity and counit axioms is a bialgebra.

@[reducible, inline]

abbrev IsBialgebra (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] : Type (max u v)

A bialgebra over R is an algebra equipped with a compatible coalgebra structure.

@[reducible, inline]

abbrev Definition_1_21_2 (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] : Type (max u v)

Definition 1.21.2: An algebra H with comultiplication Δ and counit ε satisfying the bialgebra axioms is called a bialgebra.

theorem Coalgebra.exists_fg_submodule_comul_mem {R : Type u} {C : Type v} [CommRing R] [AddCommGroup C] [Module R C] [Coalgebra R C] (c : C) : ∃ (V : Submodule R C), V.FG ∧ c ∈ V ∧ comul c ∈ Submodule.map₂ (TensorProduct.mk R C C) ⊤ V

Fundamental theorem ingredient: every element c of a coalgebra C lies in some finitely generated submodule V such that Δ(c) ∈ C ⊗ V.