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 : 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

@[simp]

theorem CoalgebraCat.of_instCoalgebra (R : Type u) [CommRing R] (X : Type v) [AddCommGroup X] [Module R X] [Coalgebra R X] : (CoalgebraCat.of R X).instCoalgebra = inferInstance

@[simp]

theorem CoalgebraCat.of_carrier (R : Type u) [CommRing R] (X : Type v) [AddCommGroup X] [Module R X] [Coalgebra R X] : ↑(CoalgebraCat.of R X).toModuleCat = X

@[simp]

theorem CoalgebraCat.of_isAddCommGroup (R : Type u) [CommRing R] (X : Type v) [AddCommGroup X] [Module R X] [Coalgebra R X] : (CoalgebraCat.of R X).isAddCommGroup = inst✝²

@[simp]

theorem CoalgebraCat.of_isModule (R : Type u) [CommRing R] (X : Type v) [AddCommGroup X] [Module R X] [Coalgebra R X] : (CoalgebraCat.of R X).isModule = inst✝¹

def 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.mk X, instCoalgebra := inferInstance }

@[simp]

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

@[simp]

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

theorem CoalgebraCat.Hom.ext_iff {R : Type u} : ∀ {inst : CommRing R} {V W : CoalgebraCat R} {x y : V.Hom W}, x = y ↔ x.toCoalgHom = y.toCoalgHom

theorem CoalgebraCat.Hom.ext {R : Type u} : ∀ {inst : CommRing R} {V W : CoalgebraCat R} {x y : V.Hom W}, x.toCoalgHom = y.toCoalgHom → x = y

structure CoalgebraCat.Hom {R : Type u} [CommRing R] (V : CoalgebraCat R) (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.toCoalgHom_injective {R : Type u} [CommRing R] (V : CoalgebraCat R) (W : CoalgebraCat R) : Function.Injective CoalgebraCat.Hom.toCoalgHom

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

Equations

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

theorem CoalgebraCat.hom_ext_iff {R : Type u} [CommRing R] {M : CoalgebraCat R} {N : CoalgebraCat R} {f : M ⟶ N} {g : M ⟶ N} : f = g ↔ f.toCoalgHom = g.toCoalgHom

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

@[reducible, inline]

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

Typecheck a CoalgHom as a morphism in CoalgebraCat R.

Equations

• CoalgebraCat.ofHom f = { toCoalgHom := f }

@[simp]

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

@[simp]

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

instance CoalgebraCat.concreteCategory {R : Type u} [CommRing R] : CategoryTheory.ConcreteCategory (CoalgebraCat R)

Equations

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

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 : CoalgebraCat R) (Y : CoalgebraCat R) (f : X ⟶ Y) : (CategoryTheory.forget₂ (CoalgebraCat R) (ModuleCat R)).map f = ↑f.toCoalgHom

@[simp]

theorem CoalgEquiv.toCoalgebraCatIso_hom_toCoalgHom {R : Type u} [CommRing R] {X : Type v} {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.toCoalgHom = ↑e

@[simp]

theorem CoalgEquiv.toCoalgebraCatIso_inv_toCoalgHom {R : Type u} [CommRing R] {X : Type v} {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.toCoalgHom = ↑e.symm

def CoalgEquiv.toCoalgebraCatIso {R : Type u} [CommRing R] {X : Type v} {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_refl {R : Type u} [CommRing R] {X : Type v} [AddCommGroup X] [Module R X] [Coalgebra R X] : (CoalgEquiv.refl R X).toCoalgebraCatIso = CategoryTheory.Iso.refl (CoalgebraCat.of R X)

@[simp]

theorem CoalgEquiv.toCoalgebraCatIso_symm {R : Type u} [CommRing R] {X : Type v} {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 : Type v} {Y : Type v} {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 : CoalgebraCat R} {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 := i.hom.toCoalgHom, invFun := ⇑i.inv.toCoalgHom, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Iso.toCoalgEquiv_trans {R : Type u} [CommRing R] {X : CoalgebraCat R} {Y : CoalgebraCat R} {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

Equations

• ⋯ = ⋯