NYLL
Module

SchemeArithmeticComplementCover.lean

Nyll.EtaleFundamentalGroups.Kummer.NormalCrossings.SchemeArithmeticComplementCover
12 declarations indexed from sourceView source ↗

Module documentation

Finite-etale covers on local normal-crossings complements

A finite-etale cover of the complement of a divisor support restricts to the principal local chart supplied by a normal-crossings boundary equation. The resulting object has exactly the base scheme used by the local finite-quotient inertia statement.

Imports5
Imported by4

Declarations

theorem

SpecMap_genericPoint_of_injective

L31 ↗
AlgebraicGeometry.SpecMap_genericPoint_of_injective
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem SpecMap_genericPoint_of_injective
    {R S : CommRingCat.{u}} [IsDomain R] [IsDomain S]
    (φ : R ⟶ S) (hφ : Function.Injective φ) :
    Spec.map φ (genericPoint (Spec S)) = genericPoint (Spec R)
theorem

fromSpecStalk_genericPoint_eq

L40 ↗
AlgebraicGeometry.Scheme.fromSpecStalk_genericPoint_eq
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem Scheme.fromSpecStalk_genericPoint_eq
    {X : Scheme.{u}} [IsIntegral X] (x : X) :
    X.fromSpecStalk x (genericPoint (Spec (X.presheaf.stalk x))) =
      genericPoint X
theorem

localizationAwayToAmbient_isDominant

L72 ↗
AlgebraicGeometry.Scheme.IdealSheafData.localizationAwayToAmbient_isDominant
Documentation

The canonical map from an away localization of a prime-localized stalk to an integral ambient scheme is dominant whenever the inverted element is nonzero.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X : Scheme.{u}}
Lean source · statement
theorem localizationAwayToAmbient_isDominant
    [IsIntegral X] (x : X)
    (P : Ideal (X.presheaf.stalk x)) [P.IsPrime]
    (f : Localization.AtPrime P) (hf : f ≠ 0) :
    IsDominant
      (Spec.map (CommRingCat.ofHom
          (algebraMap (Localization.AtPrime P) (Localization.Away f))) ≫
        Scheme.localizationAtPrimeTo X x P)
theorem

localizationAwayToSupportComplement_isPreimmersion

L125 ↗
AlgebraicGeometry.Scheme.IdealSheafData.localizationAwayToSupportComplement_isPreimmersion
Documentation

The local principal-complement map is a preimmersion.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X : Scheme.{u}}
Lean source · statement
theorem localizationAwayToSupportComplement_isPreimmersion
    (I : X.IdealSheafData) (x : X)
    (P : Ideal (X.presheaf.stalk x)) [P.IsPrime]
    (f : Localization.AtPrime P)
    (hboundary :
      (I.stalkIdeal x).map
          (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)) =
        Ideal.span {f}) :
    IsPreimmersion
      (localizationAwayToSupportComplement I x P f hboundary)
theorem

localizationAwayToSupportComplement_isDominant

L156 ↗
AlgebraicGeometry.Scheme.IdealSheafData.localizationAwayToSupportComplement_isDominant
Documentation

The local principal-complement map is dominant over an integral ambient scheme when its boundary equation is nonzero.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X : Scheme.{u}}
Lean source · statement
theorem localizationAwayToSupportComplement_isDominant
    [IsIntegral X]
    (I : X.IdealSheafData) (x : X)
    (P : Ideal (X.presheaf.stalk x)) [P.IsPrime]
    (f : Localization.AtPrime P) (hf : f ≠ 0)
    (hboundary :
      (I.stalkIdeal x).map
          (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)) =
        Ideal.span {f}) :
    IsDominant
      (localizationAwayToSupportComplement I x P f hboundary)
theorem

supportComplement_nonempty_of_localizationAway

L175 ↗
AlgebraicGeometry.Scheme.IdealSheafData.supportComplement_nonempty_of_localizationAway
Documentation

