NYLL
Module

AffineTransitionHom.lean

Nyll.SchemeTheory.Descent.AffineTransitionHom
12 declarations indexed from sourceView source ↗

Module documentation

Morphisms between models over an inverse limit

For a cofiltered diagram of qcqs schemes with affine transition maps, a morphism between two base-changed models descends to an actual stage. The source model is qcqs over the base and the target is locally of finite presentation. All base changes are the native chosen pullbacks, and the recovery assertion is the literal commuting square between them.

This supplies the morphism and eventual-equality parts of Stacks 01ZM for the finite-etale limit theorem 0BTV. It does not assert descent of objects or eventual finiteness or etaleness. No integrality or Noetherian condition on the diagram is used.

Imports10
  • Mathlib.AlgebraicGeometry.AffineTransitionLimit
  • Mathlib.AlgebraicGeometry.Morphisms.Affine
  • Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
  • Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
  • Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
  • Mathlib.CategoryTheory.Adjunction.Limits
  • Mathlib.CategoryTheory.Comma.Over.Pullback
  • Mathlib.CategoryTheory.Filtered.Connected
  • Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
  • Mathlib.CategoryTheory.MorphismProperty.Limits
Imported by8

Declarations

abbrev

diagram

L44 ↗
AlgebraicGeometry.AffineTransitionHom.diagram
Documentation

The actual pullbacks of a model along the coefficient diagram.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S Y Z : Scheme.{u}}
    (D : I ⥤ Over S) (c : Cone D)
Lean source · full declaration
abbrev diagram (f : Y ⟶ S) : I ⥤ Scheme.{u} where
  obj i := pullback (D.obj i).hom f
  map h := ((Over.pullback f).map (D.map h)).left
  map_id i := (D ⋙ Over.pullback f ⋙ Over.forget Y).map_id i
  map_comp h k := (D ⋙ Over.pullback f ⋙ Over.forget Y).map_comp h k
abbrev

cone

L52 ↗
AlgebraicGeometry.AffineTransitionHom.cone
Documentation

The actual pullback of the limiting coefficient scheme and its maps to the stage pullbacks.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S Y Z : Scheme.{u}}
    (D : I ⥤ Over S) (c : Cone D)
Lean source · full declaration
abbrev cone (f : Y ⟶ S) : Cone (diagram D f) where
  pt := pullback c.pt.hom f
  π :=
    { app i := ((Over.pullback f).map (c.π.app i)).left
      naturality _ _ h :=
        ((Over.pullback f ⋙ Over.forget Y).mapCone c).π.naturality h }
def

projection

L60 ↗
AlgebraicGeometry.AffineTransitionHom.projection
Documentation

The structure maps of the pullback diagram to its original base.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S Y Z : Scheme.{u}}
    (D : I ⥤ Over S) (c : Cone D)
Lean source · full declaration
def projection (f : Y ⟶ S) : diagram D f ⟶ (Functor.const I).obj S where
  app i := pullback.snd (D.obj i).hom f ≫ f
  naturality i j h := by
    change ((Over.pullback f).map (D.map h)).left ≫
        (pullback.snd (D.obj j).hom f ≫ f) =
      (pullback.snd (D.obj i).hom f ≫ f) ≫ 𝟙 S
    have hw : ((Over.pullback f).map (D.map h)).left ≫
        pullback.snd (D.obj j).hom f = pullback.snd (D.obj i).hom f :=
      Over.w ((Over.pullback f).map (D.map h))
    rw [Category.comp_id, ← Category.assoc, hw]
theorem

cone_map_snd

L72 ↗
AlgebraicGeometry.AffineTransitionHom.cone_map_snd
Documentation

Cone maps commute with the projection to the original model.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S Y Z : Scheme.{u}}
    (D : I ⥤ Over S) (c : Cone D)
Lean source · statement
theorem cone_map_snd (f : Y ⟶ S) (i : I) :
    (cone D c f).π.app i ≫ pullback.snd (D.obj i).hom f =
      pullback.snd c.pt.hom f
theorem

cone_map_fst

L78 ↗
AlgebraicGeometry.AffineTransitionHom.cone_map_fst
Documentation

Cone maps commute with the actual coefficient map.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S Y Z : Scheme.{u}}
    (D : I ⥤ Over S) (c : Cone D)
Lean source · statement
theorem cone_map_fst (f : Y ⟶ S) (i : I) :
    (cone D c f).π.app i ≫ pullback.fst (D.obj i).hom f =
      pullback.fst c.pt.hom f ≫ (c.π.app i).left
def

coneIsLimit

L85 ↗
AlgebraicGeometry.AffineTransitionHom.coneIsLimit
Documentation

Base change preserves this limit; forgetting the structure map preserves it because the indexing category is connected.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S Y Z : Scheme.{u}}
    (D : I ⥤ Over S) (c : Cone D)
Lean source · statement
def coneIsLimit [IsCofiltered I] (hc : IsLimit c) (f : Y ⟶ S) :
    IsLimit (cone D c f)
theorem

diagram_map_isAffineHom

L92 ↗
AlgebraicGeometry.AffineTransitionHom.diagram_map_isAffineHom
Documentation

Every transition in the pulled-back diagram is the base change of the original affine transition.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S Y Z : Scheme.{u}}
    (D : I ⥤ Over S) (c : Cone D)
Lean source · statement
theorem diagram_map_isAffineHom (f : Y ⟶ S)
    [∀ {i j : I} (h : i ⟶ j), IsAffineHom (D.map h).left]
    {i j : I} (h : i ⟶ j) : IsAffineHom ((diagram D f).map h)
theorem

diagram_obj_compactSpace

