Constant group schemes from finite families of rational sections

Over a field, the constant scheme on a finite group is the finite coproduct of copies of the base point. This file makes that decomposition explicit, proves that an injective finite family of rational sections is a closed immersion, and checks componentwise that a group-valued family extends to a morphism of commutative group schemes.

The final construction is the scheme-theoretic input used by the split \Gamma_0(N) source datum: it replaces an assumed extension interface by a checked morphism and closed-immersion proof.

theorem isClosedImmersion_sigmaDesc {ι : Type u} [Finite ι] {Y : ι → AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (α : (i : ι) → Y i ⟶ X) [∀ (i : ι), AlgebraicGeometry.IsClosedImmersion (α i)] (hα : Pairwise (Function.onFun Disjoint fun (x : ι) => Set.range ⇑(α x))) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.Sigma.desc α)

A finite coproduct of pairwise-disjoint closed immersions is a closed immersion.

theorem specField_identityResidue_isIso {K : Type u} [Field K] : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.descResidueField (AlgebraicGeometry.Scheme.stalkClosedPointTo (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K)))))

The residue-field map induced by the identity point of the spectrum of a field is an isomorphism.

theorem section_eq_of_apply_closedPoint_eq {K : Type u} [Field K] {X : AlgebraicGeometry.Scheme} (π : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) (f g : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X) (hf : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K))) (hg : CategoryTheory.CategoryStruct.comp g π = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K))) (h : f (IsLocalRing.closedPoint K) = g (IsLocalRing.closedPoint K)) : f = g

Two sections over the spectrum of a field agree if they agree on its unique closed point.

theorem pairwise_disjoint_section_ranges {K : Type u} [Field K] {X : AlgebraicGeometry.Scheme} {ι : Type u} (π : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) (s : ι → (AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X)) (hs : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (s i) π = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K))) (hinj : Function.Injective s) : Pairwise (Function.onFun Disjoint fun (i : ι) => Set.range ⇑(s i))

Distinct sections over the spectrum of a field have disjoint ranges.

theorem isClosedImmersion_sigmaDesc_sections {K : Type u} [Field K] {X : AlgebraicGeometry.Scheme} {ι : Type u} [Finite ι] (π : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) (s : ι → (AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X)) (hs : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (s i) π = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K))) (hinj : Function.Injective s) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.Sigma.desc s)

An injective finite family of sections over a field descends from their coproduct as a closed immersion.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.constantGeometricPointMap (K : Type u) [Field K] (G : Type u) [CommGroup G] [Fintype G] (g : G) : Spec (CommRingCat.of K) ⟶ (constantScheme K G).scheme

The underlying map of schemes of a distinguished point of a constant group scheme.

Equations

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

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.constantSchemeSigmaIso (K : Type u) [Field K] (G : Type u) [CommGroup G] [Fintype G] : (constantScheme K G).scheme ≅ ∐ fun (x : G) => Spec (CommRingCat.of K)

The constant scheme on a finite group is the coproduct of one copy of the base field spectrum for each group element.

Equations

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

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantGeometricPoint_left (K : Type u) [Field K] (G : Type u) [CommGroup G] [Fintype G] (g : G) : constantGeometricPointMap K G g = Spec.map (CommRingCat.ofHom (ConstantCoordinates.evaluation g).toRingHom)

The underlying scheme map of a distinguished constant point is evaluation at its index.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantGeometricPoint_sigma (K : Type u) [Field K] (G : Type u) [CommGroup G] [Fintype G] (g : G) : CategoryTheory.CategoryStruct.comp (constantGeometricPointMap K G g) (constantSchemeSigmaIso K G).hom = CategoryTheory.Limits.Sigma.ι (fun (x : G) => Spec (CommRingCat.of K)) g

Under the coproduct decomposition, a distinguished constant point is the corresponding coproduct inclusion.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.constantScheme_hom_ext (K : Type u) [Field K] (G : Type u) [CommGroup G] [Fintype G] {X : Scheme} (f g : (constantScheme K G).scheme ⟶ X) (h : ∀ (a : G), CategoryTheory.CategoryStruct.comp (constantGeometricPointMap K G a) f = CategoryTheory.CategoryStruct.comp (constantGeometricPointMap K G a) g) : f = g

Morphisms out of a finite constant scheme agree if they agree on every distinguished constant point.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.extendConstantHom (K : Type u) [Field K] (E : CommGroupScheme (Spec (CommRingCat.of K))) (G : Type u) [CommGroup G] [Fintype G] (f : G →* (AffineCommGroupScheme.testObject K ⟶ E.X)) : (constantScheme K G).obj ⟶ E

Extend a finite group-valued family of rational sections to a morphism from the corresponding constant commutative group scheme.

Equations

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

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.extendConstantHom_map_point (K : Type u) [Field K] (E : CommGroupScheme (Spec (CommRingCat.of K))) (G : Type u) [CommGroup G] [Fintype G] (f : G →* (AffineCommGroupScheme.testObject K ⟶ E.X)) (g : G) : CategoryTheory.CategoryStruct.comp (constantGeometricPoint K G g) (extendConstantHom K E G f).hom.hom.hom = f g

The constant-group extension agrees with the supplied rational section at each distinguished constant point.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.extendConstantHom_isClosedImmersion (K : Type u) [Field K] (E : CommGroupScheme (Spec (CommRingCat.of K))) (G : Type u) [CommGroup G] [Fintype G] (f : G →* (AffineCommGroupScheme.testObject K ⟶ E.X)) (hinj : Function.Injective ⇑f) : IsClosedImmersion (CategoryTheory.Over.Hom.left (extendConstantHom K E G f).hom.hom.hom)

If the rational sections are injectively indexed, their constant-group extension is a closed immersion.