NYLL
Module

InverseLimitIsoModels.lean

Nyll.SchemeTheory.FiniteEtale.InverseLimitIsoModels
7 declarations indexed from sourceView source ↗

Module documentation

Isomorphisms between finite-etale models at a later stage

Combine actual Hom descent, eventual invertibility, and pullback-composition coherence. The resulting isomorphism recovers the originally supplied map.

Imports1
Imported by3

Declarations

instance

finiteEtaleOverCategoryIsoModels

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

finiteEtaleHasPullbacksAlongIsoModels

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

finiteEtaleStableUnderBaseChangeAlongIsoModels

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

isIso_of_recovered_iso

L41 ↗
AlgebraicGeometry.FiniteEtale.isIso_of_recovered_iso
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 finiteEtaleOverCategoryIsoModels (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongIsoModels
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongIsoModels
    {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 isIso_of_recovered_iso
    {C₀ C₁ C₂ : Type*} [Category* C₀] [Category* C₁] [Category* C₂]
    (F : C₀ ⥤ C₂) (U : C₀ ⥤ C₁) (V : C₁ ⥤ C₂) (e : F ≅ U ⋙ V)
    {A B : C₀} (a : F.obj A ≅ F.obj B) (b : U.obj A ⟶ U.obj B)
    (hb : e.hom.app A ≫ V.map b = a.hom ≫ e.hom.app B) : IsIso (V.map b)
theorem

extend_recovered_map

L54 ↗
AlgebraicGeometry.FiniteEtale.extend_recovered_map
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 finiteEtaleOverCategoryIsoModels (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongIsoModels
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongIsoModels
    {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 extend_recovered_map
    {C₀ C₁ C₂ C₃ : Type*}
    [Category* C₀] [Category* C₁] [Category* C₂] [Category* C₃]
    (F : C₀ ⥤ C₃) (U : C₀ ⥤ C₁) (W : C₁ ⥤ C₂)
    (V : C₁ ⥤ C₃) (V' : C₂ ⥤ C₃) (T : C₀ ⥤ C₂)
    (e : F ≅ U ⋙ V) (e' : V ≅ W ⋙ V') (E : T ≅ U ⋙ W)
    (eT : F ≅ T ⋙ V')
    (hcomp : ∀ Q : C₀, V'.map (E.inv.app Q) ≫ eT.inv.app Q =
      e'.inv.app (U.obj Q) ≫ e.inv.app Q)
    {A B : C₀} (a : F.obj A ⟶ F.obj B) (b : U.obj A ⟶ U.obj B)
    (hb : e.hom.app A ≫ V.map b = a ≫ e.hom.app B) :
    eT.hom.app A ≫ V'.map (E.hom.app A ≫ W.map b ≫ E.inv.app B) =
      a ≫ eT.hom.app B
theorem

exists_inverse_limit_stage_iso_later

L104 ↗
AlgebraicGeometry.FiniteEtale.exists_inverse_limit_stage_iso_later
Documentation

A recovered stage isomorphism retains its recovery at every 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 finiteEtaleOverCategoryIsoModels (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongIsoModels
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongIsoModels
    {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_iso_later
    {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
    {i j k : I} (hji : j ⟶ i) (hkj : k ⟶ j)
    (A B : FiniteEtale (D.obj i))
    (a : (FiniteEtale.pullback (c.π.app i)).obj A ≅
      (FiniteEtale.pullback (c.π.app i)).obj B)
    (b : (FiniteEtale.pullback (D.map hji)).obj A ≅
      (FiniteEtale.pullback (D.map hji)).obj B)
    (hb : (inverseLimitPullbackComparison D c hji).hom.app A ≫
        (FiniteEtale.pullback (c.π.app j)).map b.hom =
      a.hom ≫ (inverseLimitPullbackComparison D c hji).hom.app B) :
    ∃ b' : (FiniteEtale.pullback (D.map (hkj ≫ hji))).obj A ≅
        (FiniteEtale.pullback (D.map (hkj ≫ hji))).obj B,
      (inverseLimitPullbackComparison D c (hkj ≫ hji)).hom.app A ≫
          (FiniteEtale.pullback (c.π.app k)).map b'.hom =
        a.hom ≫ (inverseLimitPullbackComparison D c (hkj ≫ hji)).hom.app B
theorem

exists_inverse_limit_stage_iso

L139 ↗
AlgebraicGeometry.FiniteEtale.exists_inverse_limit_stage_iso
Documentation

An isomorphism of limit pullbacks is induced by an actual isomorphism of the two native models at a later original 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 finiteEtaleOverCategoryIsoModels (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongIsoModels
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongIsoModels
    {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_iso
    {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.hom =
        a.hom ≫ (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.