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
.
structure
BialgebraCat
(R : Type u)
[CommRing R]
extends
CategoryTheory.Bundled
:
Type (max u (v + 1))
The category of R
-bialgebras.
Instances For
Equations
- BialgebraCat.instCoeSortType = { coe := fun (x : BialgebraCat R) => ↑x.toBundled }
@[simp]
theorem
BialgebraCat.of_instBialgebra
(R : Type u)
[CommRing R]
(X : Type v)
[Ring X]
[Bialgebra R X]
:
(BialgebraCat.of R X).instBialgebra = inferInstance
@[simp]
theorem
BialgebraCat.of_α
(R : Type u)
[CommRing R]
(X : Type v)
[Ring X]
[Bialgebra R X]
:
↑(BialgebraCat.of R X).toBundled = X
@[simp]
theorem
BialgebraCat.of_str
(R : Type u)
[CommRing R]
(X : Type v)
[Ring X]
[Bialgebra R X]
:
(BialgebraCat.of R X).str = inferInstance
The object in the category of R
-bialgebras associated to an R
-bialgebra.
Equations
- BialgebraCat.of R X = BialgebraCat.mk { α := X, str := inferInstance }
Instances For
theorem
BialgebraCat.Hom.ext
{R : Type u}
:
∀ {inst : CommRing R} {V W : BialgebraCat R} {x y : V.Hom W}, x.toBialgHom = y.toBialgHom → x = y
theorem
BialgebraCat.Hom.ext_iff
{R : Type u}
:
∀ {inst : CommRing R} {V W : BialgebraCat R} {x y : V.Hom W}, x = y ↔ x.toBialgHom = y.toBialgHom
structure
BialgebraCat.Hom
{R : Type u}
[CommRing R]
(V : BialgebraCat R)
(W : BialgebraCat R)
:
Type v
A type alias for BialgHom
to avoid confusion between the categorical and
algebraic spellings of composition.
The underlying
BialgHom
Instances For
theorem
BialgebraCat.Hom.toBialgHom_injective
{R : Type u}
[CommRing R]
(V : BialgebraCat R)
(W : BialgebraCat R)
:
Function.Injective BialgebraCat.Hom.toBialgHom
Equations
- BialgebraCat.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯
theorem
BialgebraCat.hom_ext_iff
{R : Type u}
[CommRing R]
{X : BialgebraCat R}
{Y : BialgebraCat R}
{f : X ⟶ Y}
{g : X ⟶ Y}
:
theorem
BialgebraCat.hom_ext
{R : Type u}
[CommRing R]
{X : BialgebraCat R}
{Y : BialgebraCat R}
(f : X ⟶ Y)
(g : X ⟶ Y)
(h : f.toBialgHom = g.toBialgHom)
:
f = g
@[reducible, inline]
abbrev
BialgebraCat.ofHom
{R : Type u}
[CommRing R]
{X : Type v}
{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
@[simp]
theorem
BialgebraCat.toBialgHom_comp
{R : Type u}
[CommRing R]
{X : BialgebraCat R}
{Y : BialgebraCat R}
{Z : BialgebraCat R}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
(CategoryTheory.CategoryStruct.comp f g).toBialgHom = g.toBialgHom.comp f.toBialgHom
@[simp]
theorem
BialgebraCat.toBialgHom_id
{R : Type u}
[CommRing R]
{M : BialgebraCat R}
:
(CategoryTheory.CategoryStruct.id M).toBialgHom = BialgHom.id R ↑M.toBundled
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
@[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.toBundled
@[simp]
theorem
BialgebraCat.forget₂_algebra_map
{R : Type u}
[CommRing R]
(X : BialgebraCat R)
(Y : BialgebraCat R)
(f : X ⟶ Y)
:
(CategoryTheory.forget₂ (BialgebraCat R) (AlgebraCat R)).map f = ↑f.toBialgHom
Equations
- One or more equations did not get rendered due to their size.
@[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.toBundled
@[simp]
theorem
BialgebraCat.forget₂_coalgebra_map
{R : Type u}
[CommRing R]
(X : BialgebraCat R)
(Y : BialgebraCat R)
(f : X ⟶ Y)
:
(CategoryTheory.forget₂ (BialgebraCat R) (CoalgebraCat R)).map f = CoalgebraCat.ofHom ↑f.toBialgHom
def
BialgEquiv.toBialgebraCatIso
{R : Type u}
[CommRing R]
{X : Type v}
{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
@[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)
@[simp]
def
CategoryTheory.Iso.toBialgEquiv
{R : Type u}
[CommRing R]
{X : BialgebraCat R}
{Y : BialgebraCat R}
(i : X ≅ Y)
:
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
@[simp]
theorem
CategoryTheory.Iso.toBialgEquiv_toBialgHom
{R : Type u}
[CommRing R]
{X : BialgebraCat R}
{Y : BialgebraCat R}
(i : X ≅ Y)
:
↑i.toBialgEquiv = i.hom.toBialgHom
@[simp]
theorem
CategoryTheory.Iso.toBialgEquiv_refl
{R : Type u}
[CommRing R]
{X : BialgebraCat R}
:
(CategoryTheory.Iso.refl X).toBialgEquiv = BialgEquiv.refl R ↑X.toBundled
@[simp]
theorem
CategoryTheory.Iso.toBialgEquiv_symm
{R : Type u}
[CommRing R]
{X : BialgebraCat R}
{Y : BialgebraCat R}
(e : X ≅ Y)
:
e.symm.toBialgEquiv = e.toBialgEquiv.symm
@[simp]
theorem
CategoryTheory.Iso.toBialgEquiv_trans
{R : Type u}
[CommRing R]
{X : BialgebraCat R}
{Y : BialgebraCat R}
{Z : BialgebraCat R}
(e : X ≅ Y)
(f : Y ≅ Z)
:
instance
BialgebraCat.forget_reflects_isos
{R : Type u}
[CommRing R]
:
(CategoryTheory.forget (BialgebraCat R)).ReflectsIsomorphisms
Equations
- ⋯ = ⋯