Centers and isomorphisms of affine groups

An isomorphism of commutative Hopf algebras carries the ideal defining the center to the ideal defining the center. Equivalently, the induced isomorphism of affine group schemes restricts to an isomorphism of their centers.

The proof uses the universal property of centerDefiningIdeal: the pullback of a central Hopf ideal along a bialgebra equivalence is central, so minimality gives both inclusions. The resulting coordinate isomorphism transports the general quotient-by-pullback isomorphism along this ideal equality and is then carried through hopfSpec.

Main declarations

• TauCeti.CommHopfAlgCat.comapOfSurjective_centerDefiningIdeal: center ideals are preserved by isomorphisms.
• TauCeti.CommHopfAlgCat.centerCoordinateMap: restriction of an isomorphism to the coordinate Hopf algebras of the centers.
• TauCeti.CommHopfAlgCat.centerCoordinateIso: the resulting coordinate isomorphism.
• TauCeti.CommHopfAlgCat.centerGroupSchemeIso: the corresponding isomorphism of center group schemes.

References

• J. S. Milne, Algebraic Groups (2017), §1.k and §2.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 2.

@[simp]

theorem TauCeti.CommHopfAlgCat.comapOfSurjective_centerDefiningIdeal {k : Type u} [Field k] {H K : CommHopfAlgCat k} (e : H ≅ K) : (centerDefiningIdeal K).comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯ = centerDefiningIdeal H

An isomorphism of commutative Hopf algebras preserves the ideal defining the center.

noncomputable def TauCeti.CommHopfAlgCat.centerCoordinateIso {k : Type u} [Field k] {H K : CommHopfAlgCat k} (e : H ≅ K) : quotient H (centerDefiningIdeal H) ≅ quotient K (centerDefiningIdeal K)

The isomorphism on coordinate Hopf algebras obtained by restricting an ambient isomorphism to the centers.

Equations

• TauCeti.CommHopfAlgCat.centerCoordinateIso e = TauCeti.CommHopfAlgCat.quotientIsoOfComapEq e (TauCeti.CommHopfAlgCat.centerDefiningIdeal K) ⋯

noncomputable def TauCeti.CommHopfAlgCat.centerCoordinateMap {k : Type u} [Field k] {H K : CommHopfAlgCat k} (e : H ≅ K) : quotient H (centerDefiningIdeal H) ⟶ quotient K (centerDefiningIdeal K)

The coordinate morphism obtained by restricting an ambient isomorphism to the centers.

Equations

• TauCeti.CommHopfAlgCat.centerCoordinateMap e = (TauCeti.CommHopfAlgCat.centerCoordinateIso e).hom

@[simp]

theorem TauCeti.CommHopfAlgCat.centerCoordinateIso_hom {k : Type u} [Field k] {H K : CommHopfAlgCat k} (e : H ≅ K) : (centerCoordinateIso e).hom = centerCoordinateMap e

The forward morphism of the coordinate isomorphism is the restricted coordinate map.

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_centerCoordinateMap {k : Type u} [Field k] {H K : CommHopfAlgCat k} (e : H ≅ K) : CategoryTheory.CategoryStruct.comp (mkQuotient H (centerDefiningIdeal H)) (centerCoordinateMap e) = CategoryTheory.CategoryStruct.comp e.hom (mkQuotient K (centerDefiningIdeal K))

Restriction to centers commutes with the two ambient quotient morphisms.

@[simp]

theorem TauCeti.CommHopfAlgCat.centerCoordinateMap_mk {k : Type u} [Field k] {H K : CommHopfAlgCat k} (e : H ≅ K) (x : ↑H) : (CommHopfAlgCat.Hom.hom (centerCoordinateMap e)) ((Ideal.Quotient.mk (centerDefiningIdeal H).toIdeal) x) = (Ideal.Quotient.mkₐ k (centerDefiningIdeal K).toIdeal) ((CommHopfAlgCat.Hom.hom e.hom) x)

On quotient classes, restriction to the center applies the ambient isomorphism before taking the target quotient class.

@[simp]

theorem TauCeti.CommHopfAlgCat.centerCoordinateMap_refl {k : Type u} [Field k] (H : CommHopfAlgCat k) : centerCoordinateMap (CategoryTheory.Iso.refl H) = CategoryTheory.CategoryStruct.id (quotient H (centerDefiningIdeal H))

