Hopf subalgebras

A subalgebra A of a Hopf algebra H over R is a Hopf subalgebra when comultiplication maps A into the image of A ⊗[R] A in H ⊗[R] H and the antipode maps A into itself. When H and A are flat over R (for instance over a field), the map A ⊗[R] A → H ⊗[R] H is injective, so the comultiplication, counit and antipode of H restrict to a Hopf algebra structure on A for which the inclusion is a morphism of bialgebras.

For commutative H, the inclusion of a Hopf subalgebra A is the coordinate map of a homomorphism of affine groups Spec H → Spec A; over a field, the Hopf subalgebras are exactly the coordinate rings of the quotients of Spec H (Waterhouse, §16.3). This file packages A as an object of CommHopfAlgCat together with the inclusion morphism, and proves the universal property: a morphism of commutative Hopf algebras into H factors, necessarily uniquely, through the inclusion exactly when its image lies in A.

For A : Subalgebra R H, state the predicate as A.IsHopfSubalgebra. Given hA : A.IsHopfSubalgebra, use hA.toSubcoalgebra for the underlying subcoalgebra. Under the flatness hypotheses, hA.hopfAlgebra supplies the restricted Hopf structure and hA.valBialgHom its inclusion. For a bialgebra homomorphism f : K →ₐc[R] H with hf : ∀ x, f x ∈ A, hA.codRestrict f hf is the corestriction to A; hA.coe_codRestrict_apply f hf x identifies its value in H with f x.

Install the restricted structure locally with letI : HopfAlgebra R A := hA.hopfAlgebra. Then hA.comul_apply x, hA.counit_apply x, and hA.coe_antipode_apply x identify its operations with the restricted comultiplication, ambient counit, and ambient antipode.

Main declarations

• Subalgebra.IsHopfSubalgebra: a subalgebra stable under comultiplication and the antipode.
• Subalgebra.IsHopfSubalgebra.hopfAlgebra: the restricted Hopf algebra structure, under flatness.
• TauCeti.CommHopfAlgCat.ofHopfSubalgebra: a Hopf subalgebra as a bundled commutative Hopf algebra.
• TauCeti.CommHopfAlgCat.hopfSubalgebraι: the inclusion morphism, a bialgebra morphism which commutes with the antipodes and is injective, hence a monomorphism.
• TauCeti.CommHopfAlgCat.liftHopfSubalgebra: the factorization of a morphism with image in the Hopf subalgebra, with TauCeti.CommHopfAlgCat.exists_comp_hopfSubalgebraι_iff.

References

• M. E. Sweedler, Hopf Algebras (1969), §4.1.
• W. C. Waterhouse, Introduction to Affine Group Schemes (1979), §§15.1 and 16.3.

