The category of bialgebras over a commutative ring #

We introduce the bundled category BialgCat of bialgebras over a fixed commutative ring R along with the forgetful functors to CoalgCat and AlgCat.

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

source

structure BialgCat (R : Type u) [CommRing R] :

Type (max u (v + 1))

The category of R-bialgebras.

carrier : Type v
The underlying type.
instRing : Ring self.carrier
instBialgebra : Bialgebra R self.carrier

Instances For

source

@[instance_reducible]

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

CoeSort (BialgCat R) (Type v)

Equations

BialgCat.instCoeSortType = { coe := fun (x : BialgCat R) => x.carrier }

source

def BialgCat.of (R : Type u) [CommRing R] (X : Type v) [Ring X] [Bialgebra R X] :

BialgCat R

The object in the category of R-bialgebras associated to an R-bialgebra.

Equations

↧X = { carrier := X, instRing := inst✝¹, instBialgebra := inst✝ }

Instances For

source

@[simp]

theorem BialgCat.of_carrier (R : Type u) [CommRing R] (X : Type v) [Ring X] [Bialgebra R X] :

(↧X).carrier = X

source

def BialgCat.delabOf :

Lean.PrettyPrinter.Delaborator.Delab

This prints BialgCat.of R X as ↧X.

Equations

BialgCat.delabOf = CategoryTheory.delabOf

Instances For

source

@[simp]

theorem BialgCat.of_comul {R : Type u} [CommRing R] {X : Type v} [Ring X] [Bialgebra R X] :

CoalgebraStruct.comul = CoalgebraStruct.comul

source

@[simp]

theorem BialgCat.of_counit {R : Type u} [CommRing R] {X : Type v} [Ring X] [Bialgebra R X] :

CoalgebraStruct.counit = CoalgebraStruct.counit

source

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

Type v

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

toBialgHom' : V.carrier →ₐc[R] W.carrier
The underlying BialgHom

Instances For

source

theorem BialgCat.Hom.ext_iff {R : Type u} {inst✝ : CommRing R} {V W : BialgCat R} {x y : V.Hom W} :

x = y ↔ x.toBialgHom' = y.toBialgHom'

source

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

x = y

source

@[instance_reducible]

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

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

Equations

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

source

@[instance_reducible]

instance BialgCat.concreteCategory {R : Type u} [CommRing R] :

CategoryTheory.ConcreteCategory (BialgCat R) fun (x1 x2 : BialgCat R) => x1.carrier →ₐc[R] x2.carrier

Equations

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

source

@[reducible, inline]

abbrev BialgCat.Hom.toBialgHom {R : Type u} [CommRing R] {X Y : BialgCat R} (f : X.Hom Y) :

X.carrier →ₐc[R] Y.carrier

Turn a morphism in BialgCat back into a BialgHom.

Equations

f.toBialgHom = CategoryTheory.ConcreteCategory.hom f

Instances For

source

@[reducible, inline]

