NYLL
Module

PunctureIsoSpreading.lean

Nyll.SchemeTheory.Descent.PunctureIsoSpreading
7 declarations indexed from sourceView source ↗

Module documentation

Isomorphism spreading over a punctured neighborhood

A specified isomorphism of finite étale covers over the part of an actual local spectrum lying in a retrocompact open descends to the intersection with an actual open neighborhood. The original local isomorphism is retained under the native pullback comparisons. This supplies the overlap comparison needed to glue local extensions in Stacks Project, Lemma 58.21.6 (0EY7).

Imports8
Imported by2

Declarations

instance

finiteEtaleOverCategoryPunctureIso

L34 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategoryPunctureIso
Source context 4 commands

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

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

finiteEtaleHasPullbacksAlongPunctureIso

L38 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongPunctureIso
Source context 5 commands

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

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

finiteEtaleStableUnderBaseChangeAlongPunctureIso

L44 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongPunctureIso
Source context 6 commands

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

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

pullbackComp_inv_coherence

L51 ↗
AlgebraicGeometry.FiniteEtale.pullbackComp_inv_coherence
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryPunctureIso (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongPunctureIso
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongPunctureIso
    {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⟩
Lean source · full declaration
theorem pullbackComp_inv_coherence
    {L N M U : Scheme.{u}}
    (r : L ⟶ N) (t : N ⟶ M) (q : M ⟶ U)
    (p : L ⟶ M) (qn : N ⟶ U) (ql : L ⟶ U)
    (hp : p = r ≫ t) (hqn : qn = t ≫ q)
    (hql : ql = p ≫ q) (hql' : ql = r ≫ qn)
    (A : FiniteEtale U) :
    let E := MorphismProperty.Over.pullbackComp
      (P := @IsFiniteEtale) (Q := ⊤) t q qn hqn
    let C := MorphismProperty.Over.pullbackComp
      (P := @IsFiniteEtale) (Q := ⊤) r qn ql hql'
    let D := MorphismProperty.Over.pullbackComp
      (P := @IsFiniteEtale) (Q := ⊤) r t p hp
    let F := MorphismProperty.Over.pullbackComp
      (P := @IsFiniteEtale) (Q := ⊤) p q ql hql
    (pullback r).map (E.inv.app A) ≫ C.inv.app A =
      D.inv.app ((pullback q).obj A) ≫ F.inv.app A := by
  intro E C D F
  let f : A.left ⟶ U := A.hom
  let qt : Limits.pullback f q ⟶ M := Limits.pullback.snd f q
  let qtt : Limits.pullback qt t ⟶ N := Limits.pullback.snd qt t
  let qnA : Limits.pullback f qn ⟶ N := Limits.pullback.snd f qn
  let α : Limits.pullback qtt r ⟶ Limits.pullback qnA r :=
    ((pullback r).map (E.inv.app A)).left
  let β : Limits.pullback qnA r ⟶ Limits.pullback f ql := (C.inv.app A).left
  let δ : Limits.pullback qtt r ⟶ Limits.pullback qt p :=
    (D.inv.app ((pullback q).obj A)).left
  let ε : Limits.pullback qt p ⟶ Limits.pullback f ql := (F.inv.app A).left
  let v : Limits.pullback qt t ⟶ Limits.pullback f qn := (E.inv.app A).left
  have hα : α ≫ Limits.pullback.fst qnA r = Limits.pullback.fst qtt r ≫ v :=
    Limits.pullback.lift_fst _ _ _
  have hβ : β ≫ Limits.pullback.fst f ql =
      Limits.pullback.fst qnA r ≫ Limits.pullback.fst f qn :=
    pullbackComp_inv_app_left_fst r qn ql hql' A
  have hδ : δ ≫ Limits.pullback.fst qt p =
      Limits.pullback.fst qtt r ≫ Limits.pullback.fst qt t :=
    pullbackComp_inv_app_left_fst r t p hp ((pullback q).obj A)
  have hε : ε ≫ Limits.pullback.fst f ql =
      Limits.pullback.fst qt p ≫ Limits.pullback.fst f q :=
    pullbackComp_inv_app_left_fst p q ql hql A
  have hv : v ≫ Limits.pullback.fst f qn =
      Limits.pullback.fst qt t ≫ Limits.pullback.fst f q :=
    pullbackComp_inv_app_left_fst t q qn hqn A
  have hαs : α ≫ Limits.pullback.snd qnA r = Limits.pullback.snd qtt r :=
    MorphismProperty.Over.w ((pullback r).map (E.inv.app A))
  have hβs : β ≫ Limits.pullback.snd f ql = Limits.pullback.snd qnA r :=
    MorphismProperty.Over.w (C.inv.app A)
  have hδs : δ ≫ Limits.pullback.snd qt p = Limits.pullback.snd qtt r :=
    MorphismProperty.Over.w (D.inv.app ((pullback q).obj A))
  have hεs : ε ≫ Limits.pullback.snd f ql = Limits.pullback.snd qt p :=
    MorphismProperty.Over.w (F.inv.app A)
  apply MorphismProperty.Over.Hom.ext
  change α ≫ β = δ ≫ ε
  apply Limits.pullback.hom_ext
  · rw [Category.assoc, hβ, ← Category.assoc, hα, Category.assoc, hv,
      Category.assoc, hε, ← Category.assoc δ, hδ, Category.assoc]
  · rw [Category.assoc, hβs, hαs, Category.assoc, hεs, hδs]
theorem

transport_recovered_iso

L109 ↗
AlgebraicGeometry.FiniteEtale.transport_recovered_iso
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryPunctureIso (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongPunctureIso
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongPunctureIso
    {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⟩
Lean source · statement
theorem transport_recovered_iso
    {C D E F : Type*} [Category* C] [Category* D] [Category* E] [Category* F]
    (P : C ⥤ F) (Q : C ⥤ D) (R : C ⥤ E)
    (V : D ⥤ F) (W : D ⥤ E) (T : E ⥤ F)
    (e : P ≅ Q ⋙ V) (f : V ≅ W ⋙ T)
    (g : R ≅ Q ⋙ W) (h : P ≅ R ⋙ T)
    (hcomp : ∀ A : C, T.map (g.inv.app A) ≫ h.inv.app A =
      f.inv.app (Q.obj A) ≫ e.inv.app A)
    {A B : C} (a : P.obj A ≅ P.obj B)
    (b : (Q ⋙ W).obj A ≅ (Q ⋙ W).obj B)
    (hb : f.hom.app (Q.obj A) ≫ T.map b.hom =
      ((e.app A).symm ≪≫ a ≪≫ e.app B).hom ≫ f.hom.app (Q.obj B)) :
    h.hom.app A ≫ T.map ((g.app A ≪≫ b ≪≫ (g.app B).symm).hom) =
      a.hom ≫ h.hom.app B
def

punctureIsoPullbackComparison

L144 ↗
AlgebraicGeometry.FiniteEtale.punctureIsoPullbackComparison
Documentation

The native comparison from the actual stalk overlap to the overlap with an open neighborhood.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryPunctureIso (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongPunctureIso
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongPunctureIso
    {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⟩
Lean source · statement
def punctureIsoPullbackComparison
    (X : Scheme.{u}) (x : X) (U N : X.Opens) (hxN : x ∈ N) :
    pullback (Limits.pullback.snd (X.fromSpecStalk x) U.ι) ≅
      pullback (Limits.pullback.snd N.ι U.ι) ⋙
        pullback (Scheme.stalkOverlapToNeighborhood X x U N hxN)
theorem

exists_open_overlap_iso_fromSpecStalk

L158 ↗
AlgebraicGeometry.FiniteEtale.exists_open_overlap_iso_fromSpecStalk
Documentation

A specified isomorphism over the stalk overlap descends to an actual open-neighborhood overlap, with its original pullback retained.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryPunctureIso (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongPunctureIso
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongPunctureIso
    {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⟩
Lean source · statement
theorem exists_open_overlap_iso_fromSpecStalk
    (X : Scheme.{u}) [IsAffine X]
    (U : X.Opens) [QuasiCompact U.ι] (x : X)
    (A B : FiniteEtale U.toScheme)
    (a : (pullback (Limits.pullback.snd (X.fromSpecStalk x) U.ι)).obj A ≅
      (pullback (Limits.pullback.snd (X.fromSpecStalk x) U.ι)).obj B) :
    ∃ (N : X.Opens) (hxN : x ∈ N)
      (b : (pullback (Limits.pullback.snd N.ι U.ι)).obj A ≅
        (pullback (Limits.pullback.snd N.ι U.ι)).obj B),
      (punctureIsoPullbackComparison X x U N hxN).hom.app A ≫
          (pullback (Scheme.stalkOverlapToNeighborhood X x U N hxN)).map b.hom =
        a.hom ≫ (punctureIsoPullbackComparison X x U N hxN).hom.app B

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