NYLL
Module

OpenNormalNormalizationExtension.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.OpenNormalNormalizationExtension
15 declarations indexed from sourceView source ↗

Module documentation

Canonical normalization extensions on open-normal pullback models

The source of an open-normal pullback model is canonically the complement of the pulled boundary. This file transports a cover across that isomorphism, uses the canonical function-field normalization as its extension, and then transports the resulting pullback isomorphism back to the original model.

Imports4
Imported by1

Declarations

def

coverOnPulledSupportComplement

L44 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.coverOnPulledSupportComplement
Documentation

The cover on the pulled boundary complement obtained by transporting a cover on the selected pullback component across the canonical source isomorphism.

Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · statement
def coverOnPulledSupportComplement
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U)
    (W : FiniteEtale M.sourceScheme) :
    FiniteEtale (I.comap M.targetCover.hom).supportComplement
instance

targetSchemeIsIntegral

L51 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.targetSchemeIsIntegral
Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · statement
instance targetSchemeIsIntegral
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U) :
    IsIntegral M.targetCover.left
instance

targetSchemeIsNormalIntegral

L58 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.targetSchemeIsNormalIntegral
Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · statement
instance targetSchemeIsNormalIntegral
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U) :
    IsNormalIntegral M.targetCover.left
instance

targetSchemeIsLocallyNoetherian

L65 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.targetSchemeIsLocallyNoetherian
Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · statement
instance targetSchemeIsLocallyNoetherian
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U) :
    IsLocallyNoetherian M.targetCover.left
instance

targetSchemeIdIsIntegral

L73 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.targetSchemeIdIsIntegral
Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · statement
instance targetSchemeIdIsIntegral
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U) :
    IsIntegral ((𝟭 Scheme).obj M.targetCover.left)
instance

targetSchemeIdIsNormalIntegral

L79 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.targetSchemeIdIsNormalIntegral
Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · statement
instance targetSchemeIdIsNormalIntegral
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U) :
    IsNormalIntegral ((𝟭 Scheme).obj M.targetCover.left)
instance

targetSchemeIdIsLocallyNoetherian

L85 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.targetSchemeIdIsLocallyNoetherian
Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · statement
instance targetSchemeIdIsLocallyNoetherian
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U) :
    IsLocallyNoetherian ((𝟭 Scheme).obj M.targetCover.left)
instance

pulledSupportComplementConnectedSpace

L91 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.pulledSupportComplementConnectedSpace
Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · statement
instance pulledSupportComplementConnectedSpace
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U) :
    ConnectedSpace (I.comap M.targetCover.hom).supportComplement
instance

pulledSupportComplementIsIntegral

L97 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.pulledSupportComplementIsIntegral
Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · statement
instance pulledSupportComplementIsIntegral
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U) :
    IsIntegral (I.comap M.targetCover.hom).supportComplement
instance

pulledSupportComplementIsNormalIntegral

L104 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.pulledSupportComplementIsNormalIntegral
Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · statement
instance pulledSupportComplementIsNormalIntegral
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U) :
    IsNormalIntegral (I.comap M.targetCover.hom).supportComplement
instance

pulledSupportComplementIsLocallyNoetherian

L111 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.pulledSupportComplementIsLocallyNoetherian
Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · statement
instance pulledSupportComplementIsLocallyNoetherian
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U) :
    IsLocallyNoetherian (I.comap M.targetCover.hom).supportComplement
instance

pulledSupportComplementInclusionQuasiCompact

L118 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.pulledSupportComplementInclusionQuasiCompact
Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · statement
instance pulledSupportComplementInclusionQuasiCompact
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U) :
    QuasiCompact (I.comap M.targetCover.hom).supportComplement.ι
theorem

coverOnPulledSupportComplement_isGalois

L125 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.coverOnPulledSupportComplement_isGalois
Documentation

Transport across the source isomorphism preserves a connected Galois cover.

Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · statement
theorem coverOnPulledSupportComplement_isGalois
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U)
    (W : FiniteEtale M.sourceScheme) (hW : IsGalois W) :
    IsGalois (M.coverOnPulledSupportComplement I xi U W)
