NYLL
Module

NormalizationComponent.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationComponent
6 declarations indexed from sourceView source ↗

Module documentation

Normalizing a finite-etale component inclusion

A monomorphism between finite-etale covers is a direct summand in the Galois category. Forgetting to schemes preserves that coproduct, and relative normalization preserves the resulting decomposition. Consequently, the actual map obtained by normalizationDesc for a component inclusion is an open immersion with closed image.

If the component has integral source, its relative normalization is integral. A normalization endomorphism fixing a point in this component must map the whole normalized component back into itself: its connected image meets the clopen component. This establishes the geometric component-preservation step without assuming equivariance or a lift of the deck transformation.

Imports6
Imported by4

Declarations

def

normalizationComponentInclusion

L46 ↗
EtaleFundamentalGroups.Inertia.normalizationComponentInclusion
Documentation

The actual map on relative normalizations induced by a morphism of finite-etale covers.

Source context 8 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]
variable {W Z : FiniteEtale U}
variable (f : W.left ⟶ S) [QuasiCompact f] [QuasiSeparated f]
Lean source · statement
def normalizationComponentInclusion (i : Z ⟶ W) :
    (i.left ≫ f).normalization ⟶ f.normalization
theorem

toNormalization_normalizationComponentInclusion

L55 ↗
EtaleFundamentalGroups.Inertia.toNormalization_normalizationComponentInclusion
Source context 9 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]
variable {W Z : FiniteEtale U}
variable (f : W.left ⟶ S) [QuasiCompact f] [QuasiSeparated f]
omit [ConnectedSpace U] in
Lean source · statement
theorem toNormalization_normalizationComponentInclusion (i : Z ⟶ W) :
    (i.left ≫ f).toNormalization ≫ normalizationComponentInclusion f i =
      i.left ≫ f.toNormalization
instance

normalizationComponentInclusion_isOpenImmersion

L63 ↗
EtaleFundamentalGroups.Inertia.normalizationComponentInclusion_isOpenImmersion
Documentation

Normalizing a component inclusion gives an open immersion. The complementary summand is obtained from the Galois-category axiom and the normalization coproduct comparison, rather than supplied as input.

Source context 8 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]
variable {W Z : FiniteEtale U}
variable (f : W.left ⟶ S) [QuasiCompact f] [QuasiSeparated f]
Lean source · statement
instance normalizationComponentInclusion_isOpenImmersion
    (i : Z ⟶ W) [Mono i] :
    IsOpenImmersion (normalizationComponentInclusion f i)
theorem

isClopen_range_normalizationComponentInclusion

L83 ↗
EtaleFundamentalGroups.Inertia.isClopen_range_normalizationComponentInclusion
Documentation

The normalized component is clopen: openness follows from the coproduct comparison, and closedness from the integrality of the normalization map.

Source context 9 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]
variable {W Z : FiniteEtale U}
variable (f : W.left ⟶ S) [QuasiCompact f] [QuasiSeparated f]
omit [ConnectedSpace U] in
Lean source · statement
theorem isClopen_range_normalizationComponentInclusion
    (i : Z ⟶ W) [Mono i] :
    IsClopen (Set.range (normalizationComponentInclusion f i))
theorem

normalizationComponentInclusion_range_comp_subset_of_fixed_point

L93 ↗
EtaleFundamentalGroups.Inertia.normalizationComponentInclusion_range_comp_subset_of_fixed_point
Documentation

If the normalization extension of a cover endomorphism fixes a point of an integral normalized component, it sends that entire normalized component into itself.

Source context 9 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]
variable {W Z : FiniteEtale U}
variable (f : W.left ⟶ S) [QuasiCompact f] [QuasiSeparated f]
omit [ConnectedSpace U] in
Lean source · statement
theorem normalizationComponentInclusion_range_comp_subset_of_fixed_point
    (i : Z ⟶ W) [Mono i] [IsIntegral Z.left]
    (sigma : W.left ⟶ W.left) (hsigma : sigma ≫ f = f)
    (x : (i.left ≫ f).normalization)
    (hfix : normalizationEndomorphism f sigma hsigma
      (normalizationComponentInclusion f i x) =
        normalizationComponentInclusion f i x) :
    Set.range (normalizationComponentInclusion f i ≫
      normalizationEndomorphism f sigma hsigma) ⊆
        Set.range (normalizationComponentInclusion f i)
theorem

normalizationComponentInclusion_range_comp_subset_of_fixes_geometricPoint

L113 ↗
EtaleFundamentalGroups.Inertia.normalizationComponentInclusion_range_comp_subset_of_fixes_geometricPoint
Documentation

Fixing a geometric point in the normalized component supplies the fixed topological point required by component preservation. No choice of a residue-field automorphism or point-action comparison is assumed.

Source context 9 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]
variable {W Z : FiniteEtale U}
variable (f : W.left ⟶ S) [QuasiCompact f] [QuasiSeparated f]
omit [ConnectedSpace U] in
Lean source · statement
theorem normalizationComponentInclusion_range_comp_subset_of_fixes_geometricPoint
    (i : Z ⟶ W) [Mono i] [IsIntegral Z.left]
    {Omega : Type u} [Field Omega]
    (z : Spec (.of Omega) ⟶ (i.left ≫ f).normalization)
    (sigma : W.left ⟶ W.left) (hsigma : sigma ≫ f = f)
    (hfix : z ≫ normalizationComponentInclusion f i ≫
        normalizationEndomorphism f sigma hsigma =
      z ≫ normalizationComponentInclusion f i) :
    Set.range (normalizationComponentInclusion f i ≫
      normalizationEndomorphism f sigma hsigma) ⊆
        Set.range (normalizationComponentInclusion f i)

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