A nonzero local boundary equation makes the global support complement nonempty.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X : Scheme.{u}}
Lean source · statement
theorem supportComplement_nonempty_of_localizationAway
    [IsIntegral X]
    (I : X.IdealSheafData) (x : X)
    (P : Ideal (X.presheaf.stalk x)) [P.IsPrime]
    (f : Localization.AtPrime P) (hf : f ≠ 0)
    (hboundary :
      (I.stalkIdeal x).map
          (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)) =
        Ideal.span {f}) :
    Nonempty I.supportComplement
theorem

localizationAwayToSupportComplement_quasiCompact

L194 ↗
AlgebraicGeometry.Scheme.IdealSheafData.localizationAwayToSupportComplement_quasiCompact
Documentation

The local principal-complement map is quasi-compact over a locally Noetherian ambient scheme.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X : Scheme.{u}}
Lean source · statement
theorem localizationAwayToSupportComplement_quasiCompact
    [IsLocallyNoetherian X]
    (I : X.IdealSheafData) (x : X)
    (P : Ideal (X.presheaf.stalk x)) [P.IsPrime]
    (f : Localization.AtPrime P)
    (hboundary :
      (I.stalkIdeal x).map
          (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)) =
        Ideal.span {f}) :
    QuasiCompact
      (localizationAwayToSupportComplement I x P f hboundary)
def

pullbackSupportComplementCoverToBoundaryAway

L209 ↗
AlgebraicGeometry.Scheme.IdealSheafData.pullbackSupportComplementCoverToBoundaryAway
Documentation

Pull a finite-etale cover of a support complement to the local chart obtained by inverting the normal-crossings boundary product.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X : Scheme.{u}}
Lean source · statement
def pullbackSupportComplementCoverToBoundaryAway
    (I : X.IdealSheafData) (x : X)
    (P : PrimeSpectrum (X.presheaf.stalk x)) {r : ℕ}
    (t : Fin 2 → Localization.AtPrime P.asIdeal)
    (hboundary :
      (I.stalkIdeal x).map
          (algebraMap (X.presheaf.stalk x)
            (Localization.AtPrime P.asIdeal)) =
        Ideal.span {boundaryProduct t r})
    (W : FiniteEtale I.supportComplement) :
    FiniteEtale
      (Spec (.of (Localization.Away (boundaryProduct t r))))
theorem

boundaryProduct_ne_zero_of_splitStrictNormalCrossings

L225 ↗
AlgebraicGeometry.Scheme.IdealSheafData.boundaryProduct_ne_zero_of_splitStrictNormalCrossings
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X : Scheme.{u}}
Lean source · statement
theorem boundaryProduct_ne_zero_of_splitStrictNormalCrossings
    {V : Type u} [CommRing V] [IsDomain V] [IsLocalRing V]
    {r : ℕ} {t : Fin 2 → V}
    (hNC : IsSplitStrictNormalCrossingsAt
      (boundaryProduct t r) t r) :
    boundaryProduct t r ≠ 0
theorem

localizationAwayToSupportComplement_pullback_isGalois

L238 ↗
AlgebraicGeometry.Scheme.IdealSheafData.localizationAwayToSupportComplement_pullback_isGalois
Documentation

Pullback along the canonical localization-away map preserves connected Galois covers when the inverted boundary equation is nonzero.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X : Scheme.{u}}
Lean source · statement
theorem localizationAwayToSupportComplement_pullback_isGalois
    [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
    (I : X.IdealSheafData) (x : X)
    (P : Ideal (X.presheaf.stalk x)) [P.IsPrime]
    (f : Localization.AtPrime P) (hf : f ≠ 0)
    (hboundary :
      (I.stalkIdeal x).map
          (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)) =
        Ideal.span {f})
    [Nonempty I.supportComplement]
    [IsDomain (Localization.Away f)]
    (W : FiniteEtale I.supportComplement) (hW : IsGalois W) :
    IsGalois ((FiniteEtale.pullback
      (localizationAwayToSupportComplement I x P f hboundary)).obj W)
