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.

source

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

source

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

CoeSort (HopfAlgebraCat R) (Type v)

Equations

HopfAlgebraCat.instCoeSortType = { coe := fun (x : HopfAlgebraCat R) => ↑x.toBundled }

source

@[simp]

theorem HopfAlgebraCat.of_α (R : Type u) [CommRing R] (X : Type v) [Ring X] [HopfAlgebra R X] :

↑(HopfAlgebraCat.of R X).toBundled = X

source

@[simp]

theorem HopfAlgebraCat.of_str (R : Type u) [CommRing R] (X : Type v) [Ring X] [HopfAlgebra R X] :

(HopfAlgebraCat.of R X).str = inferInstance

source

@[simp]

theorem HopfAlgebraCat.of_instHopfAlgebra (R : Type u) [CommRing R] (X : Type v) [Ring X] [HopfAlgebra R X] :

(HopfAlgebraCat.of R X).instHopfAlgebra = inferInstance

source

def HopfAlgebraCat.of (R : Type u) [CommRing R] (X : Type v) [Ring X] [HopfAlgebra R X] :

HopfAlgebraCat R

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

source

@[simp]

theorem HopfAlgebraCat.of_comul {R : Type u} [CommRing R] {X : Type v} [Ring X] [HopfAlgebra R X] :

Coalgebra.comul = Coalgebra.comul

source

@[simp]

theorem HopfAlgebraCat.of_counit {R : Type u} [CommRing R] {X : Type v} [Ring X] [HopfAlgebra R X] :

Coalgebra.counit = Coalgebra.counit

source

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

source

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

source

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.

toBialgHom : ↑V.toBundled →ₐc[R] ↑W.toBundled
The underlying BialgHom.

Instances For

source

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

Function.Injective HopfAlgebraCat.Hom.toBialgHom

source

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

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

Equations

HopfAlgebraCat.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯

source

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

source

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

source

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

source

@[simp]

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

(CategoryTheory.CategoryStruct.id M).toBialgHom = BialgHom.id R ↑M.toBundled

source

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

CategoryTheory.ConcreteCategory (HopfAlgebraCat R)

Equations

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

source

instance HopfAlgebraCat.hasForgetToBialgebra {R : Type u} [CommRing R] :

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

Equations

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

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

source

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

↑X.toBundled ≃ₐc[R] ↑Y.toBundled

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

Equations

i.toHopfAlgEquiv = let __src := i.hom.toBialgHom; { toCoalgHom := __src.toCoalgHom, invFun := ⇑i.inv.toBialgHom, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }