NYLL
Module

ThickeningGluing.lean

Nyll.SchemeTheory.FiniteEtale.ThickeningGluing
10 declarations indexed from sourceView source ↗

Module documentation

Gluing finite étale lifts across a thickening

Local finite étale lifts represent the same presheaf of maps after pullback. Their universal elements therefore supply compatible transition maps and cartesian squares on the directed affine cover. Gluing these local representers produces a finite étale lift over the whole target.

Imports19
Imported by2

Declarations

instance

finiteEtaleInfStableUnderBaseChangeThickeningGluing

L49 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleInfStableUnderBaseChangeThickeningGluing
Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite
open SchemeTheory.WeilRestriction
noncomputable section
universe u
namespace AlgebraicGeometry.FiniteEtale
Lean source · statement
instance finiteEtaleInfStableUnderBaseChangeThickeningGluing :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale)
def

pullbackMapLeftIso

L56 ↗
AlgebraicGeometry.FiniteEtale.pullbackMapLeftIso
Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite
open SchemeTheory.WeilRestriction
noncomputable section
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickeningGluing :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y U : Scheme.{u}}
Lean source · statement
def pullbackMapLeftIso (i : X ⟶ Y) (u : U ⟶ Y) (T : Over U) :
    Limits.pullback T.hom (Limits.pullback.snd i u) ≅ Limits.pullback (T.hom ≫ u) i
lemma

pullbackMapLeftIso_hom_fst

L63 ↗
AlgebraicGeometry.FiniteEtale.pullbackMapLeftIso_hom_fst
Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite
open SchemeTheory.WeilRestriction
noncomputable section
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickeningGluing :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y U : Scheme.{u}}
Lean source · statement
lemma pullbackMapLeftIso_hom_fst (i : X ⟶ Y) (u : U ⟶ Y) (T : Over U) :
    (pullbackMapLeftIso i u T).hom ≫ Limits.pullback.fst (T.hom ≫ u) i =
      Limits.pullback.fst T.hom (Limits.pullback.snd i u)
lemma

pullbackMapLeftIso_hom_snd

L71 ↗
AlgebraicGeometry.FiniteEtale.pullbackMapLeftIso_hom_snd
Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite
open SchemeTheory.WeilRestriction
noncomputable section
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickeningGluing :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y U : Scheme.{u}}
Lean source · statement
lemma pullbackMapLeftIso_hom_snd (i : X ⟶ Y) (u : U ⟶ Y) (T : Over U) :
    (pullbackMapLeftIso i u T).hom ≫ Limits.pullback.snd (T.hom ≫ u) i =
      Limits.pullback.snd T.hom (Limits.pullback.snd i u) ≫ Limits.pullback.fst i u
def

pullbackMapIso

L78 ↗
AlgebraicGeometry.FiniteEtale.pullbackMapIso
Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite
open SchemeTheory.WeilRestriction
noncomputable section
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickeningGluing :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y U : Scheme.{u}}
Lean source · statement
def pullbackMapIso (i : X ⟶ Y) (u : U ⟶ Y) :
    Over.pullback (Limits.pullback.snd i u) ⋙ Over.map (Limits.pullback.fst i u) ≅
      Over.map u ⋙ Over.pullback i
def

restrictionPullbackHomIso

L108 ↗
AlgebraicGeometry.FiniteEtale.restrictionPullbackHomIso
Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite
open SchemeTheory.WeilRestriction
noncomputable section
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickeningGluing :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y U : Scheme.{u}}
Lean source · statement
def restrictionPullbackHomIso (i : X ⟶ Y) (u : U ⟶ Y) (V : Over X) :
    (Over.map u).op ⋙ ((Over.pullback i).op ⋙ yoneda.obj V) ≅
      (Over.pullback (Limits.pullback.snd i u)).op ⋙
        yoneda.obj ((Over.pullback (Limits.pullback.fst i u)).obj V)
lemma

pullbackHom_isSheaf

L119 ↗
AlgebraicGeometry.FiniteEtale.pullbackHom_isSheaf
Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite
open SchemeTheory.WeilRestriction
noncomputable section
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickeningGluing :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y U : Scheme.{u}}
Lean source · statement
lemma pullbackHom_isSheaf (i : X ⟶ Y) (V : Over X) :
    Presheaf.IsSheaf (Scheme.zariskiTopology.over Y)
      ((Over.pullback i).op ⋙ yoneda.obj V)
def

pullbackHomRepresentable

L130 ↗
AlgebraicGeometry.FiniteEtale.pullbackHomRepresentable
Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite
open SchemeTheory.WeilRestriction
noncomputable section
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickeningGluing :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y U : Scheme.{u}}
Lean source · full declaration
def pullbackHomRepresentable
    (i : X ⟶ Y) [IsClosedImmersion i] [Surjective i]
    (W : Over Y) [IsFinite W.hom] [Etale W.hom] :
    ((Over.pullback i).op ⋙ yoneda.obj ((Over.pullback i).obj W)).RepresentableBy W where
  homEquiv {T} := Equiv.ofBijective ((Over.pullback i).map (X := T) (Y := W))
    (pullback_map_bijective_to_finiteEtale i T W)
  homEquiv_comp f g := (Over.pullback i).map_comp f g
theorem

exists_localRepresenter

L138 ↗
AlgebraicGeometry.FiniteEtale.exists_localRepresenter
Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite
open SchemeTheory.WeilRestriction
noncomputable section
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickeningGluing :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y U : Scheme.{u}}
Lean source · statement
theorem exists_localRepresenter
    (i : X ⟶ Y) [IsClosedImmersion i] [Surjective i]
    (u : U ⟶ Y) [IsAffine U]
    (V : MorphismProperty.Over
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ X) :
    ∃ W : Over U, IsFiniteEtale W.hom ∧
      Nonempty (((Over.map u).op ⋙
        ((Over.pullback i).op ⋙ yoneda.obj V.toComma)).RepresentableBy W)
theorem

pullback_essSurj_of_surjective_closedImmersion

L174 ↗
AlgebraicGeometry.FiniteEtale.pullback_essSurj_of_surjective_closedImmersion
Documentation

Finite étale covers lift across an arbitrary surjective closed immersion. The lifts on the directed affine cover glue using their actual representing equivalences, so compatibility on overlaps is part of the construction.

Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite
open SchemeTheory.WeilRestriction
noncomputable section
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickeningGluing :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y U : Scheme.{u}}
Lean source · statement
theorem pullback_essSurj_of_surjective_closedImmersion
    (i : X ⟶ Y) [IsClosedImmersion i] [Surjective i] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ i).EssSurj

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