Closed immersions of affine group schemes

The scheme morphism underlying the contravariant hopfSpec image of a morphism of commutative Hopf algebras is a closed immersion exactly when the coordinate morphism is surjective. This criterion requires no hypotheses beyond commutativity of the base and coordinate rings.

Mathlib's affine closed-immersion criterion identifies closed immersions between affine spectra with surjective coordinate-ring morphisms. The result here specializes that criterion to the underlying scheme morphism of hopfSpec.

The pinned hopfSpec construction requires the base ring and the Hopf-algebra carriers to lie in the same universe, which is reflected in the declaration in this file.

Main declarations

• TauCeti.CommHopfAlgCat.isClosedImmersion_hopfSpec_map_iff: the coordinate criterion for a morphism of Hopf spectra to be a closed immersion.
• TauCeti.CommHopfAlgCat.isClosedImmersion_hopfSpec_map_comp_eqToHom_iff: the same criterion after identifying the target group scheme.
• TauCeti.CommHopfAlgCat.isClosedImmersion_eqToHom_comp_hopfSpec_map_iff: the criterion after identifying the source group scheme.
• TauCeti.CommHopfAlgCat.isClosedImmersion_eqToHom_comp_hopfSpec_map_comp_eqToHom_iff: the criterion after identifying both group schemes.

@[simp]

theorem TauCeti.CommHopfAlgCat.isClosedImmersion_hopfSpec_map_iff {S : CommRingCat} {A B : CommHopfAlgCat ↑S} (f : A ⟶ B) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left ((AlgebraicGeometry.hopfSpec S).map f.op).hom.hom) ↔ Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)

The scheme morphism underlying the contravariant hopfSpec image of f is a closed immersion if and only if the coordinate Hopf-algebra morphism f is surjective.

@[simp]

theorem TauCeti.CommHopfAlgCat.isClosedImmersion_hopfSpec_map_comp_eqToHom_iff {S : CommRingCat} {A B : CommHopfAlgCat ↑S} {G : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec S))} (hG : G = (AlgebraicGeometry.hopfSpec S).obj (Opposite.op A)) (f : A ⟶ B) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec S).map f.op) (CategoryTheory.eqToHom ⋯)).hom.hom) ↔ Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)

Composing the hopfSpec image of a Hopf-algebra morphism with an identification of its target group scheme does not change the closed-immersion criterion.

@[simp]

theorem TauCeti.CommHopfAlgCat.isClosedImmersion_eqToHom_comp_hopfSpec_map_iff {S : CommRingCat} {A B : CommHopfAlgCat ↑S} {G : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec S))} (hG : G = (AlgebraicGeometry.hopfSpec S).obj (Opposite.op B)) (f : A ⟶ B) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hG) ((AlgebraicGeometry.hopfSpec S).map f.op)).hom.hom) ↔ Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)

Precomposing the hopfSpec image of a Hopf-algebra morphism with an identification of its source group scheme does not change the closed-immersion criterion.

@[simp]

theorem TauCeti.CommHopfAlgCat.isClosedImmersion_eqToHom_comp_hopfSpec_map_comp_eqToHom_iff {S : CommRingCat} {A B : CommHopfAlgCat ↑S} {G H : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec S))} (hG : G = (AlgebraicGeometry.hopfSpec S).obj (Opposite.op B)) (hH : H = (AlgebraicGeometry.hopfSpec S).obj (Opposite.op A)) (f : A ⟶ B) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hG) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec S).map f.op) (CategoryTheory.eqToHom ⋯))).hom.hom) ↔ Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)

Identifying both the source and target of the hopfSpec image of a Hopf-algebra morphism does not change the closed-immersion criterion.