Module

OpenImmersionPullbackModel.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.OpenImmersionPullbackModel

4 declarations indexed from sourceView source ↗

Module documentation

Open-normal pullback models over open immersions

For a nonempty open immersion into a normal locally Noetherian integral scheme, the pullback of a connected finite-etale cover is connected. Hence the connected component occurring in an open-normal pullback model is the whole pullback.

Imports3

Imported by5

theorem

inclusion_isIso_of_isOpenImmersion

L38 ↗

AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.inclusion_isIso_of_isOpenImmersion

Documentation

Over a nonempty open immersion into a normal locally Noetherian integral scheme, the selected Galois component is the entire pulled-back cover.

Source context 10 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 Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable {f : X ⟶ Y} {xi : Spec (.of Omega) ⟶ X}
variable {U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ f)}

Lean source · statement

theorem inclusion_isIso_of_isOpenImmersion
    [IsIntegral Y] [IsNormalIntegral Y] [IsLocallyNoetherian Y]
    [IsOpenImmersion f] [Nonempty X]
    (M : OpenNormalPullbackModel f xi U) : IsIso M.inclusion

def

sourceIsoPullback_of_isOpenImmersion

L53 ↗

AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.sourceIsoPullback_of_isOpenImmersion

Documentation

The scheme underlying the selected component is canonically isomorphic to the scheme underlying the entire pulled-back cover.

Source context 10 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 Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable {f : X ⟶ Y} {xi : Spec (.of Omega) ⟶ X}
variable {U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ f)}

Lean source · statement

def sourceIsoPullback_of_isOpenImmersion
    [IsIntegral Y] [IsNormalIntegral Y] [IsLocallyNoetherian Y]
    [IsOpenImmersion f] [Nonempty X]
    (M : OpenNormalPullbackModel f xi U) :
    M.sourceScheme ≅ ((pullback f).obj M.targetCover).left

def

pullbackSupportComplementIso

L70 ↗

AlgebraicGeometry.FiniteEtale.pullbackSupportComplementIso

Documentation

Pulling a finite-etale cover back to the support complement of an ideal sheaf gives the support complement of the pulled-back ideal sheaf.

Source context 5 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

def pullbackSupportComplementIso
    {Y : Scheme.{u}} (I : Y.IdealSheafData) (A : FiniteEtale Y) :
    ((pullback I.supportComplement.ι).obj A).left ≅
      (I.comap A.hom).supportComplement

def

sourceIsoPulledSupportComplement

L84 ↗

AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.sourceIsoPulledSupportComplement

Documentation

For a boundary complement, the source scheme of an open-normal model is the support complement of the boundary pulled back to its target cover.

Source context 8 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 {Y : Scheme.{u}} [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]

Lean source · statement

def sourceIsoPulledSupportComplement
    [IsIntegral Y] [IsNormalIntegral Y] [IsLocallyNoetherian Y]
    (I : Y.IdealSheafData) [ConnectedSpace I.supportComplement]
    [Nonempty I.supportComplement]
    (xi : Spec (.of Omega) ⟶ I.supportComplement)
    (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U) :
    M.sourceScheme ≅ (I.comap M.targetCover.hom).supportComplement

Module documentation

Open-normal pullback models over open immersions

Declarations

inclusion_isIso_of_isOpenImmersion

sourceIsoPullback_of_isOpenImmersion

pullbackSupportComplementIso

sourceIsoPulledSupportComplement