NYLL
Module

InverseLimitHom.lean

Nyll.SchemeTheory.FiniteEtale.InverseLimitHom
9 declarations indexed from sourceView source ↗

Module documentation

Native finite-etale morphisms descend along inverse limits

Translate the actual scheme Hom descent through pullback symmetry and retain the canonical pullback-composition comparison. The output is a morphism in the native finite-etale category with its categorical recovery equation.

Imports3
Imported by5

Declarations

instance

finiteEtaleOverCategoryLimitHom

L27 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategoryLimitHom
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 finiteEtaleOverCategoryLimitHom (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X)
instance

finiteEtaleHasPullbacksAlongLimitHom

L32 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongLimitHom
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 finiteEtaleOverCategoryLimitHom (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
Lean source · statement
instance finiteEtaleHasPullbacksAlongLimitHom
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
instance

finiteEtaleStableUnderBaseChangeAlongLimitHom

L38 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongLimitHom
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 finiteEtaleOverCategoryLimitHom (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongLimitHom
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
Lean source · statement
instance finiteEtaleStableUnderBaseChangeAlongLimitHom
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
abbrev

rawToStage

L45 ↗
AlgebraicGeometry.FiniteEtale.rawToStage
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryLimitHom (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongLimitHom
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongLimitHom
    {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
abbrev rawToStage {L T S Y : Scheme.{u}}
    (p : L ⟶ S) (q : T ⟶ S) (r : L ⟶ T) (w : r ≫ q = p) (f : Y ⟶ S) :
    Limits.pullback p f ⟶ Limits.pullback q f
def

toStage

L50 ↗
AlgebraicGeometry.FiniteEtale.toStage
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryLimitHom (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongLimitHom
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongLimitHom
    {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 toStage {L T S Y : Scheme.{u}}
    (p : L ⟶ S) (q : T ⟶ S) (r : L ⟶ T) (w : r ≫ q = p) (f : Y ⟶ S) :
    Limits.pullback f p ⟶ Limits.pullback f q
theorem

toStage_eq_symmetry

L56 ↗
AlgebraicGeometry.FiniteEtale.toStage_eq_symmetry
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryLimitHom (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongLimitHom
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongLimitHom
    {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 toStage_eq_symmetry {L T S Y : Scheme.{u}}
    (p : L ⟶ S) (q : T ⟶ S) (r : L ⟶ T) (w : r ≫ q = p) (f : Y ⟶ S) :
    toStage p q r w f = (pullbackSymmetry p f).inv ≫
      rawToStage p q r w f ≫ (pullbackSymmetry q f).hom
theorem

pullbackComp_hom_toStage

L79 ↗
AlgebraicGeometry.FiniteEtale.pullbackComp_hom_toStage
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryLimitHom (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongLimitHom
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongLimitHom
    {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 pullbackComp_hom_toStage {L T S : Scheme.{u}}
    (p : L ⟶ S) (q : T ⟶ S) (r : L ⟶ T) (w : r ≫ q = p) (A : FiniteEtale S) :
    ((MorphismProperty.Over.pullbackComp
      (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) (Q := ⊤)
      r q p w.symm).hom.app A).left ≫
        Limits.pullback.fst (Limits.pullback.snd A.hom q) r = toStage p q r w A.hom
def

inverseLimitPullbackComparison

L114 ↗
AlgebraicGeometry.FiniteEtale.inverseLimitPullbackComparison
Documentation

The canonical comparison from a model pulled directly to the limit to the same model pulled through a later stage.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryLimitHom (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongLimitHom
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongLimitHom
    {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 inverseLimitPullbackComparison
    {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
    {i j : I} (h : j ⟶ i) :
    FiniteEtale.pullback (c.π.app i) ≅
      FiniteEtale.pullback (D.map h) ⋙ FiniteEtale.pullback (c.π.app j)
theorem

exists_inverse_limit_stage_hom

L126 ↗
AlgebraicGeometry.FiniteEtale.exists_inverse_limit_stage_hom
Documentation

An arbitrary morphism between pulled-back finite-etale models descends to a later original stage. Recovery uses the native pullback-composition comparison, not a separate assumed compatibility.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryLimitHom (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongLimitHom
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongLimitHom
    {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_inverse_limit_stage_hom
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [∀ {i j : I} (h : i ⟶ j), IsAffineHom (D.map h)]
    [∀ i : I, CompactSpace (D.obj i)] [∀ i : I, QuasiSeparatedSpace (D.obj i)]
    (i : I) (A B : FiniteEtale (D.obj i))
    (a : (FiniteEtale.pullback (c.π.app i)).obj A ⟶
      (FiniteEtale.pullback (c.π.app i)).obj B) :
    ∃ (j : I) (hji : j ⟶ i)
      (b : (FiniteEtale.pullback (D.map hji)).obj A ⟶
        (FiniteEtale.pullback (D.map hji)).obj B),
      (inverseLimitPullbackComparison D c hji).hom.app A ≫
          (FiniteEtale.pullback (c.π.app j)).map b =
        a ≫ (inverseLimitPullbackComparison D c hji).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.