The category of bialgebras over a commutative ring #

We introduce the bundled category BialgebraCat of bialgebras over a fixed commutative ring R along with the forgetful functors to CoalgebraCat and AlgebraCat.

This file mimics Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.

source

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

CoeSort (BialgebraCat R) (Type v)

Equations

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

source

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

BialgebraCat R

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

Equations

BialgebraCat.of R X = BialgebraCat.mk X

Instances For

source

@[simp]

theorem BialgebraCat.of_instRing (R : Type u) [CommRing R] (X : Type v) [Ring X] [Bialgebra R X] :

(BialgebraCat.of R X).instRing = inst✝

source

@[simp]

theorem BialgebraCat.of_instBialgebra (R : Type u) [CommRing R] (X : Type v) [Ring X] [Bialgebra R X] :

(BialgebraCat.of R X).instBialgebra = inst✝

source

@[simp]

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

(BialgebraCat.of R X).carrier = X

source

@[simp]

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

Coalgebra.comul = Coalgebra.comul

source

@[simp]

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

Coalgebra.counit = Coalgebra.counit

source

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

x = y

source

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

Function.Injective BialgebraCat.Hom.toBialgHom

source

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

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

Equations

BialgebraCat.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯

source

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

f = g

source

@[reducible, inline]

abbrev BialgebraCat.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) :

BialgebraCat.of R X ⟶ BialgebraCat.of R Y

Typecheck a BialgHom as a morphism in BialgebraCat R.

Equations

BialgebraCat.ofHom f = { toBialgHom := f }

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

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

CategoryTheory.ConcreteCategory (BialgebraCat R)

Equations

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

source

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

CategoryTheory.HasForget₂ (BialgebraCat R) (AlgebraCat R)

Equations

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

source

@[simp]

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

(CategoryTheory.forget₂ (BialgebraCat R) (AlgebraCat R)).obj X = AlgebraCat.of R X.carrier

source

@[simp]

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

(CategoryTheory.forget₂ (BialgebraCat R) (AlgebraCat R)).map f = AlgebraCat.ofHom ↑f.toBialgHom

source

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

CategoryTheory.HasForget₂ (BialgebraCat R) (CoalgebraCat R)

Equations

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

source

@[simp]

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

(CategoryTheory.forget₂ (BialgebraCat R) (CoalgebraCat R)).obj X = CoalgebraCat.of R X.carrier

source

@[simp]

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

(CategoryTheory.forget₂ (BialgebraCat R) (CoalgebraCat R)).map f = CoalgebraCat.ofHom ↑f.toBialgHom

source

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

BialgebraCat.of R X ≅ BialgebraCat.of R Y

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

Equations

e.toBialgebraCatIso = { hom := BialgebraCat.ofHom ↑e, inv := BialgebraCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source

@[simp]

theorem BialgEquiv.toBialgebraCatIso_hom_toBialgHom {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.toBialgebraCatIso.hom.toBialgHom = ↑e

source

@[simp]

theorem BialgEquiv.toBialgebraCatIso_inv_toBialgHom {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.toBialgebraCatIso.inv.toBialgHom = ↑e.symm

source

@[simp]

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

(BialgEquiv.refl R X).toBialgebraCatIso = CategoryTheory.Iso.refl (BialgebraCat.of R X)

source

@[simp]

theorem BialgEquiv.toBialgebraCatIso_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.toBialgebraCatIso = e.toBialgebraCatIso.symm

source

@[simp]

theorem BialgEquiv.toBialgebraCatIso_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).toBialgebraCatIso = e.toBialgebraCatIso ≪≫ f.toBialgebraCatIso

source

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

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

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

Equations

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

Instances For

source

@[simp]

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

↑i.toBialgEquiv = i.hom.toBialgHom

source

@[simp]

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

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

source

@[simp]

theorem CategoryTheory.Iso.toBialgEquiv_symm {R : Type u} [CommRing R] {X Y : BialgebraCat 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 : BialgebraCat R} (e : X ≅ Y) (f : Y ≅ Z) :

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

source

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

(CategoryTheory.forget (BialgebraCat R)).ReflectsIsomorphisms

Documentation

Mathlib.Algebra.Category.BialgebraCat.Basic

The category of bialgebras over a commutative ring #