theorem

coverOnPulledSupportComplement_aut_isMulCommutative

L147 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.coverOnPulledSupportComplement_aut_isMulCommutative
Documentation

Transport across the source isomorphism also preserves commutativity of the deck group.

Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · full declaration
theorem coverOnPulledSupportComplement_aut_isMulCommutative
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U)
    (W : FiniteEtale M.sourceScheme) (hW : IsGalois W)
    [IsMulCommutative (Aut W)] :
    let W' := M.coverOnPulledSupportComplement I xi U W
    let hW' : IsGalois W' :=
      M.coverOnPulledSupportComplement_isGalois I xi U W hW
    letI : IsGalois W' := hW'
    IsMulCommutative (Aut W') := by
  dsimp only
  let : IsGalois M.sourceCover := M.sourceIsGalois
  let : IsIntegral M.sourceScheme :=
    EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale
      M.sourceCover
  let : IsNormalIntegral M.sourceScheme :=
    EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale
      M.sourceCover
  let : IsLocallyNoetherian M.sourceScheme :=
    EtaleFundamentalGroups.isLocallyNoetherian_left_finiteEtale
      M.sourceCover
  let e := M.sourceIsoPulledSupportComplementOver I xi U
  let : ConnectedSpace (I.comap M.targetCover.hom).supportComplement :=
    e.hom.homeomorph.connectedSpace_iff.mp inferInstance
  exact pullback_obj_aut_isMulCommutative_of_isPreimmersion_of_isDominant
    e.inv W hW
def

extensionOfCanonicalNormalization

L176 ↗
AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.extensionOfCanonicalNormalization
Documentation

Finite etaleness of the canonical normalization of the transported cover produces an actual extension over the target cover and the required pullback isomorphism over the original open-normal model.

Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
namespace OpenNormalPullbackModel
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
  [IsLocallyNoetherian X]
variable (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
  [Nonempty I.supportComplement]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (xi : Spec (.of Omega) ⟶ I.supportComplement)
variable (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
Lean source · full declaration
def extensionOfCanonicalNormalization
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U)
    (W : FiniteEtale M.sourceScheme) (hW : IsGalois W)
    (hEtale :
      let W' := M.coverOnPulledSupportComplement I xi U W
      let hW' : IsGalois W' :=
        M.coverOnPulledSupportComplement_isGalois I xi U W hW
      letI : IsGalois W' := hW'
      let j := (I.comap M.targetCover.hom).supportComplement.ι
      IsFiniteEtale (connectedCoverGenericComposite W' ≫ j).fromNormalization) :
    Σ Z : FiniteEtale M.targetScheme, (pullback M.hom).obj Z ≅ W := by
  letI : IsGalois M.targetCover := M.targetIsGalois
  letI : IsIntegral M.targetCover.left :=
    EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale
      M.targetCover
  letI : IsNormalIntegral M.targetCover.left :=
    EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale
      M.targetCover
  letI : IsLocallyNoetherian M.targetCover.left :=
    EtaleFundamentalGroups.isLocallyNoetherian_left_finiteEtale
      M.targetCover
  let e := M.sourceIsoPulledSupportComplementOver I xi U
  letI : ConnectedSpace (I.comap M.targetCover.hom).supportComplement :=
    e.hom.homeomorph.connectedSpace_iff.mp inferInstance
  letI : IsIntegral (I.comap M.targetCover.hom).supportComplement :=
    isIntegral_of_isOpenImmersion
      (I.comap M.targetCover.hom).supportComplement.ι
  let W' := M.coverOnPulledSupportComplement I xi U W
  let hW' : IsGalois W' :=
    M.coverOnPulledSupportComplement_isGalois I xi U W hW
  letI : IsGalois W' := hW'
  let j := (I.comap M.targetCover.hom).supportComplement.ι
  let extension := connectedCoverExtensionOfNormalization W' j hEtale
  exact extensionOfSourceIso e j M.hom
    (M.sourceIsoPulledSupportComplementOver_hom_comp_ι I xi U)
    W extension

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