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.
• TauCeti.ClosedSubgroupScheme.mapIso: transport of closed subgroups along an isomorphism of ambient group schemes, compatible with composition of isomorphisms (TauCeti.ClosedSubgroupScheme.mapIso_trans).

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.

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

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

@[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.

instance TauCeti.ClosedSubgroupScheme.isClosedImmersion_arrow {X : AlgebraicGeometry.Scheme} {G : CategoryTheory.Grp (CategoryTheory.Over X)} (P : ClosedSubgroupScheme G) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (↑P).arrow.hom.hom)

The representative arrow of a closed subgroup scheme is a closed immersion on underlying schemes.

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.

@[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.

@[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.

noncomputable def TauCeti.ClosedSubgroupScheme.mapIso {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (e : G ≅ H) : ClosedSubgroupScheme G ≃o ClosedSubgroupScheme H

Closed subgroups are transported along an isomorphism of ambient group schemes by postcomposing their representing arrows with the isomorphism.

@[simp]

theorem TauCeti.ClosedSubgroupScheme.coe_mapIso {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (e : G ≅ H) (P : ClosedSubgroupScheme G) : ↑((mapIso e) P) = (CategoryTheory.Subobject.map e.hom).obj ↑P

The subobject underlying a transported closed subgroup is the transported subobject.

@[simp]

theorem TauCeti.ClosedSubgroupScheme.mapIso_trans {X : AlgebraicGeometry.Scheme} {G H K : CategoryTheory.Grp (CategoryTheory.Over X)} (e : G ≅ H) (e' : H ≅ K) (P : ClosedSubgroupScheme G) : (mapIso (e ≪≫ e')) P = (mapIso e') ((mapIso e) P)

Transporting closed subgroups along a composite of isomorphisms transports along each in turn.

theorem TauCeti.ClosedSubgroupScheme.existsUnique_comp_arrow_mapIso_iff {X : AlgebraicGeometry.Scheme} {G H Y : CategoryTheory.Grp (CategoryTheory.Over X)} (e : G ≅ H) (P : ClosedSubgroupScheme G) (g : Y ⟶ H) : (∃! f : Y ⟶ CategoryTheory.Subobject.underlying.obj ↑((mapIso e) P), CategoryTheory.CategoryStruct.comp f (↑((mapIso e) P)).arrow = g) ↔ ∃! f : Y ⟶ CategoryTheory.Subobject.underlying.obj ↑P, CategoryTheory.CategoryStruct.comp f (↑P).arrow = CategoryTheory.CategoryStruct.comp g e.inv

A map g factors uniquely through a closed subgroup transported along an isomorphism e exactly when g ≫ e.inv factors uniquely through the original closed subgroup.

instance TauCeti.ClosedSubgroupScheme.isClosedImmersion_comp_iso_hom {X : AlgebraicGeometry.Scheme} {G H K : CategoryTheory.Grp (CategoryTheory.Over X)} (i : K ⟶ G) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i.hom.hom)] (e : G ≅ H) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp i e.hom).hom.hom)

Postcomposing a closed immersion with an isomorphism of group schemes gives a closed immersion.

@[simp]

theorem TauCeti.ClosedSubgroupScheme.mapIso_mk {X : AlgebraicGeometry.Scheme} {G H K : CategoryTheory.Grp (CategoryTheory.Over X)} (e : G ≅ H) (i : K ⟶ G) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i.hom.hom)] : (mapIso e) (mk i) = mk (CategoryTheory.CategoryStruct.comp i e.hom)

Transporting the closed subgroup represented by a closed immersion along an isomorphism gives the closed subgroup represented by the composite.

@[simp]

theorem TauCeti.ClosedSubgroupScheme.coe_mapIso_symm {X : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (e : G ≅ H) (P : ClosedSubgroupScheme H) : ↑((mapIso e).symm P) = (CategoryTheory.Subobject.map e.inv).obj ↑P

The subobject underlying a closed subgroup transported back along an isomorphism is the subobject transported back along it.

instance TauCeti.ClosedSubgroupScheme.isClosedImmersion_comp_iso_inv {X : AlgebraicGeometry.Scheme} {G H K : CategoryTheory.Grp (CategoryTheory.Over X)} (i : K ⟶ H) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i.hom.hom)] (e : G ≅ H) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp i e.inv).hom.hom)

Postcomposing a closed immersion with the inverse of an isomorphism of group schemes gives a closed immersion.

@[simp]

theorem TauCeti.ClosedSubgroupScheme.mapIso_symm_mk {X : AlgebraicGeometry.Scheme} {G H K : CategoryTheory.Grp (CategoryTheory.Over X)} (e : G ≅ H) (i : K ⟶ H) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i.hom.hom)] : (mapIso e).symm (mk i) = mk (CategoryTheory.CategoryStruct.comp i e.inv)

Transporting the closed subgroup represented by a closed immersion back along an isomorphism gives the closed subgroup represented by the composite with the inverse.