The category of commutative Hopf algebras over a commutative ring

This file defines the bundled category CommHopfAlgCat of commutative Hopf algebras over a fixed commutative ring R along with the forgetful functor to CommBialgCat.

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

The category of commutative R-Hopf algebras and their morphisms.

• of :: (
• X : Type v

  The underlying type.

• commRing : CommRing ↑self
• hopfAlgebra : HopfAlgebra R ↑self
• )

@[implicit_reducible]

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

Equations

• CommHopfAlgCat.instCoeSortType = { coe := CommHopfAlgCat.X }

theorem CommHopfAlgCat.coe_of (R : Type u) [CommRing R] (X : Type v) [CommRing X] [HopfAlgebra R X] : ↑{ X := X, commRing := inst✝, hopfAlgebra := inst✝¹ } = X

structure CommHopfAlgCat.Hom {R : Type u} [CommRing R] (A B : CommHopfAlgCat R) : Type v

The type of morphisms in CommHopfAlgCat R.

• hom' : ↑A →ₐc[R] ↑B

  The underlying bialgebra map.

theorem CommHopfAlgCat.Hom.ext_iff {R : Type u} {inst✝ : CommRing R} {A B : CommHopfAlgCat R} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

theorem CommHopfAlgCat.Hom.ext {R : Type u} {inst✝ : CommRing R} {A B : CommHopfAlgCat R} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance CommHopfAlgCat.instConcreteCategoryBialgHomX {R : Type u} [CommRing R] : CategoryTheory.ConcreteCategory (CommHopfAlgCat R) fun (x1 x2 : CommHopfAlgCat R) => ↑x1 →ₐc[R] ↑x2

Equations

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

@[reducible, inline]

abbrev CommHopfAlgCat.Hom.hom {R : Type u} [CommRing R] {A B : CommHopfAlgCat R} (f : A.Hom B) : ↑A →ₐc[R] ↑B

Turn a morphism in CommHopfAlgCat back into a BialgHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev CommHopfAlgCat.ofHom {R : Type u} [CommRing R] {X Y : Type v} {x✝ : CommRing X} {x✝¹ : CommRing Y} {x✝² : HopfAlgebra R X} {x✝³ : HopfAlgebra R Y} (f : X →ₐc[R] Y) : { X := X, commRing := x✝, hopfAlgebra := x✝² } ⟶ { X := Y, commRing := x✝¹, hopfAlgebra := x✝³ }

Typecheck a BialgHom as a morphism in CommHopfAlgCat R.

Equations

• CommHopfAlgCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def CommHopfAlgCat.Hom.Simps.hom {R : Type u} [CommRing R] (A B : CommHopfAlgCat R) (f : A.Hom B) : ↑A →ₐc[R] ↑B

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• CommHopfAlgCat.Hom.Simps.hom A B f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem CommHopfAlgCat.hom_id {R : Type u} [CommRing R] {A : CommHopfAlgCat R} : ↑(Hom.hom (CategoryTheory.CategoryStruct.id A)) = AlgHom.id R ↑A

theorem CommHopfAlgCat.id_apply {R : Type u} [CommRing R] (A : CommHopfAlgCat R) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id A)) a = a

@[simp]

theorem CommHopfAlgCat.hom_comp {R : Type u} [CommRing R] {A B C : CommHopfAlgCat R} (f : A ⟶ B) (g : B ⟶ C) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem CommHopfAlgCat.comp_apply {R : Type u} [CommRing R] {A B C : CommHopfAlgCat R} (f : A ⟶ B) (g : B ⟶ C) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) a = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) a)

theorem CommHopfAlgCat.hom_ext {R : Type u} [CommRing R] {A B : CommHopfAlgCat R} {f g : A ⟶ B} (hf : Hom.hom f = Hom.hom g) : f = g

theorem CommHopfAlgCat.hom_ext_iff {R : Type u} [CommRing R] {A B : CommHopfAlgCat R} {f g : A ⟶ B} : f = g ↔ Hom.hom f = Hom.hom g

@[simp]

theorem CommHopfAlgCat.hom_ofHom {R : Type u} [CommRing R] {X Y : Type v} [CommRing X] [HopfAlgebra R X] [CommRing Y] [HopfAlgebra R Y] (f : X →ₐc[R] Y) : Hom.hom (ofHom f) = f

@[simp]