The map on center coordinates induced by an identity is the identity.

@[simp]

theorem TauCeti.CommHopfAlgCat.centerCoordinateMap_trans {k : Type u} [Field k] {H K L : CommHopfAlgCat k} (e : H ≅ K) (f : K ≅ L) : centerCoordinateMap (e ≪≫ f) = CategoryTheory.CategoryStruct.comp (centerCoordinateMap e) (centerCoordinateMap f)

Restriction to center coordinates is compatible with composition of isomorphisms.

@[simp]

theorem TauCeti.CommHopfAlgCat.centerCoordinateIso_inv {k : Type u} [Field k] {H K : CommHopfAlgCat k} (e : H ≅ K) : (centerCoordinateIso e).inv = centerCoordinateMap e.symm

The inverse morphism of the coordinate isomorphism is restriction along the inverse ambient isomorphism.

noncomputable def TauCeti.CommHopfAlgCat.centerGroupSchemeIso {k : Type u} [Field k] {H K : CommHopfAlgCat k} (e : H ≅ K) : centerGroupScheme H ≅ centerGroupScheme K

An isomorphism of affine group schemes represented by commutative Hopf algebras restricts to an isomorphism of their center group schemes.

Equations

• TauCeti.CommHopfAlgCat.centerGroupSchemeIso e = ((AlgebraicGeometry.hopfSpec ↧k).mapIso (TauCeti.CommHopfAlgCat.centerCoordinateIso e).op).symm

@[simp]

theorem TauCeti.CommHopfAlgCat.centerGroupSchemeIso_hom {k : Type u} [Field k] {H K : CommHopfAlgCat k} (e : H ≅ K) : (centerGroupSchemeIso e).hom = (AlgebraicGeometry.hopfSpec ↧k).map (centerCoordinateMap e.symm).op

The forward center-scheme isomorphism is induced contravariantly by restriction along the inverse ambient isomorphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.centerGroupSchemeIso_inv {k : Type u} [Field k] {H K : CommHopfAlgCat k} (e : H ≅ K) : (centerGroupSchemeIso e).inv = (AlgebraicGeometry.hopfSpec ↧k).map (centerCoordinateMap e).op

The inverse center-scheme isomorphism is induced contravariantly by restriction along the forward ambient isomorphism.

@[instance_reducible]

noncomputable def TauCeti.CommHopfAlgCat.centerAlgSpecMonoidal {k : Type u} [Field k] : (AlgebraicGeometry.algSpec ↧k).Monoidal

The monoidal structure underlying the canonical braided structure on relative spectrum.

Equations

• TauCeti.CommHopfAlgCat.centerAlgSpecMonoidal = AlgebraicGeometry.braidedAlgSpec.toMonoidal

@[simp]

theorem TauCeti.CommHopfAlgCat.centerGroupSchemeIso_hom_comp_centerGroupSchemeι {k : Type u} [Field k] {H K : CommHopfAlgCat k} (e : H ≅ K) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.algSpec ↧k).mapGrp.map ((commHopfAlgCatEquivCogrpCommAlgCat k).functor.map (centerCoordinateMap e.symm)).unop) (centerGroupSchemeι K) = CategoryTheory.CategoryStruct.comp (centerGroupSchemeι H) ((AlgebraicGeometry.hopfSpec ↧k).map e.inv.op)

The isomorphism of centers commutes with their inclusions into the ambient affine group schemes.

@[simp]

theorem TauCeti.CommHopfAlgCat.centerGroupSchemeIso_refl {k : Type u} [Field k] (H : CommHopfAlgCat k) : centerGroupSchemeIso (CategoryTheory.Iso.refl H) = CategoryTheory.Iso.refl (centerGroupScheme H)

The center-scheme isomorphism induced by the identity is the identity.

@[simp]

theorem TauCeti.CommHopfAlgCat.centerGroupSchemeIso_trans {k : Type u} [Field k] {H K L : CommHopfAlgCat k} (e : H ≅ K) (f : K ≅ L) : centerGroupSchemeIso (e ≪≫ f) = centerGroupSchemeIso e ≪≫ centerGroupSchemeIso f

Center-scheme isomorphisms induced by ambient isomorphisms respect composition.