The category of coalgebras over a commutative ring

We introduce the bundled category CoalgebraCat of coalgebras over a fixed commutative ring R along with the forgetful functor to ModuleCat.

This file mimics Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.

structure CoalgebraCat (R : Type u) [CommRing R] extends ModuleCat R : Type (max u (v + 1))

The category of R-coalgebras.

• carrier : Type v
• isAddCommGroup : AddCommGroup ↑self.toModuleCat
• isModule : Module R ↑self.toModuleCat
• instCoalgebra : Coalgebra R ↑self.toModuleCat

instance CoalgebraCat.instCoeSortType {R : Type u} [CommRing R] : CoeSort (CoalgebraCat R) (Type v)

Equations

• CoalgebraCat.instCoeSortType = { coe := fun (x : CoalgebraCat R) => ↑x.toModuleCat }

@[simp]

theorem CoalgebraCat.moduleCat_of_toModuleCat {R : Type u} [CommRing R] (X : CoalgebraCat R) : ModuleCat.of R ↑X.toModuleCat = X.toModuleCat

@[reducible, inline]

abbrev CoalgebraCat.of (R : Type u) [CommRing R] (X : Type v) [AddCommGroup X] [Module R X] [Coalgebra R X] : CoalgebraCat R

The object in the category of R-coalgebras associated to an R-coalgebra.

Equations

• CoalgebraCat.of R X = { toModuleCat := ModuleCat.of R X, instCoalgebra := inferInstance }

@[simp]

theorem CoalgebraCat.of_comul {R : Type u} [CommRing R] {X : Type v} [AddCommGroup X] [Module R X] [Coalgebra R X] : CoalgebraStruct.comul = CoalgebraStruct.comul

@[simp]

theorem CoalgebraCat.of_counit {R : Type u} [CommRing R] {X : Type v} [AddCommGroup X] [Module R X] [Coalgebra R X] : CoalgebraStruct.counit = CoalgebraStruct.counit

structure CoalgebraCat.Hom {R : Type u} [CommRing R] (V W : CoalgebraCat R) : Type v

A type alias for CoalgHom to avoid confusion between the categorical and algebraic spellings of composition.

• toCoalgHom' : ↑V.toModuleCat →ₗc[R] ↑W.toModuleCat

  The underlying CoalgHom