theorem

localizationAwayToSupportComplement_pullback_isGalois_of_ne_zero

L273 ↗
AlgebraicGeometry.Scheme.IdealSheafData.localizationAwayToSupportComplement_pullback_isGalois_of_ne_zero
Documentation

The nonzero local equation itself supplies the connected source and nonempty target required by Galois pullback.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X : Scheme.{u}}
Lean source · full declaration
theorem localizationAwayToSupportComplement_pullback_isGalois_of_ne_zero
    [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
    (I : X.IdealSheafData) (x : X)
    (P : Ideal (X.presheaf.stalk x)) [P.IsPrime]
    (f : Localization.AtPrime P) (hf : f ≠ 0)
    (hboundary :
      (I.stalkIdeal x).map
          (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)) =
        Ideal.span {f}) :
    letI : IsDomain (Localization.Away f) :=
      IsLocalization.Away.isDomain (Localization.Away f) hf
    letI : Nonempty I.supportComplement :=
      supportComplement_nonempty_of_localizationAway
        I x P f hf hboundary
    ∀ (W : FiniteEtale I.supportComplement), IsGalois W →
      IsGalois ((FiniteEtale.pullback
        (localizationAwayToSupportComplement I x P f hboundary)).obj W) := by
  let : IsDomain (Localization.Away f) :=
    IsLocalization.Away.isDomain (Localization.Away f) hf
  let : Nonempty I.supportComplement :=
    supportComplement_nonempty_of_localizationAway
      I x P f hf hboundary
  intro W hW
  exact localizationAwayToSupportComplement_pullback_isGalois
    I x P f hf hboundary W hW
theorem

pullbackSupportComplementCoverToBoundaryAway_isGalois

L301 ↗
AlgebraicGeometry.Scheme.IdealSheafData.pullbackSupportComplementCoverToBoundaryAway_isGalois
Documentation

Pullback from a global support complement to a local split normal-crossings chart preserves connected Galois covers.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X : Scheme.{u}}
Lean source · full declaration
theorem pullbackSupportComplementCoverToBoundaryAway_isGalois
    [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
    (I : X.IdealSheafData) (x : X)
    (P : PrimeSpectrum (X.presheaf.stalk x)) {r : ℕ}
    (t : Fin 2 → Localization.AtPrime P.asIdeal)
    (hboundary :
      (I.stalkIdeal x).map
          (algebraMap (X.presheaf.stalk x)
            (Localization.AtPrime P.asIdeal)) =
        Ideal.span {boundaryProduct t r})
    (hNC : IsSplitStrictNormalCrossingsAt
      (boundaryProduct t r) t r) :
    let hf := boundaryProduct_ne_zero_of_splitStrictNormalCrossings hNC
    letI : IsDomain (Localization.Away (boundaryProduct t r)) :=
      IsLocalization.Away.isDomain
        (Localization.Away (boundaryProduct t r)) hf
    letI : Nonempty I.supportComplement :=
      supportComplement_nonempty_of_localizationAway
        I x P.asIdeal (boundaryProduct t r) hf hboundary
    ∀ (W : FiniteEtale I.supportComplement), IsGalois W →
      IsGalois
        (pullbackSupportComplementCoverToBoundaryAway
          I x P t hboundary W) := by
  dsimp only
  let hf := boundaryProduct_ne_zero_of_splitStrictNormalCrossings hNC
  let : IsDomain (Localization.Away (boundaryProduct t r)) :=
    IsLocalization.Away.isDomain
      (Localization.Away (boundaryProduct t r)) hf
  let : Nonempty I.supportComplement :=
    supportComplement_nonempty_of_localizationAway
      I x P.asIdeal (boundaryProduct t r) hf hboundary
  intro W hW
  exact localizationAwayToSupportComplement_pullback_isGalois
    I x P.asIdeal (boundaryProduct t r) hf hboundary W hW

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