The category of Hopf algebras over a commutative ring #
We introduce the bundled category HopfAlgebraCat
of Hopf algebras over a fixed commutative ring
R
along with the forgetful functor to BialgebraCat
.
This file mimics Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
.
structure
HopfAlgebraCat
(R : Type u)
[CommRing R]
extends
CategoryTheory.Bundled
:
Type (max u (v + 1))
The category of R
-Hopf algebras.
- α : Type v
- str : Ring ↑self.toBundled
- instHopfAlgebra : HopfAlgebra R ↑self.toBundled
Instances For
instance
HopfAlgebraCat.instCoeSortType
{R : Type u}
[CommRing R]
:
CoeSort (HopfAlgebraCat R) (Type v)
Equations
- HopfAlgebraCat.instCoeSortType = { coe := fun (x : HopfAlgebraCat R) => ↑x.toBundled }
@[simp]
theorem
HopfAlgebraCat.of_str
(R : Type u)
[CommRing R]
(X : Type v)
[Ring X]
[HopfAlgebra R X]
:
(HopfAlgebraCat.of R X).str = inferInstance
@[simp]
theorem
HopfAlgebraCat.of_instHopfAlgebra
(R : Type u)
[CommRing R]
(X : Type v)
[Ring X]
[HopfAlgebra R X]
:
(HopfAlgebraCat.of R X).instHopfAlgebra = inferInstance
@[simp]
theorem
HopfAlgebraCat.of_α
(R : Type u)
[CommRing R]
(X : Type v)
[Ring X]
[HopfAlgebra R X]
:
↑(HopfAlgebraCat.of R X).toBundled = X
The object in the category of R
-Hopf algebras associated to an R
-Hopf algebra.
Equations
- HopfAlgebraCat.of R X = HopfAlgebraCat.mk { α := X, str := inferInstance }
Instances For
@[simp]
theorem
HopfAlgebraCat.of_comul
{R : Type u}
[CommRing R]
{X : Type v}
[Ring X]
[HopfAlgebra R X]
:
Coalgebra.comul = Coalgebra.comul
@[simp]
theorem
HopfAlgebraCat.of_counit
{R : Type u}
[CommRing R]
{X : Type v}
[Ring X]
[HopfAlgebra R X]
:
Coalgebra.counit = Coalgebra.counit
theorem
HopfAlgebraCat.Hom.ext_iff
{R : Type u}
:
∀ {inst : CommRing R} {V W : HopfAlgebraCat R} {x y : V.Hom W}, x = y ↔ x.toBialgHom = y.toBialgHom
theorem
HopfAlgebraCat.Hom.ext
{R : Type u}
:
∀ {inst : CommRing R} {V W : HopfAlgebraCat R} {x y : V.Hom W}, x.toBialgHom = y.toBialgHom → x = y
structure
HopfAlgebraCat.Hom
{R : Type u}
[CommRing R]
(V : HopfAlgebraCat R)
(W : HopfAlgebraCat 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
HopfAlgebraCat.Hom.toBialgHom_injective
{R : Type u}
[CommRing R]
(V : HopfAlgebraCat R)
(W : HopfAlgebraCat R)
:
Function.Injective HopfAlgebraCat.Hom.toBialgHom
Equations
- HopfAlgebraCat.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯
theorem
HopfAlgebraCat.hom_ext_iff
{R : Type u}
[CommRing R]
{X : HopfAlgebraCat R}
{Y : HopfAlgebraCat R}
{f : X ⟶ Y}
{g : X ⟶ Y}
:
theorem
HopfAlgebraCat.hom_ext
{R : Type u}
[CommRing R]
{X : HopfAlgebraCat R}
{Y : HopfAlgebraCat R}
(f : X ⟶ Y)
(g : X ⟶ Y)
(h : f.toBialgHom = g.toBialgHom)
:
f = g
@[reducible, inline]
abbrev
HopfAlgebraCat.ofHom
{R : Type u}
[CommRing R]
{X : Type v}
{Y : Type v}
[Ring X]
[Ring Y]
[HopfAlgebra R X]
[HopfAlgebra R Y]
(f : X →ₐc[R] Y)
:
HopfAlgebraCat.of R X ⟶ HopfAlgebraCat.of R Y
Typecheck a BialgHom
as a morphism in HopfAlgebraCat R
.
Equations
- HopfAlgebraCat.ofHom f = { toBialgHom := f }
Instances For
@[simp]
theorem
HopfAlgebraCat.toBialgHom_comp
{R : Type u}
[CommRing R]
{X : HopfAlgebraCat R}
{Y : HopfAlgebraCat R}
{Z : HopfAlgebraCat R}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
(CategoryTheory.CategoryStruct.comp f g).toBialgHom = g.toBialgHom.comp f.toBialgHom
@[simp]
theorem
HopfAlgebraCat.toBialgHom_id
{R : Type u}
[CommRing R]
{M : HopfAlgebraCat 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
HopfAlgebraCat.forget₂_bialgebra_obj
{R : Type u}
[CommRing R]
(X : HopfAlgebraCat R)
:
(CategoryTheory.forget₂ (HopfAlgebraCat R) (BialgebraCat R)).obj X = BialgebraCat.of R ↑X.toBundled
@[simp]
theorem
HopfAlgebraCat.forget₂_bialgebra_map
{R : Type u}
[CommRing R]
(X : HopfAlgebraCat R)
(Y : HopfAlgebraCat R)
(f : X ⟶ Y)
:
(CategoryTheory.forget₂ (HopfAlgebraCat R) (BialgebraCat R)).map f = BialgebraCat.ofHom f.toBialgHom
@[simp]
theorem
BialgEquiv.toHopfAlgebraCatIso_inv_toBialgHom
{R : Type u}
[CommRing R]
{X : Type v}
{Y : Type v}
[Ring X]
[Ring Y]
[HopfAlgebra R X]
[HopfAlgebra R Y]
(e : X ≃ₐc[R] Y)
:
e.toHopfAlgebraCatIso.inv.toBialgHom = ↑e.symm
@[simp]
theorem
BialgEquiv.toHopfAlgebraCatIso_hom_toBialgHom
{R : Type u}
[CommRing R]
{X : Type v}
{Y : Type v}
[Ring X]
[Ring Y]
[HopfAlgebra R X]
[HopfAlgebra R Y]
(e : X ≃ₐc[R] Y)
:
e.toHopfAlgebraCatIso.hom.toBialgHom = ↑e
def
BialgEquiv.toHopfAlgebraCatIso
{R : Type u}
[CommRing R]
{X : Type v}
{Y : Type v}
[Ring X]
[Ring Y]
[HopfAlgebra R X]
[HopfAlgebra R Y]
(e : X ≃ₐc[R] Y)
:
HopfAlgebraCat.of R X ≅ HopfAlgebraCat.of R Y
Build an isomorphism in the category HopfAlgebraCat R
from a
BialgEquiv
.
Equations
- e.toHopfAlgebraCatIso = { hom := HopfAlgebraCat.ofHom ↑e, inv := HopfAlgebraCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
theorem
BialgEquiv.toHopfAlgebraCatIso_refl
{R : Type u}
[CommRing R]
{X : Type v}
[Ring X]
[HopfAlgebra R X]
:
(BialgEquiv.refl R X).toHopfAlgebraCatIso = CategoryTheory.Iso.refl (HopfAlgebraCat.of R X)
@[simp]
theorem
BialgEquiv.toHopfAlgebraCatIso_symm
{R : Type u}
[CommRing R]
{X : Type v}
{Y : Type v}
[Ring X]
[Ring Y]
[HopfAlgebra R X]
[HopfAlgebra R Y]
(e : X ≃ₐc[R] Y)
:
e.symm.toHopfAlgebraCatIso = e.toHopfAlgebraCatIso.symm
@[simp]
theorem
BialgEquiv.toHopfAlgebraCatIso_trans
{R : Type u}
[CommRing R]
{X : Type v}
{Y : Type v}
{Z : Type v}
[Ring X]
[Ring Y]
[Ring Z]
[HopfAlgebra R X]
[HopfAlgebra R Y]
[HopfAlgebra R Z]
(e : X ≃ₐc[R] Y)
(f : Y ≃ₐc[R] Z)
:
def
CategoryTheory.Iso.toHopfAlgEquiv
{R : Type u}
[CommRing R]
{X : HopfAlgebraCat R}
{Y : HopfAlgebraCat R}
(i : X ≅ Y)
:
Build a BialgEquiv
from an isomorphism in the category
HopfAlgebraCat R
.
Equations
- i.toHopfAlgEquiv = { toCoalgHom := i.hom.toBialgHom.toCoalgHom, invFun := ⇑i.inv.toBialgHom, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom
{R : Type u}
[CommRing R]
{X : HopfAlgebraCat R}
{Y : HopfAlgebraCat R}
(i : X ≅ Y)
:
↑i.toHopfAlgEquiv = i.hom.toBialgHom
@[simp]
theorem
CategoryTheory.Iso.toHopfAlgEquiv_refl
{R : Type u}
[CommRing R]
{X : HopfAlgebraCat R}
:
(CategoryTheory.Iso.refl X).toHopfAlgEquiv = BialgEquiv.refl R ↑X.toBundled
@[simp]
theorem
CategoryTheory.Iso.toHopfAlgEquiv_symm
{R : Type u}
[CommRing R]
{X : HopfAlgebraCat R}
{Y : HopfAlgebraCat R}
(e : X ≅ Y)
:
e.symm.toHopfAlgEquiv = e.toHopfAlgEquiv.symm
@[simp]
theorem
CategoryTheory.Iso.toHopfAlgEquiv_trans
{R : Type u}
[CommRing R]
{X : HopfAlgebraCat R}
{Y : HopfAlgebraCat R}
{Z : HopfAlgebraCat R}
(e : X ≅ Y)
(f : Y ≅ Z)
:
instance
HopfAlgebraCat.forget_reflects_isos
{R : Type u}
[CommRing R]
:
(CategoryTheory.forget (HopfAlgebraCat R)).ReflectsIsomorphisms
Equations
- ⋯ = ⋯