theorem CoalgebraCat.Hom.ext {R : Type u} {inst✝ : CommRing R} {V W : CoalgebraCat R} {x y : V.Hom W} (toCoalgHom' : x.toCoalgHom' = y.toCoalgHom') : x = y

instance CoalgebraCat.category {R : Type u} [CommRing R] : CategoryTheory.Category.{v, max (v + 1) u} (CoalgebraCat R)

Equations

• CoalgebraCat.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯

instance CoalgebraCat.concreteCategory {R : Type u} [CommRing R] : CategoryTheory.ConcreteCategory (CoalgebraCat R) fun (x1 x2 : CoalgebraCat R) => ↑x1.toModuleCat →ₗc[R] ↑x2.toModuleCat

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CoalgebraCat.Hom.toCoalgHom {R : Type u} [CommRing R] {X Y : CoalgebraCat R} (f : X.Hom Y) : ↑X.toModuleCat →ₗc[R] ↑Y.toModuleCat

Turn a morphism in CoalgebraCat back into a CoalgHom.

Equations

• f.toCoalgHom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev CoalgebraCat.ofHom {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] [Coalgebra R X] [Coalgebra R Y] (f : X →ₗc[R] Y) : of R X ⟶ of R Y

Typecheck a CoalgHom as a morphism in CoalgebraCat R.

Equations

• CoalgebraCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

theorem CoalgebraCat.Hom.toCoalgHom_injective {R : Type u} [CommRing R] (V W : CoalgebraCat R) : Function.Injective toCoalgHom'

theorem CoalgebraCat.hom_ext {R : Type u} [CommRing R] {M N : CoalgebraCat R} (f g : M ⟶ N) (h : Hom.toCoalgHom f = Hom.toCoalgHom g) : f = g

@[simp]

theorem CoalgebraCat.toCoalgHom_comp {R : Type u} [CommRing R] {M N U : CoalgebraCat R} (f : M ⟶ N) (g : N ⟶ U) : Hom.toCoalgHom (CategoryTheory.CategoryStruct.comp f g) = (Hom.toCoalgHom g).comp (Hom.toCoalgHom f)

@[simp]

theorem CoalgebraCat.toCoalgHom_id {R : Type u} [CommRing R] {M : CoalgebraCat R} : Hom.toCoalgHom (CategoryTheory.CategoryStruct.id M) = CoalgHom.id R ↑M.toModuleCat

instance CoalgebraCat.hasForgetToModule {R : Type u} [CommRing R] : CategoryTheory.HasForget₂ (CoalgebraCat R) (ModuleCat R)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CoalgebraCat.forget₂_obj {R : Type u} [CommRing R] (X : CoalgebraCat R) : (CategoryTheory.forget₂ (CoalgebraCat R) (ModuleCat R)).obj X = ModuleCat.of R ↑X.toModuleCat

@[simp]

theorem CoalgebraCat.forget₂_map {R : Type u} [CommRing R] (X Y : CoalgebraCat R) (f : X ⟶ Y) : (CategoryTheory.forget₂ (CoalgebraCat R) (ModuleCat R)).map f = ModuleCat.ofHom ↑(Hom.toCoalgHom f)

def CoalgEquiv.toCoalgebraCatIso {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] [Coalgebra R X] [Coalgebra R Y] (e : X ≃ₗc[R] Y) : CoalgebraCat.of R X ≅ CoalgebraCat.of R Y

Build an isomorphism in the category CoalgebraCat R from a CoalgEquiv.

Equations

• e.toCoalgebraCatIso = { hom := CoalgebraCat.ofHom ↑e, inv := CoalgebraCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CoalgEquiv.toCoalgebraCatIso_inv {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] [Coalgebra R X] [Coalgebra R Y] (e : X ≃ₗc[R] Y) : e.toCoalgebraCatIso.inv = CoalgebraCat.ofHom ↑e.symm

@[simp]

theorem CoalgEquiv.toCoalgebraCatIso_hom {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] [Coalgebra R X] [Coalgebra R Y] (e : X ≃ₗc[R] Y) : e.toCoalgebraCatIso.hom = CoalgebraCat.ofHom ↑e

@[simp]

theorem CoalgEquiv.toCoalgebraCatIso_refl {R : Type u} [CommRing R] {X : Type v} [AddCommGroup X] [Module R X] [Coalgebra R X] : (refl R X).toCoalgebraCatIso = CategoryTheory.Iso.refl (CoalgebraCat.of R X)

@[simp]

theorem CoalgEquiv.toCoalgebraCatIso_symm {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] [Coalgebra R X] [Coalgebra R Y] (e : X ≃ₗc[R] Y) : e.symm.toCoalgebraCatIso = e.toCoalgebraCatIso.symm

@[simp]

theorem CoalgEquiv.toCoalgebraCatIso_trans {R : Type u} [CommRing R] {X Y Z : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] [AddCommGroup Z] [Module R Z] [Coalgebra R X] [Coalgebra R Y] [Coalgebra R Z] (e : X ≃ₗc[R] Y) (f : Y ≃ₗc[R] Z) : (e.trans f).toCoalgebraCatIso = e.toCoalgebraCatIso ≪≫ f.toCoalgebraCatIso

def CategoryTheory.Iso.toCoalgEquiv {R : Type u} [CommRing R] {X Y : CoalgebraCat R} (i : X ≅ Y) : ↑X.toModuleCat ≃ₗc[R] ↑Y.toModuleCat

Build a CoalgEquiv from an isomorphism in the category CoalgebraCat R.

Equations

• i.toCoalgEquiv = { toCoalgHom := CoalgebraCat.Hom.toCoalgHom i.hom, invFun := ⇑(CoalgebraCat.Hom.toCoalgHom i.inv), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.Iso.toCoalgEquiv_toCoalgHom {R : Type u} [CommRing R] {X Y : CoalgebraCat R} (i : X ≅ Y) : ↑i.toCoalgEquiv = CoalgebraCat.Hom.toCoalgHom i.hom

@[simp]

theorem CategoryTheory.Iso.toCoalgEquiv_refl {R : Type u} [CommRing R] {X : CoalgebraCat R} : (refl X).toCoalgEquiv = CoalgEquiv.refl R ↑X.toModuleCat

@[simp]

theorem CategoryTheory.Iso.toCoalgEquiv_symm {R : Type u} [CommRing R] {X Y : CoalgebraCat R} (e : X ≅ Y) : e.symm.toCoalgEquiv = e.toCoalgEquiv.symm

@[simp]

theorem CategoryTheory.Iso.toCoalgEquiv_trans {R : Type u} [CommRing R] {X Y Z : CoalgebraCat R} (e : X ≅ Y) (f : Y ≅ Z) : (e ≪≫ f).toCoalgEquiv = e.toCoalgEquiv.trans f.toCoalgEquiv

instance CoalgebraCat.forget_reflects_isos {R : Type u} [CommRing R] : (CategoryTheory.forget (CoalgebraCat R)).ReflectsIsomorphisms