Module

PuncturedSpectrumConnectedRestriction.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumConnectedRestriction

21 declarations indexed from sourceView source ↗

Module documentation

Restricting connected function-field normalizations

This file compares the normalization in the function field of a connected finite-etale cover with the cover itself. The comparison is constructed from the universal property of relative normalization and checked on affine charts by the uniqueness of integral closure inside the common function field.

Imports2

Imported by7

instance

connectedLeftIntegral

L31 ↗

AlgebraicGeometry.FiniteEtale.connectedLeftIntegral

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]

Lean source · statement

instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left

instance

fieldSpecQuasiCompact

L35 ↗

AlgebraicGeometry.FiniteEtale.fieldSpecQuasiCompact

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W

Lean source · full declaration

instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

instance

connectedLeftNormal

L40 ↗

AlgebraicGeometry.FiniteEtale.connectedLeftNormal

Source context 8 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

Lean source · statement

instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left

def

connectedCoverGenericMorphism

L46 ↗

AlgebraicGeometry.FiniteEtale.connectedCoverGenericMorphism

Documentation

The generic-point morphism of the source of a connected finite-etale cover.

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

def connectedCoverGenericMorphism
    (W : FiniteEtale X) [IsConnected W] :
    Spec (.of W.left.functionField) ⟶ W.left

def

connectedCoverGenericComposite

L53 ↗

AlgebraicGeometry.FiniteEtale.connectedCoverGenericComposite

Documentation

The generic-point morphism of a connected finite-etale cover, composed with the cover map to the base.

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

def connectedCoverGenericComposite
    (W : FiniteEtale X) [IsConnected W] :
    Spec (.of W.left.functionField) ⟶ X

def

connectedCoverGenericCompositeSectionsIso

L60 ↗

AlgebraicGeometry.FiniteEtale.connectedCoverGenericCompositeSectionsIso

Documentation

Sections on the inverse image of the top open under the generic composite identify with the function field of the connected cover.

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

def connectedCoverGenericCompositeSectionsIso
    (W : FiniteEtale X) [IsConnected W] :
    Γ(Spec (.of W.left.functionField),
        connectedCoverGenericComposite W ⁻¹ᵁ (⊤ : X.Opens)) ≅
      .of W.left.functionField

theorem

connectedCoverGenericCompositeSectionsIso_hom_appTop

L76 ↗

AlgebraicGeometry.FiniteEtale.connectedCoverGenericCompositeSectionsIso_hom_appTop

Documentation

Under the canonical sections identification, the generic composite on global sections is the canonical map through the two function fields.

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · full declaration

theorem connectedCoverGenericCompositeSectionsIso_hom_appTop
    (W : FiniteEtale X) [IsConnected W] (r : Γ(X, ⊤)) :
    letI : Nonempty (⊤ : X.Opens) :=
      ⟨⟨Classical.choice (inferInstance : Nonempty X), by simp⟩⟩
    letI : Algebra X.functionField W.left.functionField :=
      EtaleFundamentalGroups.finiteEtaleFunctionFieldAlgebra W
    (connectedCoverGenericCompositeSectionsIso W).hom
          ((connectedCoverGenericComposite W).appTop r) =
        algebraMap X.functionField W.left.functionField
          (X.germToFunctionField ⊤ r) := by
  dsimp only
  let : Algebra X.functionField W.left.functionField :=
    EtaleFundamentalGroups.finiteEtaleFunctionFieldAlgebra W
  let : IsIntegral W.left :=
    EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
  let : Nonempty (⊤ : X.Opens) :=
    ⟨⟨Classical.choice (inferInstance : Nonempty X), by simp⟩⟩
  let : Nonempty (⊤ : W.left.Opens) :=
    let y : W.left := Classical.choice (inferInstance : Nonempty W.left)
    ⟨⟨y, by trivial⟩⟩
  let hDense : DenseRange W.hom :=
    EtaleFundamentalGroups.finiteEtale_hom_denseRange_of_isConnected W
  have hGeneric :
      (connectedCoverGenericCompositeSectionsIso W).hom
          ((connectedCoverGenericComposite W).appTop r) =
        W.left.germToFunctionField ⊤ (W.hom.appTop r) := by
    change (W.left.genericExtensionSectionsIso W.left.functionField
        (⊤ : W.left.Opens)).hom
          ((W.left.genericExtensionMorphism W.left.functionField).app
            (⊤ : W.left.Opens) (W.hom.appTop r)) = _
    rw [W.left.genericExtensionSectionsIso_hom_app]
    simp
  rw [hGeneric]
  have hFieldMap :
      (@Scheme.Hom.functionFieldMap X W.left W.hom inferInstance
        (EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W)
          hDense).comp (X.germToFunctionField ⊤).hom =
        (W.left.germToFunctionField ⊤).hom.comp W.hom.appTop.hom :=
    @Scheme.Hom.functionFieldMap_comp_germToFunctionField_top
      X W.left W.hom inferInstance
        (EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W)
          hDense
  have hMap := DFunLike.congr_fun hFieldMap r
  change (@Scheme.Hom.functionFieldMap X W.left W.hom inferInstance
      (EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W)
        hDense) (X.germToFunctionField ⊤ r) =
    W.left.germToFunctionField ⊤ (W.hom.appTop r) at hMap
  change W.left.germToFunctionField ⊤ (W.hom.appTop r) =
    (@Scheme.Hom.functionFieldMap X W.left W.hom inferInstance
      (EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W)
        (EtaleFundamentalGroups.finiteEtale_hom_denseRange_of_isConnected W))
          (X.germToFunctionField ⊤ r)
  simpa only [hDense] using hMap.symm

