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.

source

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

Instances For

source

instance CoalgebraCat.instCoeSortType {R : Type u} [CommRing R] :

CoeSort (CoalgebraCat R) (Type v)

Equations

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

source

@[simp]

theorem CoalgebraCat.moduleCat_of_toModuleCat {R : Type u} [CommRing R] (X : CoalgebraCat R) :

ModuleCat.of R ↑X.toModuleCat = X.toModuleCat

source

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

Instances For

source

@[simp]

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

(of R X).instCoalgebra = inferInstance

source

@[simp]

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

↑(of R X).toModuleCat = X

source

@[simp]

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

(of R X).isAddCommGroup = inst✝

source

@[simp]

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

(of R X).isModule = inst✝

source

@[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

source

@[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

source

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

Instances For

source

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

source

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

Function.Injective toCoalgHom

source

instance CoalgebraCat.category {R : Type u} [CommRing R] :

CategoryTheory.Category.{v, max (v + 1) u} (CoalgebraCat R)

Equations

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

source

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

f = g

source

@[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 = { toCoalgHom := f }

Instances For

source

@[simp]

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

(CategoryTheory.CategoryStruct.comp f g).toCoalgHom = g.toCoalgHom.comp f.toCoalgHom

source

@[simp]

theorem CoalgebraCat.toCoalgHom_id {R : Type u} [CommRing R] {M : CoalgebraCat R} :

(CategoryTheory.CategoryStruct.id M).toCoalgHom = CoalgHom.id R ↑M.toModuleCat

source

instance CoalgebraCat.hasForget {R : Type u} [CommRing R] :

CategoryTheory.HasForget (CoalgebraCat R)

Equations

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

source

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.

source

@[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

source

@[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 ↑f.toCoalgHom

source

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 := ⋯ }

Instances For

source

@[simp]

theorem CoalgEquiv.toCoalgebraCatIso_inv_toCoalgHom {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.toCoalgHom = ↑e.symm

source

@[simp]

theorem CoalgEquiv.toCoalgebraCatIso_hom_toCoalgHom {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.toCoalgHom = ↑e

source

@[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)

source

@[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

source

@[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

source

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 := i.hom.toCoalgHom, invFun := ⇑i.inv.toCoalgHom, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

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

↑i.toCoalgEquiv = i.hom.toCoalgHom

source

@[simp]

theorem CategoryTheory.Iso.toCoalgEquiv_refl {R : Type u} [CommRing R] {X : CoalgebraCat R} :

(refl X).toCoalgEquiv = CoalgEquiv.refl R ↑X.toModuleCat

source

@[simp]

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

e.symm.toCoalgEquiv = e.toCoalgEquiv.symm

source

@[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

source

instance CoalgebraCat.forget_reflects_isos {R : Type u} [CommRing R] :

(CategoryTheory.forget (CoalgebraCat R)).ReflectsIsomorphisms

Documentation

Mathlib.Algebra.Category.CoalgebraCat.Basic

The category of coalgebras over a commutative ring #