NYLL
Module

NormalizationComponentLift.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationComponentLift
5 declarations indexed from sourceView source ↗

Module documentation

Lifting deck transformations from normalized components

The inverse image of a normalized component is the original finite-etale component. This supplies the passage from component preservation on the normalization to component preservation on the cover itself.

Imports8
Imported by2

Declarations

theorem

preimage_normalizationComponentInclusion_range

L38 ↗
EtaleFundamentalGroups.Inertia.preimage_normalizationComponentInclusion_range
Documentation

Normalization preserves the actual decomposition into finite-etale components, including the inverse image of each component.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups.Inertia
universe u
variable {U S : Scheme.{u}}
variable {W Z : FiniteEtale U}
Lean source · statement
theorem preimage_normalizationComponentInclusion_range
    (f : W.left ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    (i : Z ⟶ W) [Mono i] :
    f.toNormalization ⁻¹' Set.range (normalizationComponentInclusion f i) =
      Set.range i.left
theorem

range_comp_subset_of_fixes_normalized_component_geometricPoint

L91 ↗
EtaleFundamentalGroups.Inertia.range_comp_subset_of_fixes_normalized_component_geometricPoint
Documentation

Fixing a geometric point on a normalized component forces preservation of the original finite-etale component, before normalization.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups.Inertia
universe u
variable {U S : Scheme.{u}}
variable {W Z : FiniteEtale U}
Lean source · statement
theorem range_comp_subset_of_fixes_normalized_component_geometricPoint
    (f : W.left ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    (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 (i.left ≫ sigma) ⊆ Set.range i.left
theorem

exists_aut_component_lift_of_preserves_range

L121 ↗
EtaleFundamentalGroups.Inertia.exists_aut_component_lift_of_preserves_range
Documentation

A deck transformation preserving a connected component lifts to an actual deck transformation of that component. The lift is constructed using the open immersion of the component and the connected-object axiom.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups.Inertia
universe u
variable {U S : Scheme.{u}}
variable {W Z : FiniteEtale U}
Lean source · statement
theorem exists_aut_component_lift_of_preserves_range
    (i : Z ⟶ W) [Mono i] [IsConnected Z]
    (sigma : Aut W)
    (hpreserve : Set.range (i.left ≫ sigma.hom.left) ⊆ Set.range i.left) :
    ∃ tau : Aut Z, tau.hom ≫ i = i ≫ sigma.hom
theorem

normalizationComponentInclusion_endomorphism

L160 ↗
EtaleFundamentalGroups.Inertia.normalizationComponentInclusion_endomorphism
Documentation

Normalization of a component inclusion intertwines any commuting endomorphisms of the actual covers.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups.Inertia
universe u
variable {U S : Scheme.{u}}
variable {W Z : FiniteEtale U}
Lean source · full declaration
theorem normalizationComponentInclusion_endomorphism
    (f : W.left ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    (i : Z ⟶ W)
    (sigma : W.left ⟶ W.left) (hsigma : sigma ≫ f = f)
    (tau : Z.left ⟶ Z.left) (htau : tau ≫ i.left = i.left ≫ sigma) :
    normalizationEndomorphism (i.left ≫ f) tau
        (by rw [← Category.assoc, htau, Category.assoc, hsigma]) ≫
      normalizationComponentInclusion f i =
    normalizationComponentInclusion f i ≫ normalizationEndomorphism f sigma hsigma := by
  refine Scheme.Hom.normalization.hom_ext (i.left ≫ f)
    _ _ f.fromNormalization ?_ ?_ ?_
  · simp only [toNormalization_normalizationEndomorphism_assoc,
      toNormalization_normalizationComponentInclusion_assoc,
      toNormalization_normalizationComponentInclusion,
      toNormalization_normalizationEndomorphism]
    rw [← Category.assoc, htau, Category.assoc]
  · simp only [normalizationComponentInclusion, Category.assoc,
      Scheme.Hom.normalizationDesc_comp,
      normalizationEndomorphism_fromNormalization]
  · simp only [normalizationComponentInclusion, Category.assoc,
      normalizationEndomorphism_fromNormalization,
      Scheme.Hom.normalizationDesc_comp]
theorem

exists_aut_component_lift_of_fixes_normalized_geometricPoint

L185 ↗
EtaleFundamentalGroups.Inertia.exists_aut_component_lift_of_fixes_normalized_geometricPoint
Documentation

A deck transformation fixing a geometric point on a normalized component lifts to a component deck transformation fixing that very point.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups.Inertia
universe u
variable {U S : Scheme.{u}}
variable {W Z : FiniteEtale U}
Lean source · full declaration
theorem exists_aut_component_lift_of_fixes_normalized_geometricPoint
    (f : W.left ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    (i : Z ⟶ W) [Mono i] [IsConnected Z] [IsIntegral Z.left]
    {Omega : Type u} [Field Omega]
    (z : Spec (.of Omega) ⟶ (i.left ≫ f).normalization)
    (sigma : Aut W) (hsigma : sigma.hom.left ≫ f = f)
    (hfix : z ≫ normalizationComponentInclusion f i ≫
        normalizationEndomorphism f sigma.hom.left hsigma =
      z ≫ normalizationComponentInclusion f i) :
    ∃ (tau : Aut Z) (htau : tau.hom ≫ i = i ≫ sigma.hom),
      z ≫ normalizationEndomorphism (i.left ≫ f) tau.hom.left (by
        have h := congrArg (fun q : Z ⟶ W => q.left) htau
        change tau.hom.left ≫ i.left = i.left ≫ sigma.hom.left at h
        rw [← Category.assoc, h, Category.assoc, hsigma]) = z := by
  obtain ⟨tau, htau⟩ := exists_aut_component_lift_of_preserves_range i sigma
    (range_comp_subset_of_fixes_normalized_component_geometricPoint
      f i z sigma.hom.left hsigma hfix)
  refine ⟨tau, htau, ?_⟩
  have htauLeft : tau.hom.left ≫ i.left = i.left ≫ sigma.hom.left :=
    congrArg (fun q : Z ⟶ W => q.left) htau
  apply (cancel_mono (normalizationComponentInclusion f i)).mp
  rw [Category.assoc,
    normalizationComponentInclusion_endomorphism f i sigma.hom.left hsigma
      tau.hom.left htauLeft]
  exact hfix

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