theorem CommHopfAlgCat.ofHom_hom {R : Type u} [CommRing R] {A B : CommHopfAlgCat R} (f : A ⟶ B) : ofHom (Hom.hom f) = f

@[simp]

theorem CommHopfAlgCat.ofHom_id {R : Type u} [CommRing R] {X : Type v} [CommRing X] [HopfAlgebra R X] : ofHom (BialgHom.id R X) = CategoryTheory.CategoryStruct.id { X := X, commRing := inst✝, hopfAlgebra := inst✝¹ }

@[simp]

theorem CommHopfAlgCat.ofHom_comp {R : Type u} [CommRing R] {X Y Z : Type v} [CommRing X] [HopfAlgebra R X] [CommRing Y] [HopfAlgebra R Y] [CommRing Z] [HopfAlgebra R Z] (f : X →ₐc[R] Y) (g : Y →ₐc[R] Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem CommHopfAlgCat.ofHom_apply {R : Type u} [CommRing R] {X Y : Type v} [CommRing X] [HopfAlgebra R X] [CommRing Y] [HopfAlgebra R Y] (f : X →ₐc[R] Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem CommHopfAlgCat.inv_hom_apply {R : Type u} [CommRing R] {A B : CommHopfAlgCat R} (e : A ≅ B) (x : ↑A) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem CommHopfAlgCat.hom_inv_apply {R : Type u} [CommRing R] {A B : CommHopfAlgCat R} (e : A ≅ B) (x : ↑B) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) x) = x

@[implicit_reducible]

instance CommHopfAlgCat.instInhabited {R : Type u} [CommRing R] : Inhabited (CommHopfAlgCat R)

Equations

• CommHopfAlgCat.instInhabited = { default := { X := R, commRing := inst✝, hopfAlgebra := CommSemiring.toHopfAlgebra R } }

theorem CommHopfAlgCat.forget_obj {R : Type u} [CommRing R] (A : CommHopfAlgCat R) : (CategoryTheory.forget (CommHopfAlgCat R)).obj A = ↑A

@[implicit_reducible]

instance CommHopfAlgCat.instCommRingObjForgetBialgHomX {R : Type u} [CommRing R] {A : CommHopfAlgCat R} : CommRing ((CategoryTheory.forget (CommHopfAlgCat R)).obj A)

Equations

• CommHopfAlgCat.instCommRingObjForgetBialgHomX = A.commRing

@[implicit_reducible]

instance CommHopfAlgCat.instHopfAlgebraObjForgetBialgHomX {R : Type u} [CommRing R] {A : CommHopfAlgCat R} : HopfAlgebra R ((CategoryTheory.forget (CommHopfAlgCat R)).obj A)

Equations

• CommHopfAlgCat.instHopfAlgebraObjForgetBialgHomX = A.hopfAlgebra

@[implicit_reducible]

instance CommHopfAlgCat.hasForgetToCommBialgCat {R : Type u} [CommRing R] : CategoryTheory.HasForget₂ (CommHopfAlgCat R) (CommBialgCat R)

Equations

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

@[simp]

theorem CommHopfAlgCat.forget₂_commBialgCat_obj {R : Type u} [CommRing R] (A : CommHopfAlgCat R) : (CategoryTheory.forget₂ (CommHopfAlgCat R) (CommBialgCat R)).obj A = CommBialgCat.of R ↑A

@[simp]

theorem CommHopfAlgCat.forget₂_commBialgCat_map {R : Type u} [CommRing R] {A B : CommHopfAlgCat R} (f : A ⟶ B) : (CategoryTheory.forget₂ (CommHopfAlgCat R) (CommBialgCat R)).map f = CommBialgCat.ofHom (Hom.hom f)

def CommHopfAlgCat.ofIsoSelf {R : Type u} [CommRing R] (A : CommHopfAlgCat R) : { X := ↑A, commRing := instCommRingObjForgetBialgHomX, hopfAlgebra := instHopfAlgebraObjForgetBialgHomX } ≅ A

Forgetting to the underlying type and then building the bundled object returns the original Hopf algebra.

Equations

