The category of coalgebras over a commutative ring

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

This file mimics Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean.

structure CoalgCat (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 CoalgCat.instCoeSortType {R : Type u} [CommRing R] : CoeSort (CoalgCat R) (Type v)

Equations

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

@[simp]

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

@[reducible, inline]

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

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

Equations

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

@[simp]

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

@[simp]

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

structure CoalgCat.Hom {R : Type u} [CommRing R] (V W : CoalgCat 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 CoalgCat.Hom.ext {R : Type u} {inst✝ : CommRing R} {V W : CoalgCat R} {x y : V.Hom W} (toCoalgHom' : x.toCoalgHom' = y.toCoalgHom') : x = y

theorem CoalgCat.Hom.ext_iff {R : Type u} {inst✝ : CommRing R} {V W : CoalgCat R} {x y : V.Hom W} : x = y ↔ x.toCoalgHom' = y.toCoalgHom'

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

Equations

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

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

Equations

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

@[reducible, inline]

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

Turn a morphism in CoalgCat back into a CoalgHom.

Equations

• f.toCoalgHom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev CoalgCat.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 CoalgCat R.

Equations

• CoalgCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

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

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

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

def CoalgEquiv.toCoalgIso {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) : CoalgCat.of R X ≅ CoalgCat.of R Y

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

Equations

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

@[simp]

theorem CoalgEquiv.toCoalgIso_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.toCoalgIso.inv = CoalgCat.ofHom ↑e.symm

@[simp]

theorem CoalgEquiv.toCoalgIso_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.toCoalgIso.hom = CoalgCat.ofHom ↑e

@[simp]

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

@[simp]

theorem CoalgEquiv.toCoalgIso_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.toCoalgIso = e.toCoalgIso.symm

@[simp]

theorem CoalgEquiv.toCoalgIso_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).toCoalgIso = e.toCoalgIso ≪≫ f.toCoalgIso

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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