def

connectedCoverGenericNormalizationDesc

L130 ↗

AlgebraicGeometry.FiniteEtale.connectedCoverGenericNormalizationDesc

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

def connectedCoverGenericNormalizationDesc
    (W : FiniteEtale X) [IsConnected W] :
    (connectedCoverGenericComposite W).normalization ⟶ W.left

lemma

connectedCoverGenericNormalizationDesc_comp

L140 ↗

AlgebraicGeometry.FiniteEtale.connectedCoverGenericNormalizationDesc_comp

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

lemma connectedCoverGenericNormalizationDesc_comp
    (W : FiniteEtale X) [IsConnected W] :
    connectedCoverGenericNormalizationDesc W ≫ W.hom =
      (connectedCoverGenericComposite W).fromNormalization

def

normalizationSourceIso

L154 ↗

AlgebraicGeometry.FiniteEtale.normalizationSourceIso

Documentation

Relative normalization is unchanged when the source of the morphism is replaced by an isomorphic scheme.

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

def normalizationSourceIso
    {Y Y' Z : Scheme.{u}} (e : Y ≅ Y') (f : Y' ⟶ Z)
    [QuasiCompact f] [QuasiSeparated f] :
    (e.hom ≫ f).normalization ≅ f.normalization

lemma

normalizationSourceIso_hom_fromNormalization

L178 ↗

AlgebraicGeometry.FiniteEtale.normalizationSourceIso_hom_fromNormalization

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

lemma normalizationSourceIso_hom_fromNormalization
    {Y Y' Z : Scheme.{u}} (e : Y ≅ Y') (f : Y' ⟶ Z)
    [QuasiCompact f] [QuasiSeparated f] :
    (normalizationSourceIso e f).hom ≫ f.fromNormalization =
      (e.hom ≫ f).fromNormalization

def

normalizationSourceIsoOfEq

L185 ↗

AlgebraicGeometry.FiniteEtale.normalizationSourceIsoOfEq

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

def normalizationSourceIsoOfEq
    {Y Y' Z : Scheme.{u}} (e : Y ≅ Y') (f : Y' ⟶ Z) (g : Y ⟶ Z)
    [QuasiCompact f] [QuasiSeparated f] [QuasiCompact g]
    [QuasiSeparated g] (h : e.hom ≫ f = g) :
    g.normalization ≅ f.normalization

lemma

normalizationSourceIsoOfEq_hom_fromNormalization

L194 ↗

AlgebraicGeometry.FiniteEtale.normalizationSourceIsoOfEq_hom_fromNormalization

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

lemma normalizationSourceIsoOfEq_hom_fromNormalization
    {Y Y' Z : Scheme.{u}} (e : Y ≅ Y') (f : Y' ⟶ Z) (g : Y ⟶ Z)
    [QuasiCompact f] [QuasiSeparated f] [QuasiCompact g]
    [QuasiSeparated g] (h : e.hom ≫ f = g) :
    (normalizationSourceIsoOfEq e f g h).hom ≫ f.fromNormalization =
      g.fromNormalization

theorem

monoFactorIsPullback

L203 ↗

AlgebraicGeometry.FiniteEtale.monoFactorIsPullback

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

theorem monoFactorIsPullback {Y X S : Scheme.{u}}
    (j : X ⟶ S) [Mono j] (f : Y ⟶ X) :
    IsPullback (𝟙 Y) f (f ≫ j) j

def

monoFactorPullbackIso

L209 ↗

AlgebraicGeometry.FiniteEtale.monoFactorPullbackIso

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

def monoFactorPullbackIso {Y X S : Scheme.{u}}
    (j : X ⟶ S) [Mono j] (f : Y ⟶ X) :
    Y ≅ Limits.pullback (f ≫ j) j

lemma

monoFactorPullbackIso_hom_snd

L215 ↗

AlgebraicGeometry.FiniteEtale.monoFactorPullbackIso_hom_snd

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

lemma monoFactorPullbackIso_hom_snd {Y X S : Scheme.{u}}
    (j : X ⟶ S) [Mono j] (f : Y ⟶ X) :
    (monoFactorPullbackIso j f).hom ≫
      Limits.pullback.snd (f ≫ j) j = f

theorem

connectedCoverGenericNormalizationDesc_isIso

L222 ↗

AlgebraicGeometry.FiniteEtale.connectedCoverGenericNormalizationDesc_isIso

Documentation

The generic normalization of a connected finite étale cover is the cover itself.

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

theorem connectedCoverGenericNormalizationDesc_isIso
    (W : FiniteEtale X) [IsConnected W] :
    IsIso (connectedCoverGenericNormalizationDesc W)

def

connectedCoverGenericNormalizationIso

L230 ↗

AlgebraicGeometry.FiniteEtale.connectedCoverGenericNormalizationIso

Documentation

The relative normalization in the function field of a connected finite-etale cover is canonically the cover itself.

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

def connectedCoverGenericNormalizationIso
    (W : FiniteEtale X) [IsConnected W] :
    (connectedCoverGenericComposite W).normalization ≅ W.left

theorem

connectedCoverGenericNormalizationIso_inv_fromNormalization

L237 ↗

AlgebraicGeometry.FiniteEtale.connectedCoverGenericNormalizationIso_inv_fromNormalization

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

theorem connectedCoverGenericNormalizationIso_inv_fromNormalization
    (W : FiniteEtale X) [IsConnected W] :
    (connectedCoverGenericNormalizationIso W).inv ≫
        (connectedCoverGenericComposite W).fromNormalization =
      W.hom

def

connectedCoverGenericNormalizationPullbackIso

L250 ↗

AlgebraicGeometry.FiniteEtale.connectedCoverGenericNormalizationPullbackIso

Documentation

If X maps smoothly and monomorphically to an ambient scheme, the normalization of that ambient scheme in the function field of a connected finite-etale cover restricts canonically to the original cover on X.

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

def connectedCoverGenericNormalizationPullbackIso
    {S : Scheme.{u}} (W : FiniteEtale X) [IsConnected W]
    (j : X ⟶ S) [Mono j] [Smooth j] [QuasiCompact j]
    [QuasiSeparated j] :
    W.left ≅ Limits.pullback
      (connectedCoverGenericComposite W ≫ j).fromNormalization j

theorem

connectedCoverGenericNormalizationPullbackIso_hom_snd

L270 ↗

AlgebraicGeometry.FiniteEtale.connectedCoverGenericNormalizationPullbackIso_hom_snd

Source context 9 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
private local instance connectedLeftIntegral
    (W : FiniteEtale X) [IsConnected W] : IsIntegral W.left :=
  EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
private local instance connectedLeftNormal
    (W : FiniteEtale X) [IsConnected W] : IsNormalIntegral W.left :=
  EtaleFundamentalGroups.isNormalIntegral_left_of_isConnected_finiteEtale W

Lean source · statement

theorem connectedCoverGenericNormalizationPullbackIso_hom_snd
    {S : Scheme.{u}} (W : FiniteEtale X) [IsConnected W]
    (j : X ⟶ S) [Mono j] [Smooth j] [QuasiCompact j]
    [QuasiSeparated j] :
    (connectedCoverGenericNormalizationPullbackIso W j).hom ≫
        Limits.pullback.snd
          (connectedCoverGenericComposite W ≫ j).fromNormalization j =
      W.hom

Module documentation

Restricting connected function-field normalizations

Declarations