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 Ring : Type (max u (v + 1))

The category of R-Hopf algebras.

• α : Type v
• str : Ring ↑self.toBundled
• instHopfAlgebra : HopfAlgebra R ↑self.toBundled

instance HopfAlgebraCat.instCoeSortType {R : Type u} [CommRing R] : CoeSort (HopfAlgebraCat R) (Type v)

Equations

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

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 }

@[simp]

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

@[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_str (R : Type u) [CommRing R] (X : Type v) [Ring X] [HopfAlgebra R X] : (HopfAlgebraCat.of R X).str = inferInstance

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

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

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

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

instance HopfAlgebraCat.category {R : Type u} [CommRing R] : CategoryTheory.Category.{v, max (v + 1) u} (HopfAlgebraCat R)

Equations

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

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

@[reducible, inline]

abbrev HopfAlgebraCat.ofHom {R : Type u} [CommRing R] {X 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 }

@[simp]

theorem HopfAlgebraCat.toBialgHom_comp {R : Type u} [CommRing R] {X Y 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

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.

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.

@[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 Y : HopfAlgebraCat R) (f : X ⟶ Y) : (CategoryTheory.forget₂ (HopfAlgebraCat R) (BialgebraCat R)).map f = BialgebraCat.ofHom f.toBialgHom

def BialgEquiv.toHopfAlgebraCatIso {R : Type u} [CommRing R] {X 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 := ⋯ }

@[simp]

theorem BialgEquiv.toHopfAlgebraCatIso_inv_toBialgHom {R : Type u} [CommRing R] {X 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 Y : Type v} [Ring X] [Ring Y] [HopfAlgebra R X] [HopfAlgebra R Y] (e : X ≃ₐc[R] Y) : e.toHopfAlgebraCatIso.hom.toBialgHom = ↑e

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

def CategoryTheory.Iso.toHopfAlgEquiv {R : Type u} [CommRing R] {X 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 = { toCoalgHom := i.hom.toBialgHom.toCoalgHom, invFun := ⇑i.inv.toBialgHom, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom {R : Type u} [CommRing R] {X 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 Y : HopfAlgebraCat R} (e : X ≅ Y) : e.symm.toHopfAlgEquiv = e.toHopfAlgEquiv.symm

@[simp]

theorem CategoryTheory.Iso.toHopfAlgEquiv_trans {R : Type u} [CommRing R] {X Y Z : HopfAlgebraCat R} (e : X ≅ Y) (f : Y ≅ Z) : (e ≪≫ f).toHopfAlgEquiv = e.toHopfAlgEquiv.trans f.toHopfAlgEquiv

instance HopfAlgebraCat.forget_reflects_isos {R : Type u} [CommRing R] : (CategoryTheory.forget (HopfAlgebraCat R)).ReflectsIsomorphisms

Equations

• ⋯ = ⋯