abbrev BialgCat.ofHom {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (f : X →ₐc[R] Y) :

↧X ⟶ ↧Y

Typecheck a BialgHom as a morphism in BialgCat R.

Equations

BialgCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

Instances For

source

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

Function.Injective toBialgHom

source

theorem BialgCat.hom_ext {R : Type u} [CommRing R] {X Y : BialgCat R} (f g : X ⟶ Y) (h : Hom.toBialgHom f = Hom.toBialgHom g) :

f = g

source

theorem BialgCat.hom_ext_iff {R : Type u} [CommRing R] {X Y : BialgCat R} {f g : X ⟶ Y} :

f = g ↔ Hom.toBialgHom f = Hom.toBialgHom g

source

@[simp]

theorem BialgCat.toBialgHom_comp {R : Type u} [CommRing R] {X Y Z : BialgCat R} (f : X ⟶ Y) (g : Y ⟶ Z) :

Hom.toBialgHom (CategoryTheory.CategoryStruct.comp f g) = (Hom.toBialgHom g).comp (Hom.toBialgHom f)

source

@[simp]

theorem BialgCat.toBialgHom_id {R : Type u} [CommRing R] {M : BialgCat R} :

Hom.toBialgHom (CategoryTheory.CategoryStruct.id M) = BialgHom.id R M.carrier

source

@[instance_reducible]

instance BialgCat.hasForgetToAlgebra {R : Type u} [CommRing R] :

CategoryTheory.HasForget₂ (BialgCat R) (AlgCat R)

Equations

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

source

@[simp]

theorem BialgCat.forget₂_algebra_obj {R : Type u} [CommRing R] (X : BialgCat R) :

(CategoryTheory.forget₂ (BialgCat R) (AlgCat R)).obj X = ↧X.carrier

source

@[simp]

theorem BialgCat.forget₂_algebra_map {R : Type u} [CommRing R] (X Y : BialgCat R) (f : X ⟶ Y) :

(CategoryTheory.forget₂ (BialgCat R) (AlgCat R)).map f = AlgCat.ofHom ↑(Hom.toBialgHom f)

source

@[instance_reducible]

instance BialgCat.hasForgetToCoalgebra {R : Type u} [CommRing R] :

CategoryTheory.HasForget₂ (BialgCat R) (CoalgCat R)

Equations

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

source

@[simp]

theorem BialgCat.forget₂_coalgebra_obj {R : Type u} [CommRing R] (X : BialgCat R) :

(CategoryTheory.forget₂ (BialgCat R) (CoalgCat R)).obj X = ↧X.carrier

source

@[simp]

theorem BialgCat.forget₂_coalgebra_map {R : Type u} [CommRing R] (X Y : BialgCat R) (f : X ⟶ Y) :

(CategoryTheory.forget₂ (BialgCat R) (CoalgCat R)).map f = CoalgCat.ofHom ↑(Hom.toBialgHom f)

source

def BialgEquiv.toBialgIso {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (e : X ≃ₐc[R] Y) :

↧X ≅ ↧Y

Build an isomorphism in the category BialgCat R from a BialgEquiv.

Equations

e.toBialgIso = { hom := BialgCat.ofHom ↑e, inv := BialgCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source

@[simp]

theorem BialgEquiv.toBialgIso_inv {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (e : X ≃ₐc[R] Y) :

e.toBialgIso.inv = BialgCat.ofHom ↑e.symm

source

@[simp]

theorem BialgEquiv.toBialgIso_hom {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (e : X ≃ₐc[R] Y) :

e.toBialgIso.hom = BialgCat.ofHom ↑e

source

@[simp]

theorem BialgEquiv.toBialgIso_refl {R : Type u} [CommRing R] {X : Type v} [Ring X] [Bialgebra R X] :

(refl R X).toBialgIso = CategoryTheory.Iso.refl ↧X

source

@[simp]

theorem BialgEquiv.toBialgIso_symm {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (e : X ≃ₐc[R] Y) :

e.symm.toBialgIso = e.toBialgIso.symm

source

@[simp]

theorem BialgEquiv.toBialgIso_trans {R : Type u} [CommRing R] {X Y Z : Type v} [Ring X] [Ring Y] [Ring Z] [Bialgebra R X] [Bialgebra R Y] [Bialgebra R Z] (e : X ≃ₐc[R] Y) (f : Y ≃ₐc[R] Z) :

(e.trans f).toBialgIso = e.toBialgIso ≪≫ f.toBialgIso

source

def CategoryTheory.Iso.toBialgEquiv {R : Type u} [CommRing R] {X Y : BialgCat R} (i : X ≅ Y) :

X.carrier ≃ₐc[R] Y.carrier

Build a BialgEquiv from an isomorphism in the category BialgCat R.

Equations

i.toBialgEquiv = { toCoalgHom := (BialgCat.Hom.toBialgHom i.hom).toCoalgHom, invFun := ⇑(BialgCat.Hom.toBialgHom i.inv), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source

@[simp]

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

↑i.toBialgEquiv = i.hom.toBialgHom'

source

@[simp]

theorem CategoryTheory.Iso.toBialgEquiv_refl {R : Type u} [CommRing R] {X : BialgCat R} :

(refl X).toBialgEquiv = BialgEquiv.refl R X.carrier

source

@[simp]

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

e.symm.toBialgEquiv = e.toBialgEquiv.symm

source

@[simp]

theorem CategoryTheory.Iso.toBialgEquiv_trans {R : Type u} [CommRing R] {X Y Z : BialgCat R} (e : X ≅ Y) (f : Y ≅ Z) :

(e ≪≫ f).toBialgEquiv = e.toBialgEquiv.trans f.toBialgEquiv

source

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

(CategoryTheory.forget (BialgCat R)).ReflectsIsomorphisms

Documentation

Mathlib.Algebra.Category.BialgCat.Basic

The category of bialgebras over a commutative ring #