NYLL
Module

NormalizationComponentPoint.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationComponentPoint
2 declarations indexed from sourceView source ↗

Module documentation

A normalized geometric point lies in an actual cover component

The finite connected decomposition of the original cover has clopen images in its normalization. Their union contains the dense image of the cover and is closed, so it covers the normalization. The open-immersion lifting property then factors an actual geometric-point morphism through one of these normalized components.

Imports8
Imported by3

Declarations

theorem

exists_normalizationComponent_geometricPoint

L39 ↗
EtaleFundamentalGroups.Inertia.exists_normalizationComponent_geometricPoint
Documentation

Every geometric point of the relative normalization lies in the normalization of a connected finite-etale component of the original cover.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u
variable {U S : Scheme.{u}} [ConnectedSpace U]
Lean source · statement
theorem exists_normalizationComponent_geometricPoint
    (W : FiniteEtale U)
    (f : W.left ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    {Omega : Type u} [Field Omega]
    (z : Spec (.of Omega) ⟶ f.normalization) :
    ∃ (Z : FiniteEtale U) (i : Z ⟶ W)
      (q : Spec (.of Omega) ⟶ (i.left ≫ f).normalization),
      Mono i ∧ IsConnected Z ∧ q ≫ normalizationComponentInclusion f i = z
theorem

exists_galoisNormalizationComponent_geometricPoint

L88 ↗
EtaleFundamentalGroups.Inertia.exists_galoisNormalizationComponent_geometricPoint
Documentation

For a pulled-back Galois cover, the component selected by an arbitrary normalization point is itself Galois and can be pointed over any fixed geometric base point.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u
variable {U S : Scheme.{u}} [ConnectedSpace U]
Lean source · statement
theorem exists_galoisNormalizationComponent_geometricPoint
    {Y : Scheme.{u}} [ConnectedSpace Y]
    (b : U ⟶ Y) {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ U)
    (W : FiniteEtale Y) (hW : IsGalois W)
    (f : ((FiniteEtale.pullback b).obj W).left ⟶ S)
    [QuasiCompact f] [QuasiSeparated f]
    {Omega' : Type u} [Field Omega']
    (q : Spec (.of Omega') ⟶ f.normalization) :
    ∃ (Z : FiniteEtale U) (i : Z ⟶ (FiniteEtale.pullback b).obj W)
      (qZ : Spec (.of Omega') ⟶ (i.left ≫ f).normalization)
      (z : (FiniteEtale.fiber xi).obj Z)
      (w : (FiniteEtale.fiber (xi ≫ b)).obj W),
      Mono i ∧ IsGalois Z ∧
        qZ ≫ normalizationComponentInclusion f i = q ∧
        (FiniteEtale.fiber xi).map i z =
          transportedPointOfCompIso (FiniteEtale.pullback b)
            (FiniteEtale.pullbackFiberIso b xi) W w

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.