NYLL
Module

AffineTransitionOverlapRecovery.lean

Nyll.SchemeTheory.FiniteEtale.AffineTransitionOverlapRecovery
8 declarations indexed from sourceView source ↗

Module documentation

Actual overlap comparisons from recovered local models

Restrict a recovered local model to any smaller base open. The literal inclusions commute with the restricted cone maps, so native pullback composition transports its given recovery to the restriction of the same original cover. On an overlap the two resulting recovery isomorphisms have the identical target, and their composition supplies the overlap isomorphism.

The only model data here are the local models and their already constructed recoveries to the original cover. No overlap comparison is an input.

Imports3
Imported by1

Declarations

instance

finiteEtaleOverCategoryOverlapRecovery

L32 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategoryOverlapRecovery
Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
Lean source · statement
instance finiteEtaleOverCategoryOverlapRecovery (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X)
instance

finiteEtaleHasPullbacksAlongOverlapRecovery

L36 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongOverlapRecovery
Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryOverlapRecovery (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
Lean source · statement
instance finiteEtaleHasPullbacksAlongOverlapRecovery
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
instance

finiteEtaleStableUnderBaseChangeAlongOverlapRecovery

L42 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongOverlapRecovery
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryOverlapRecovery (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongOverlapRecovery
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
Lean source · statement
instance finiteEtaleStableUnderBaseChangeAlongOverlapRecovery
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
def

openStageInclusion

L52 ↗
AlgebraicGeometry.FiniteEtale.openStageInclusion
Documentation

The literal inclusion between two stage preimages of nested opens.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryOverlapRecovery (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongOverlapRecovery
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongOverlapRecovery
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
Lean source · statement
def openStageInclusion (i : I) (U V : (D.obj i).Opens) (h : V ≤ U) (t : Over i) :
    (D.map t.hom ⁻¹ᵁ V).toScheme ⟶ (D.map t.hom ⁻¹ᵁ U).toScheme
def

openLimitInclusion

L57 ↗
AlgebraicGeometry.FiniteEtale.openLimitInclusion
Documentation

The literal inclusion between two cone preimages of nested opens.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryOverlapRecovery (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongOverlapRecovery
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongOverlapRecovery
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
Lean source · statement
def openLimitInclusion (i : I) (U V : (D.obj i).Opens) (h : V ≤ U) :
    (c.π.app i ⁻¹ᵁ V).toScheme ⟶ (c.π.app i ⁻¹ᵁ U).toScheme
theorem

openInclusion_cone_map

L62 ↗
AlgebraicGeometry.FiniteEtale.openInclusion_cone_map
Documentation

Stage and limit inclusions commute with the actual restricted cone maps.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryOverlapRecovery (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongOverlapRecovery
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongOverlapRecovery
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
Lean source · statement
theorem openInclusion_cone_map
    (i : I) (U V : (D.obj i).Opens) (h : V ≤ U) (t : Over i) :
    (opensCone D c i V).π.app t ≫ openStageInclusion D i U V h t =
      openLimitInclusion D c i U V h ≫ (opensCone D c i U).π.app t
def

recoveredRestrictionIso

L90 ↗
AlgebraicGeometry.FiniteEtale.recoveredRestrictionIso
Documentation

Restricting a recovered local model recovers the restriction of the same original finite-etale cover, through the literal native pullback comparisons.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryOverlapRecovery (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongOverlapRecovery
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongOverlapRecovery
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
Lean source · statement
def recoveredRestrictionIso
    (i : I) (U V : (D.obj i).Opens) (h : V ≤ U) (t : Over i)
    (X : FiniteEtale c.pt) (M : FiniteEtale ((opensDiagram D i U).obj t))
    (e : (FiniteEtale.pullback ((opensCone D c i U).π.app t)).obj M ≅
      (FiniteEtale.pullback (c.π.app i ⁻¹ᵁ U).ι).obj X) :
    (FiniteEtale.pullback ((opensCone D c i V).π.app t)).obj
        ((FiniteEtale.pullback (openStageInclusion D i U V h t)).obj M) ≅
      (FiniteEtale.pullback (c.π.app i ⁻¹ᵁ V).ι).obj X
def

recoveredOverlapIso

L131 ↗
AlgebraicGeometry.FiniteEtale.recoveredOverlapIso
Documentation

The actual limit-overlap isomorphism between two recovered stage models. Its two recovery maps land in the identical restriction of the original X.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryOverlapRecovery (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongOverlapRecovery
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongOverlapRecovery
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
Lean source · statement
def recoveredOverlapIso
    (i : I) (U V : (D.obj i).Opens) (t : Over i) (X : FiniteEtale c.pt)
    (M : FiniteEtale ((opensDiagram D i U).obj t))
    (N : FiniteEtale ((opensDiagram D i V).obj t))
    (eM : (FiniteEtale.pullback ((opensCone D c i U).π.app t)).obj M ≅
      (FiniteEtale.pullback (c.π.app i ⁻¹ᵁ U).ι).obj X)
    (eN : (FiniteEtale.pullback ((opensCone D c i V).π.app t)).obj N ≅
      (FiniteEtale.pullback (c.π.app i ⁻¹ᵁ V).ι).obj X) :
    (FiniteEtale.pullback ((opensCone D c i (U ⊓ V)).π.app t)).obj
        ((FiniteEtale.pullback (openStageInclusion D i U (U ⊓ V) inf_le_left t)).obj M) ≅
      (FiniteEtale.pullback ((opensCone D c i (U ⊓ V)).π.app t)).obj
        ((FiniteEtale.pullback (openStageInclusion D i V (U ⊓ V) inf_le_right t)).obj N)

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