L100 ↗
AlgebraicGeometry.AffineTransitionHom.diagram_obj_compactSpace
Documentation

The source-model quasi-compactness supplies quasi-compact stage pullbacks.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S Y Z : Scheme.{u}}
    (D : I ⥤ Over S) (c : Cone D)
Lean source · statement
theorem diagram_obj_compactSpace (f : Y ⟶ S) [QuasiCompact f]
    [∀ i : I, CompactSpace (D.obj i).left] (i : I) :
    CompactSpace ((diagram D f).obj i)
theorem

diagram_obj_quasiSeparatedSpace

L107 ↗
AlgebraicGeometry.AffineTransitionHom.diagram_obj_quasiSeparatedSpace
Documentation

The source-model quasi-separatedness supplies quasi-separated stage pullbacks over the original qcqs coefficient schemes.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S Y Z : Scheme.{u}}
    (D : I ⥤ Over S) (c : Cone D)
Lean source · statement
theorem diagram_obj_quasiSeparatedSpace (f : Y ⟶ S) [QuasiSeparated f]
    [∀ i : I, QuasiSeparatedSpace (D.obj i).left] (i : I) :
    QuasiSeparatedSpace ((diagram D f).obj i)
theorem

exists_hom_stage

L118 ↗
AlgebraicGeometry.AffineTransitionHom.exists_hom_stage
Documentation

An arbitrary morphism over the limit between two pulled-back models descends to a stage, with its exact recovery square.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S Y Z : Scheme.{u}}
    (D : I ⥤ Over S) (c : Cone D)
Lean source · statement
theorem exists_hom_stage [IsCofiltered I] (hc : IsLimit c)
    [∀ {i j : I} (h : i ⟶ j), IsAffineHom (D.map h).left]
    [∀ i : I, CompactSpace (D.obj i).left]
    [∀ i : I, QuasiSeparatedSpace (D.obj i).left]
    (f : Y ⟶ S) (g : Z ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    [LocallyOfFinitePresentation g]
    (a : pullback c.pt.hom f ⟶ pullback c.pt.hom g)
    (ha : a ≫ pullback.fst c.pt.hom g = pullback.fst c.pt.hom f) :
    ∃ (i : I) (b : pullback (D.obj i).hom f ⟶ pullback (D.obj i).hom g),
      b ≫ pullback.fst (D.obj i).hom g = pullback.fst (D.obj i).hom f ∧
      (cone D c f).π.app i ≫ b = a ≫ (cone D c g).π.app i
theorem

exists_eq_stage

L167 ↗
AlgebraicGeometry.AffineTransitionHom.exists_eq_stage
Documentation

Equality of two morphisms of stage models is detected after an actual transition. Equality is stated in the original stage target; both maps also have the same coefficient projection, so it determines equality of their base changes to the later stage.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S Y Z : Scheme.{u}}
    (D : I ⥤ Over S) (c : Cone D)
Lean source · statement
theorem exists_eq_stage [IsCofiltered I] (hc : IsLimit c)
    [∀ {i j : I} (h : i ⟶ j), IsAffineHom (D.map h).left]
    [∀ i : I, CompactSpace (D.obj i).left]
    (f : Y ⟶ S) (g : Z ⟶ S) [QuasiCompact f] [LocallyOfFiniteType g]
    (i : I)
    (a b : pullback (D.obj i).hom f ⟶ pullback (D.obj i).hom g)
    (ha : a ≫ pullback.fst (D.obj i).hom g = pullback.fst (D.obj i).hom f)
    (hb : b ≫ pullback.fst (D.obj i).hom g = pullback.fst (D.obj i).hom f)
    (hab : (cone D c f).π.app i ≫ a = (cone D c f).π.app i ≫ b) :
    ∃ (j : I) (hji : j ⟶ i),
      (diagram D f).map hji ≫ a = (diagram D f).map hji ≫ b
theorem

exists_hom_later_stage

L209 ↗
AlgebraicGeometry.AffineTransitionHom.exists_hom_later_stage
Documentation

The original scheme-diagram form: models and maps over any fixed stage descend farther along the same diagram. The limit supplied here is the actual original limit, and the later stage map is produced rather than assumed.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S Y Z : Scheme.{u}}
    (D : I ⥤ Over S) (c : Cone D)
Lean source · statement
theorem exists_hom_later_stage
    (F : I ⥤ Scheme.{u}) (s : Cone F) [IsCofiltered I] (hs : IsLimit s)
    [∀ {i j : I} (h : i ⟶ j), IsAffineHom (F.map h)]
    [∀ i : I, CompactSpace (F.obj i)] [∀ i : I, QuasiSeparatedSpace (F.obj i)]
    (i : I) (f : Y ⟶ F.obj i) (g : Z ⟶ F.obj i)
    [QuasiCompact f] [QuasiSeparated f] [LocallyOfFinitePresentation g]
    (a : pullback (s.π.app i) f ⟶ pullback (s.π.app i) g)
    (ha : a ≫ pullback.fst (s.π.app i) g = pullback.fst (s.π.app i) f) :
    ∃ (j : I) (hji : j ⟶ i)
      (b : pullback (F.map hji) f ⟶ pullback (F.map hji) g),
      b ≫ pullback.fst (F.map hji) g = pullback.fst (F.map hji) f ∧
      ((Over.pullback f).map
        (Over.homMk (s.π.app j) (s.w hji) :
          Over.mk (s.π.app i) ⟶ Over.mk (F.map hji))).left ≫ b =
      a ≫ ((Over.pullback g).map
        (Over.homMk (s.π.app j) (s.w hji) :
          Over.mk (s.π.app i) ⟶ Over.mk (F.map hji))).left

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