structure Subalgebra.IsHopfSubalgebra {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (A : Subalgebra R H) : Prop

A subalgebra A of a Hopf algebra H is a Hopf subalgebra when comultiplication maps it into the image of A ⊗[R] A and the antipode maps it into itself.

• comul_mem ⦃x : H⦄ : x ∈ A → CoalgebraStruct.comul x ∈ (TensorProduct.map (toSubmodule A).subtype (toSubmodule A).subtype).range

  The comultiplication of an element of A lies in the image of A ⊗[R] A.

• antipode_mem ⦃x : H⦄ : x ∈ A → (HopfAlgebraStruct.antipode R) x ∈ A

  The antipode maps A into itself.

@[reducible, inline]

abbrev Subalgebra.IsHopfSubalgebra.toSubcoalgebra {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {A : Subalgebra R H} (hA : A.IsHopfSubalgebra) : TauCeti.Subcoalgebra R H

The underlying subcoalgebra of a Hopf subalgebra.

Equations

• hA.toSubcoalgebra = { carrier := Subalgebra.toSubmodule A, comul_mem' := ⋯ }

noncomputable def Subalgebra.IsHopfSubalgebra.comulAlgHom {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {A : Subalgebra R H} (hA : A.IsHopfSubalgebra) [Module.Flat R H] [Module.Flat R ↥A] : ↥A →ₐ[R] TensorProduct R ↥A ↥A

The comultiplication of a Hopf subalgebra, valued in its own tensor square: the unique preimage of the comultiplication of H under the injective map A ⊗[R] A → H ⊗[R] H.

Equations

• hA.comulAlgHom = AlgHom.ofLinearMap hA.toSubcoalgebra.comulLinearMap ⋯ ⋯

@[simp]

theorem Subalgebra.IsHopfSubalgebra.map_val_comulAlgHom {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {A : Subalgebra R H} (hA : A.IsHopfSubalgebra) [Module.Flat R H] [Module.Flat R ↥A] (x : ↥A) : (Algebra.TensorProduct.map A.val A.val) (hA.comulAlgHom x) = CoalgebraStruct.comul ↑x

The comultiplication of a Hopf subalgebra is the restriction of that of H.

def Subalgebra.IsHopfSubalgebra.antipode {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {A : Subalgebra R H} (hA : A.IsHopfSubalgebra) : ↥A →ₗ[R] ↥A

The restriction of the antipode of H to a Hopf subalgebra.

Equations

• hA.antipode = (HopfAlgebraStruct.antipode R).restrict ⋯

@[simp]

theorem Subalgebra.IsHopfSubalgebra.coe_antipode {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {A : Subalgebra R H} (hA : A.IsHopfSubalgebra) (x : ↥A) : ↑(hA.antipode x) = (HopfAlgebraStruct.antipode R) ↑x

The restricted antipode has the same values as the ambient antipode.

@[instance_reducible]

noncomputable def Subalgebra.IsHopfSubalgebra.hopfAlgebra {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {A : Subalgebra R H} (hA : A.IsHopfSubalgebra) [Module.Flat R H] [Module.Flat R ↥A] : HopfAlgebra R ↥A

The Hopf algebra structure on a flat Hopf subalgebra of a flat Hopf algebra: comultiplication, counit and antipode are restricted from H. This is not an instance because it depends on the proof hA.

Equations

• hA.hopfAlgebra = { toBialgebra := Bialgebra.mk' R ↥A ⋯ ⋯ ⋯ ⋯, antipode := hA.antipode, mul_antipode_rTensor_comul := ⋯, mul_antipode_lTensor_comul := ⋯ }

@[simp]

theorem Subalgebra.IsHopfSubalgebra.comul_apply {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {A : Subalgebra R H} (hA : A.IsHopfSubalgebra) [Module.Flat R H] [Module.Flat R ↥A] (x : ↥A) : CoalgebraStruct.comul x = hA.comulAlgHom x

The comultiplication of the restricted Hopf structure is the restricted algebra map.

@[simp]

theorem Subalgebra.IsHopfSubalgebra.counit_apply {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {A : Subalgebra R H} (hA : A.IsHopfSubalgebra) [Module.Flat R H] [Module.Flat R ↥A] (x : ↥A) : CoalgebraStruct.counit x = CoalgebraStruct.counit ↑x

The counit of the restricted Hopf structure is the counit of the ambient algebra.

@[simp]

theorem Subalgebra.IsHopfSubalgebra.coe_antipode_apply {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {A : Subalgebra R H} (hA : A.IsHopfSubalgebra) [Module.Flat R H] [Module.Flat R ↥A] (x : ↥A) : ↑((HopfAlgebraStruct.antipode R) x) = (HopfAlgebraStruct.antipode R) ↑x

The antipode of the restricted Hopf structure is the antipode of the ambient algebra.

noncomputable def Subalgebra.IsHopfSubalgebra.valBialgHom {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {A : Subalgebra R H} (hA : A.IsHopfSubalgebra) [Module.Flat R H] [Module.Flat R ↥A] : ↥A →ₐc[R] H

The inclusion of a Hopf subalgebra, as a bialgebra homomorphism.

Equations

• hA.valBialgHom = BialgHom.ofAlgHom A.val ⋯ ⋯

@[simp]

theorem Subalgebra.IsHopfSubalgebra.valBialgHom_apply {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {A : Subalgebra R H} (hA : A.IsHopfSubalgebra) [Module.Flat R H] [Module.Flat R ↥A] (x : ↥A) : hA.valBialgHom x = ↑x

The inclusion bialgebra homomorphism is the underlying subalgebra inclusion.

noncomputable def Subalgebra.IsHopfSubalgebra.codRestrict {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {A : Subalgebra R H} (hA : A.IsHopfSubalgebra) [Module.Flat R H] [Module.Flat R ↥A] {K : Type u_1} [Semiring K] [Bialgebra R K] (f : K →ₐc[R] H) (hf : ∀ (x : K), f x ∈ A) : K →ₐc[R] ↥A

Corestrict a bialgebra homomorphism whose image lies in a Hopf subalgebra.

Equations

• hA.codRestrict f hf = BialgHom.ofAlgHom ((↑f).codRestrict A hf) ⋯ ⋯

@[simp]

theorem Subalgebra.IsHopfSubalgebra.coe_codRestrict_apply {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {A : Subalgebra R H} (hA : A.IsHopfSubalgebra) [Module.Flat R H] [Module.Flat R ↥A] {K : Type u_1} [Semiring K] [Bialgebra R K] (f : K →ₐc[R] H) (hf : ∀ (x : K), f x ∈ A) (x : K) : ↑((hA.codRestrict f hf) x) = f x

Corestriction preserves the values of the original bialgebra homomorphism.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.ofHopfSubalgebra {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {A : Subalgebra R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥A] (hA : A.IsHopfSubalgebra) : CommHopfAlgCat R

A flat Hopf subalgebra of a flat commutative Hopf algebra, as a bundled commutative Hopf algebra.

Equations

• TauCeti.CommHopfAlgCat.ofHopfSubalgebra hA = ↧↥A

noncomputable def TauCeti.CommHopfAlgCat.hopfSubalgebraι {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {A : Subalgebra R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥A] (hA : A.IsHopfSubalgebra) : ofHopfSubalgebra hA ⟶ H

The inclusion of a Hopf subalgebra as a morphism of commutative Hopf algebras.

Equations

• TauCeti.CommHopfAlgCat.hopfSubalgebraι hA = CommHopfAlgCat.ofHom hA.valBialgHom

@[simp]

theorem TauCeti.CommHopfAlgCat.hopfSubalgebraι_apply {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {A : Subalgebra R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥A] (hA : A.IsHopfSubalgebra) (x : ↥A) : (CommHopfAlgCat.Hom.hom (hopfSubalgebraι hA)) x = ↑x

The inclusion morphism of a Hopf subalgebra is the inclusion of the underlying subalgebra.

theorem TauCeti.CommHopfAlgCat.hopfSubalgebraι_injective {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {A : Subalgebra R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥A] (hA : A.IsHopfSubalgebra) : Function.Injective ⇑(CommHopfAlgCat.Hom.hom (hopfSubalgebraι hA))

The inclusion morphism of a Hopf subalgebra is injective.

instance TauCeti.CommHopfAlgCat.instMonoCommHopfAlgCatHopfSubalgebraι {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {A : Subalgebra R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥A] (hA : A.IsHopfSubalgebra) : CategoryTheory.Mono (hopfSubalgebraι hA)

noncomputable def TauCeti.CommHopfAlgCat.liftHopfSubalgebra {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {A : Subalgebra R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥A] (hA : A.IsHopfSubalgebra) (f : K ⟶ H) (hf : ∀ (x : ↑K), (CommHopfAlgCat.Hom.hom f) x ∈ A) : K ⟶ ofHopfSubalgebra hA

A morphism of commutative Hopf algebras whose image lies in a Hopf subalgebra, corestricted to that Hopf subalgebra.

Equations

• TauCeti.CommHopfAlgCat.liftHopfSubalgebra hA f hf = CommHopfAlgCat.ofHom (hA.codRestrict (CommHopfAlgCat.Hom.hom f) hf)

@[simp]

theorem TauCeti.CommHopfAlgCat.coe_liftHopfSubalgebra_apply {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {A : Subalgebra R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥A] (hA : A.IsHopfSubalgebra) (f : K ⟶ H) (hf : ∀ (x : ↑K), (CommHopfAlgCat.Hom.hom f) x ∈ A) (x : ↑K) : ↑((CommHopfAlgCat.Hom.hom (liftHopfSubalgebra hA f hf)) x) = (CommHopfAlgCat.Hom.hom f) x

The corestricted morphism has the same values as the original one.

@[simp]

theorem TauCeti.CommHopfAlgCat.liftHopfSubalgebra_comp_hopfSubalgebraι {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {A : Subalgebra R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥A] (hA : A.IsHopfSubalgebra) (f : K ⟶ H) (hf : ∀ (x : ↑K), (CommHopfAlgCat.Hom.hom f) x ∈ A) : CategoryTheory.CategoryStruct.comp (liftHopfSubalgebra hA f hf) (hopfSubalgebraι hA) = f

The corestriction followed by the inclusion is the original morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.liftHopfSubalgebra_comp_hopfSubalgebraι_assoc {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {A : Subalgebra R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥A] (hA : A.IsHopfSubalgebra) (f : K ⟶ H) (hf : ∀ (x : ↑K), (CommHopfAlgCat.Hom.hom f) x ∈ A) {Z : CommHopfAlgCat R} (h : H ⟶ Z) : CategoryTheory.CategoryStruct.comp (liftHopfSubalgebra hA f hf) (CategoryTheory.CategoryStruct.comp (hopfSubalgebraι hA) h) = CategoryTheory.CategoryStruct.comp f h

The corestriction followed by the inclusion is the original morphism.

theorem TauCeti.CommHopfAlgCat.liftHopfSubalgebra_unique {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {A : Subalgebra R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥A] (hA : A.IsHopfSubalgebra) (f : K ⟶ H) (hf : ∀ (x : ↑K), (CommHopfAlgCat.Hom.hom f) x ∈ A) (g : K ⟶ ofHopfSubalgebra hA) (hg : CategoryTheory.CategoryStruct.comp g (hopfSubalgebraι hA) = f) : g = liftHopfSubalgebra hA f hf

A morphism into a Hopf subalgebra is determined by its composite with the inclusion.

theorem TauCeti.CommHopfAlgCat.exists_comp_hopfSubalgebraι_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {A : Subalgebra R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥A] (hA : A.IsHopfSubalgebra) (f : K ⟶ H) : (∃ (g : K ⟶ ofHopfSubalgebra hA), CategoryTheory.CategoryStruct.comp g (hopfSubalgebraι hA) = f) ↔ ∀ (x : ↑K), (CommHopfAlgCat.Hom.hom f) x ∈ A

Universal property of a Hopf subalgebra. A morphism of commutative Hopf algebras into H factors through the inclusion of a Hopf subalgebra A exactly when its image lies in A.