The category of Hopf algebras over a commutative ring

We introduce the bundled category HopfAlgCat of Hopf algebras over a fixed commutative ring R along with the forgetful functor to BialgCat.

This file mimics Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean.

structure HopfAlgCat (R : Type u) [CommRing R] : Type (max u (v + 1))

The category of R-Hopf algebras.

• carrier : Type v

  The underlying type.

• instRing : Ring self.carrier
• instHopfAlgebra : HopfAlgebra R self.carrier

@[implicit_reducible]

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

@[reducible, inline]

abbrev HopfAlgCat.of (R : Type u) [CommRing R] (X : Type v) [Ring X] [HopfAlgebra R X] : HopfAlgCat R

The object in the category of R-Hopf algebras associated to an R-Hopf algebra.

@[simp]

theorem HopfAlgCat.of_comul {R : Type u} [CommRing R] {X : Type v} [Ring X] [HopfAlgebra R X] : CoalgebraStruct.comul = CoalgebraStruct.comul

@[simp]

theorem HopfAlgCat.of_counit {R : Type u} [CommRing R] {X : Type v} [Ring X] [HopfAlgebra R X] : CoalgebraStruct.counit = CoalgebraStruct.counit

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

theorem HopfAlgCat.Hom.ext_iff {R : Type u} {inst✝ : CommRing R} {V W : HopfAlgCat R} {x y : V.Hom W} : x = y ↔ x.toBialgHom' = y.toBialgHom'

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

@[implicit_reducible]

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

@[implicit_reducible]

instance HopfAlgCat.concreteCategory {R : Type u} [CommRing R] : CategoryTheory.ConcreteCategory (HopfAlgCat R) fun (x1 x2 : HopfAlgCat R) => x1.carrier →ₐc[R] x2.carrier

@[reducible, inline]

abbrev HopfAlgCat.Hom.toBialgHom {R : Type u} [CommRing R] {X Y : HopfAlgCat R} (f : X.Hom Y) : X.carrier →ₐc[R] Y.carrier

Turn a morphism in HopfAlgCat back into a BialgHom.

@[reducible, inline]

abbrev HopfAlgCat.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) : of R X ⟶ of R Y

Typecheck a BialgHom as a morphism in HopfAlgCat R.

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

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

theorem HopfAlgCat.hom_ext_iff {R : Type u} [CommRing R] {X Y : HopfAlgCat R} {f g : X ⟶ Y} : f = g ↔ Hom.toBialgHom f = Hom.toBialgHom g

@[simp]

theorem HopfAlgCat.toBialgHom_comp {R : Type u} [CommRing R] {X Y Z : HopfAlgCat R} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.toBialgHom (CategoryTheory.CategoryStruct.comp f g) = (Hom.toBialgHom g).comp (Hom.toBialgHom f)

@[simp]

theorem HopfAlgCat.toBialgHom_id {R : Type u} [CommRing R] {M : HopfAlgCat R} : Hom.toBialgHom (CategoryTheory.CategoryStruct.id M) = BialgHom.id R M.carrier

@[implicit_reducible]

instance HopfAlgCat.hasForgetToBialgebra {R : Type u} [CommRing R] : CategoryTheory.HasForget₂ (HopfAlgCat R) (BialgCat R)

@[simp]

theorem HopfAlgCat.forget₂_bialgebra_obj {R : Type u} [CommRing R] (X : HopfAlgCat R) : (CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj X = BialgCat.of R X.carrier

@[simp]

theorem HopfAlgCat.forget₂_bialgebra_map {R : Type u} [CommRing R] (X Y : HopfAlgCat R) (f : X ⟶ Y) : (CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).map f = BialgCat.ofHom (Hom.toBialgHom f)

def BialgEquiv.toHopfAlgIso {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Ring Y] [HopfAlgebra R X] [HopfAlgebra R Y] (e : X ≃ₐc[R] Y) : HopfAlgCat.of R X ≅ HopfAlgCat.of R Y

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

@[simp]

theorem BialgEquiv.toHopfAlgIso_hom {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.toHopfAlgIso.hom = HopfAlgCat.ofHom ↑e

@[simp]

theorem BialgEquiv.toHopfAlgIso_inv {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.toHopfAlgIso.inv = HopfAlgCat.ofHom ↑e.symm

@[simp]

theorem BialgEquiv.toHopfAlgIso_refl {R : Type u} [CommRing R] {X : Type v} [Ring X] [HopfAlgebra R X] : (refl R X).toHopfAlgIso = CategoryTheory.Iso.refl (HopfAlgCat.of R X)

@[simp]

theorem BialgEquiv.toHopfAlgIso_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.toHopfAlgIso = e.toHopfAlgIso.symm

@[simp]

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

def CategoryTheory.Iso.toHopfAlgEquiv {R : Type u} [CommRing R] {X Y : HopfAlgCat R} (i : X ≅ Y) : X.carrier ≃ₐc[R] Y.carrier

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

@[simp]

theorem CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom {R : Type u} [CommRing R] {X Y : HopfAlgCat R} (i : X ≅ Y) : ↑i.toHopfAlgEquiv = i.hom.toBialgHom'

@[simp]

theorem CategoryTheory.Iso.toHopfAlgEquiv_refl {R : Type u} [CommRing R] {X : HopfAlgCat R} : (refl X).toHopfAlgEquiv = BialgEquiv.refl R X.carrier

@[simp]

theorem CategoryTheory.Iso.toHopfAlgEquiv_symm {R : Type u} [CommRing R] {X Y : HopfAlgCat R} (e : X ≅ Y) : e.symm.toHopfAlgEquiv = e.toHopfAlgEquiv.symm

@[simp]

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

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