• A.ofIsoSelf = { hom := CategoryTheory.CategoryStruct.id A, inv := CategoryTheory.CategoryStruct.id A, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CommHopfAlgCat.ofIsoSelf_inv {R : Type u} [CommRing R] (A : CommHopfAlgCat R) : A.ofIsoSelf.inv = CategoryTheory.CategoryStruct.id A

@[simp]

theorem CommHopfAlgCat.ofIsoSelf_hom {R : Type u} [CommRing R] (A : CommHopfAlgCat R) : A.ofIsoSelf.hom = CategoryTheory.CategoryStruct.id A

def CommHopfAlgCat.isoMk {R : Type u} [CommRing R] {X Y : Type v} {x✝ : CommRing X} {x✝¹ : CommRing Y} {x✝² : HopfAlgebra R X} {x✝³ : HopfAlgebra R Y} (e : X ≃ₐc[R] Y) : { X := X, commRing := x✝, hopfAlgebra := x✝² } ≅ { X := Y, commRing := x✝¹, hopfAlgebra := x✝³ }

Build an isomorphism in the category CommHopfAlgCat R from a BialgEquiv between HopfAlgebras.

Equations

• CommHopfAlgCat.isoMk e = { hom := CommHopfAlgCat.ofHom ↑e, inv := CommHopfAlgCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CommHopfAlgCat.isoMk_hom {R : Type u} [CommRing R] {X Y : Type v} {x✝ : CommRing X} {x✝¹ : CommRing Y} {x✝² : HopfAlgebra R X} {x✝³ : HopfAlgebra R Y} (e : X ≃ₐc[R] Y) : (isoMk e).hom = ofHom ↑e

@[simp]

theorem CommHopfAlgCat.isoMk_inv {R : Type u} [CommRing R] {X Y : Type v} {x✝ : CommRing X} {x✝¹ : CommRing Y} {x✝² : HopfAlgebra R X} {x✝³ : HopfAlgebra R Y} (e : X ≃ₐc[R] Y) : (isoMk e).inv = ofHom ↑e.symm

def CommHopfAlgCat.ofIso {R : Type u} [CommRing R] {A B : CommHopfAlgCat R} (i : A ≅ B) : ↑A ≃ₐc[R] ↑B

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

Equations

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

theorem CommHopfAlgCat.ofIso_apply {R : Type u} [CommRing R] {A B : CommHopfAlgCat R} (i : A ≅ B) (a : ↑A) : (ofIso i) a = (CategoryTheory.ConcreteCategory.hom i.hom) a

theorem CommHopfAlgCat.ofIso_symm_apply {R : Type u} [CommRing R] {A B : CommHopfAlgCat R} (i : A ≅ B) (a : ↑B) : (ofIso i).symm a = (CategoryTheory.ConcreteCategory.hom i.inv) a

def CommHopfAlgCat.isoEquivBialgEquiv {R : Type u} [CommRing R] {X Y : Type v} [CommRing X] [HopfAlgebra R X] [CommRing Y] [HopfAlgebra R Y] : ({ X := X, commRing := inst✝, hopfAlgebra := inst✝¹ } ≅ { X := Y, commRing := inst✝², hopfAlgebra := inst✝³ }) ≃ X ≃ₐc[R] Y

Commutative Hopf algebra equivalences between HopfAlgebras are the same as isomorphisms in CommHopfAlgCat R.

Equations

• CommHopfAlgCat.isoEquivBialgEquiv = { toFun := CommHopfAlgCat.ofIso, invFun := CommHopfAlgCat.isoMk, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CommHopfAlgCat.isoEquivBialgEquiv_symm_apply {R : Type u} [CommRing R] {X Y : Type v} [CommRing X] [HopfAlgebra R X] [CommRing Y] [HopfAlgebra R Y] (e : X ≃ₐc[R] Y) : isoEquivBialgEquiv.symm e = isoMk e

@[simp]

theorem CommHopfAlgCat.isoEquivBialgEquiv_apply {R : Type u} [CommRing R] {X Y : Type v} [CommRing X] [HopfAlgebra R X] [CommRing Y] [HopfAlgebra R Y] (i : { X := X, commRing := inst✝, hopfAlgebra := inst✝¹ } ≅ { X := Y, commRing := inst✝², hopfAlgebra := inst✝³ }) : isoEquivBialgEquiv i = ofIso i

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

@[implicit_reducible]

noncomputable instance CommAlgCat.grpObjOpOf {R : Type u} [CommRing R] {A : Type u} [CommRing A] [HopfAlgebra R A] : CategoryTheory.GrpObj (Opposite.op (of R A))

Equations

• CommAlgCat.grpObjOpOf = { toMonObj := CommAlgCat.monObjOpOf, inv := (CommAlgCat.ofHom (HopfAlgebra.antipodeAlgHom R A)).op, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CommAlgCat.inv_op_of_unop_hom {R : Type u} [CommRing R] {A : Type u} [CommRing A] [HopfAlgebra R A] : Hom.hom CategoryTheory.GrpObj.inv.unop = HopfAlgebra.antipodeAlgHom R A

@[implicit_reducible]

noncomputable instance instHopfAlgebraCarrierUnopCommAlgCatOfGrpObjOpposite {R : Type u} [CommRing R] (A : (CommAlgCat R)ᵒᵖ) [CategoryTheory.GrpObj A] : HopfAlgebra R ↑(Opposite.unop A)

Equations

• instHopfAlgebraCarrierUnopCommAlgCatOfGrpObjOpposite A = HopfAlgebra.ofAlgHom (CommAlgCat.Hom.hom CategoryTheory.GrpObj.inv.unop) ⋯ ⋯

noncomputable def commHopfAlgCatEquivCogrpCommAlgCat (R : Type u) [CommRing R] : CommHopfAlgCat R ≌ (CategoryTheory.Grp (CommAlgCat R)ᵒᵖ)ᵒᵖ

Commutative Hopf algebras over a commutative ring R are the same thing as cogroup R-algebras.

Equations

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

@[simp]

theorem commHopfAlgCatEquivCogrpCommAlgCat_functor_obj_unop_X (R : Type u) [CommRing R] (A : CommHopfAlgCat R) : (Opposite.unop ((commHopfAlgCatEquivCogrpCommAlgCat R).functor.obj A)).X = Opposite.op (CommAlgCat.of R ↑A)

@[simp]

theorem commHopfAlgCatEquivCogrpCommAlgCat_inverse_obj (R : Type u) [CommRing R] (A : (CategoryTheory.Grp (CommAlgCat R)ᵒᵖ)ᵒᵖ) : (commHopfAlgCatEquivCogrpCommAlgCat R).inverse.obj A = { X := ↑(Opposite.unop (Opposite.unop A).X), commRing := CommAlgCat.instCommRingObjForgetAlgHomCarrier, hopfAlgebra := instHopfAlgebraCarrierUnopCommAlgCatOfGrpObjOpposite (Opposite.unop A).X }

@[simp]

theorem commHopfAlgCatEquivCogrpCommAlgCat_unitIso_inv_app (R : Type u) [CommRing R] (X : CommHopfAlgCat R) : (commHopfAlgCatEquivCogrpCommAlgCat R).unitIso.inv.app X = CategoryTheory.CategoryStruct.id { X := ↑X, commRing := CommAlgCat.instCommRingObjForgetAlgHomCarrier, hopfAlgebra := instHopfAlgebraCarrierUnopCommAlgCatOfGrpObjOpposite (Opposite.unop (Opposite.op { X := Opposite.op (CommAlgCat.of R ↑X), grp := CommAlgCat.grpObjOpOf })).X }

@[simp]

theorem commHopfAlgCatEquivCogrpCommAlgCat_counitIso_inv_app (R : Type u) [CommRing R] (X : (CategoryTheory.Grp (CommAlgCat R)ᵒᵖ)ᵒᵖ) : (commHopfAlgCatEquivCogrpCommAlgCat R).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem commHopfAlgCatEquivCogrpCommAlgCat_unitIso_hom_app (R : Type u) [CommRing R] (X : CommHopfAlgCat R) : (commHopfAlgCatEquivCogrpCommAlgCat R).unitIso.hom.app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem commHopfAlgCatEquivCogrpCommAlgCat_counitIso_hom_app (R : Type u) [CommRing R] (X : (CategoryTheory.Grp (CommAlgCat R)ᵒᵖ)ᵒᵖ) : (commHopfAlgCatEquivCogrpCommAlgCat R).counitIso.hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op { X := Opposite.op (CommAlgCat.of R ↑(Opposite.unop (Opposite.unop X).X)), grp := CommAlgCat.grpObjOpOf })

instance instIsCommMonObjOppositeCommAlgCatXUnopGrpObjCommHopfAlgCatFunctorCommHopfAlgCatEquivCogrpCommAlgCatOfIsCocommX {R : Type u} [CommRing R] {A : CommHopfAlgCat R} [Coalgebra.IsCocomm R ↑A] : CategoryTheory.IsCommMonObj (Opposite.unop ((commHopfAlgCatEquivCogrpCommAlgCat R).functor.obj A)).X