Coordinate Hopf algebras of semidirect products

An internal action between the group objects represented by commutative Hopf algebras equips the product of their underlying affine schemes with a semidirect-product group law. This file carries that group object back across Mathlib's commutative-Hopf-algebra/cogroup equivalence, records the coordinate morphisms representing the two canonical factor inclusions, and computes them on algebra-valued points.

Main declarations

• TauCeti.GrpObj.Action.coordinateHopfAlgebra: the coordinate Hopf algebra of an internal semidirect product.
• TauCeti.GrpObj.Action.coordinateAlgEquiv: its underlying tensor-product coordinate algebra.
• TauCeti.GrpObj.Action.coordinateInl and coordinateInr: the coordinate morphisms representing the two factor inclusions.
• TauCeti.GrpObj.Action.pointMulEquiv_mapDomain_coordinateInl and pointMulEquiv_mapDomain_coordinateInr: their formulas under the semidirect-product point equivalence.

See also

• Mathlib.Algebra.Category.CommHopfAlgCat: the equivalence commHopfAlgCatEquivCogrpCommAlgCat.
• TauCeti.Algebra.AlgebraicGroup.CommHopfAlgCat.Yoneda: the group-object Yoneda equivalence.

@[reducible, inline]

noncomputable abbrev TauCeti.GrpObj.Action.coordinateHopfAlgebra {k : Type u} [CommRing k] {H K : CommHopfAlgCat k} (A : Action (CommHopfAlgCat.grpObj K) (CommHopfAlgCat.grpObj H)) : CommHopfAlgCat k

The coordinate Hopf algebra of an internal semidirect product.

Equations

• A.coordinateHopfAlgebra = (commHopfAlgCatEquivCogrpCommAlgCat k).inverse.obj (Opposite.op A.semidirectProduct)

noncomputable def TauCeti.GrpObj.Action.coordinateAlgEquiv {k : Type u} [CommRing k] {H K : CommHopfAlgCat k} (A : Action (CommHopfAlgCat.grpObj K) (CommHopfAlgCat.grpObj H)) : ↑A.coordinateHopfAlgebra ≃ₐ[k] TensorProduct k ↑H ↑K

The underlying coordinate algebra of a semidirect product is the tensor product of the coordinate algebras of its factors.

Equations

• A.coordinateAlgEquiv = AlgEquiv.refl

instance TauCeti.GrpObj.Action.coordinateHopfAlgebra_finiteType {k : Type u} [CommRing k] {H K : CommHopfAlgCat k} (A : Action (CommHopfAlgCat.grpObj K) (CommHopfAlgCat.grpObj H)) [Algebra.FiniteType k ↑H] [Algebra.FiniteType k ↑K] : Algebra.FiniteType k ↑A.coordinateHopfAlgebra

The coordinate algebra of a semidirect product is finite type when both factors are.

noncomputable def TauCeti.GrpObj.Action.coordinateInl {k : Type u} [CommRing k] {H K : CommHopfAlgCat k} (A : Action (CommHopfAlgCat.grpObj K) (CommHopfAlgCat.grpObj H)) : A.coordinateHopfAlgebra ⟶ H

The coordinate morphism representing inclusion of the normal factor in a semidirect product.

Equations

• A.coordinateInl = (commHopfAlgCatEquivCogrpCommAlgCat k).inverse.map (Opposite.op A.inl)

noncomputable def TauCeti.GrpObj.Action.coordinateInr {k : Type u} [CommRing k] {H K : CommHopfAlgCat k} (A : Action (CommHopfAlgCat.grpObj K) (CommHopfAlgCat.grpObj H)) : A.coordinateHopfAlgebra ⟶ K

The coordinate morphism representing inclusion of the acting factor in a semidirect product.

Equations

• A.coordinateInr = (commHopfAlgCatEquivCogrpCommAlgCat k).inverse.map (Opposite.op A.inr)

@[simp]

theorem TauCeti.GrpObj.Action.grpObjMap_coordinateInl {k : Type u} [CommRing k] {H K : CommHopfAlgCat k} (A : Action (CommHopfAlgCat.grpObj K) (CommHopfAlgCat.grpObj H)) : CommHopfAlgCat.grpObjMap A.coordinateInl = A.inl.hom.hom

The represented group-object morphism associated to coordinateInl is the canonical inclusion of the normal factor.

@[simp]

theorem TauCeti.GrpObj.Action.grpObjMap_coordinateInr {k : Type u} [CommRing k] {H K : CommHopfAlgCat k} (A : Action (CommHopfAlgCat.grpObj K) (CommHopfAlgCat.grpObj H)) : CommHopfAlgCat.grpObjMap A.coordinateInr = A.inr.hom.hom

The represented group-object morphism associated to coordinateInr is the canonical inclusion of the acting factor.

theorem TauCeti.GrpObj.Action.pointMulEquiv_mapDomain_coordinateInl {k : Type u} [CommRing k] {H K : CommHopfAlgCat k} (A : Action (CommHopfAlgCat.grpObj K) (CommHopfAlgCat.grpObj H)) (L : CommAlgCat k) (g : ↑(HopfAlgebra.points L)) : ((CommHopfAlgCat.grpObjPointsMulEquiv A.coordinateHopfAlgebra (Opposite.op L)).symm.trans (A.pointMulEquiv (Opposite.op L))) ((AlgHom.mapDomain (CommHopfAlgCat.Hom.hom A.coordinateInl)) g) = SemidirectProduct.inl ((CommHopfAlgCat.grpObjPointsMulEquiv H (Opposite.op L)).symm g)

Under the point equivalence for a semidirect product, precomposition with coordinateInl is the ordinary inclusion of the normal factor.

theorem TauCeti.GrpObj.Action.pointMulEquiv_mapDomain_coordinateInr {k : Type u} [CommRing k] {H K : CommHopfAlgCat k} (A : Action (CommHopfAlgCat.grpObj K) (CommHopfAlgCat.grpObj H)) (L : CommAlgCat k) (g : ↑(HopfAlgebra.points L)) : ((CommHopfAlgCat.grpObjPointsMulEquiv A.coordinateHopfAlgebra (Opposite.op L)).symm.trans (A.pointMulEquiv (Opposite.op L))) ((AlgHom.mapDomain (CommHopfAlgCat.Hom.hom A.coordinateInr)) g) = SemidirectProduct.inr ((CommHopfAlgCat.grpObjPointsMulEquiv K (Opposite.op L)).symm g)

Under the point equivalence for a semidirect product, precomposition with coordinateInr is the ordinary inclusion of the acting factor.