Closed subgroup schemes

This file defines closed subgroup schemes of a group scheme over an arbitrary base scheme. A closed subgroup scheme is a categorical subobject whose representative arrow is a closed immersion on underlying schemes. Pulling the closed-immersion property back through the two forgetful functors makes the condition independent of the chosen representative.

Neither the base nor the group scheme is required to be affine. Affineness enters only in specialized constructions that import this generic API.

Main declarations

• TauCeti.closedSubgroupMorphismProperty: the closed-immersion property for morphisms of group schemes.
• TauCeti.ClosedSubgroupScheme: closed subgroup subobjects of a group scheme.
• TauCeti.ClosedSubgroupScheme.mk: the closed subgroup represented by a closed immersion.
• TauCeti.ClosedSubgroupScheme.mkIso: the canonical isomorphism of that closed subgroup with the source of the immersion.

def TauCeti.closedSubgroupMorphismProperty (X : AlgebraicGeometry.Scheme) : CategoryTheory.MorphismProperty (CategoryTheory.Grp (CategoryTheory.Over X))

The property of a morphism of group schemes that its underlying scheme morphism is a closed immersion. Pulling the property back along the two forgetful functors makes its invariance under isomorphisms available from the generic morphism-property API.

Equations

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

instance TauCeti.closedSubgroupMorphismProperty_respectsIso (X : AlgebraicGeometry.Scheme) : (closedSubgroupMorphismProperty X).RespectsIso

The underlying closed-immersion property is invariant under isomorphisms of group schemes.

@[instance 900]

instance TauCeti.mono_of_isClosedImmersion_underlying {X : AlgebraicGeometry.Scheme} {G K : CategoryTheory.Grp (CategoryTheory.Over X)} (f : G ⟶ K) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left f.hom.hom)] : CategoryTheory.Mono f

A group-scheme morphism whose underlying scheme morphism is a closed immersion is a monomorphism.

@[simp]

theorem TauCeti.closedSubgroupMorphismProperty_iff (X : AlgebraicGeometry.Scheme) {G K : CategoryTheory.Grp (CategoryTheory.Over X)} (f : G ⟶ K) : closedSubgroupMorphismProperty X f ↔ AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left f.hom.hom)

A morphism has closedSubgroupMorphismProperty exactly when its underlying scheme morphism is a closed immersion.

@[reducible, inline]

abbrev TauCeti.ClosedSubgroupScheme {X : AlgebraicGeometry.Scheme} (G : CategoryTheory.Grp (CategoryTheory.Over X)) : Type (u + 1)

A closed subgroup scheme of G is a categorical subobject represented by a closed immersion on underlying schemes. The use of Subobject identifies presentations isomorphic over G.

Equations

• TauCeti.ClosedSubgroupScheme G = { P : CategoryTheory.Subobject G // TauCeti.closedSubgroupMorphismProperty X P.arrow }

noncomputable def TauCeti.ClosedSubgroupScheme.mk {X : AlgebraicGeometry.Scheme} {G K : CategoryTheory.Grp (CategoryTheory.Over X)} (i : K ⟶ G) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i.hom.hom)] : ClosedSubgroupScheme G

Construct a closed subgroup scheme from a morphism whose underlying scheme morphism is a closed immersion.

Equations

• TauCeti.ClosedSubgroupScheme.mk i = ⟨CategoryTheory.Subobject.mk i, ⋯⟩

@[simp]

theorem TauCeti.ClosedSubgroupScheme.coe_mk {X : AlgebraicGeometry.Scheme} {G K : CategoryTheory.Grp (CategoryTheory.Over X)} (i : K ⟶ G) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i.hom.hom)] : ↑(mk i) = CategoryTheory.Subobject.mk i

The subobject underlying a closed subgroup scheme constructed from an explicit arrow is the subobject represented by that arrow.

noncomputable def TauCeti.ClosedSubgroupScheme.mkIso {X : AlgebraicGeometry.Scheme} {G K : CategoryTheory.Grp (CategoryTheory.Over X)} (i : K ⟶ G) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i.hom.hom)] : CategoryTheory.Subobject.underlying.obj ↑(mk i) ≅ K

The closed subgroup represented by a closed immersion is canonically isomorphic to the source of that immersion.

Equations

• TauCeti.ClosedSubgroupScheme.mkIso i = CategoryTheory.eqToIso ⋯ ≪≫ CategoryTheory.Subobject.underlyingIso i

@[simp]

theorem TauCeti.ClosedSubgroupScheme.mkIso_inv_comp_arrow {X : AlgebraicGeometry.Scheme} {G K : CategoryTheory.Grp (CategoryTheory.Over X)} (i : K ⟶ G) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i.hom.hom)] : CategoryTheory.CategoryStruct.comp (mkIso i).inv (↑(mk i)).arrow = i

The canonical parametrization of a closed subgroup followed by its inclusion is the closed immersion representing it.