NYLL
Module

AffineTransitionImageLimit.lean

Nyll.SchemeTheory.Descent.AffineTransitionImageLimit
6 declarations indexed from sourceView source ↗

Module documentation

Recovering a closed subscheme from its stage images

Sections on affine preimages descend to an actual ambient stage. This detects the kernel of a quasi-compact morphism from its stage kernels and supplies the universal property of the corresponding scheme-theoretic image limit.

Imports2
Imported by2

Declarations

theorem

exists_affine_preimage_section

L31 ↗
AlgebraicGeometry.AffineTransitionImage.exists_affine_preimage_section
Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] [IsCofiltered I]
  (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
  [∀ {i k} (f : i ⟶ k), IsAffineHom (D.map f)]
include hc in
Lean source · full declaration
theorem exists_affine_preimage_section (i : I) (V : (D.obj i).Opens)
    (hV : IsAffineOpen V) (s : Γ(c.pt, c.π.app i ⁻¹ᵁ V)) :
    ∃ (k : I) (f : k ⟶ i) (t : Γ(D.obj k, D.map f ⁻¹ᵁ V)),
      (c.π.app k).appLE (D.map f ⁻¹ᵁ V) (c.π.app i ⁻¹ᵁ V)
        (by rw [← Scheme.Hom.comp_preimage, c.w f]) t = s := by
  have (k : Over i) : IsAffine ((opensDiagram D i V).obj k) :=
    hV.preimage (D.map k.hom)
  obtain ⟨k, t, ht⟩ := exists_appTop_π_eq_of_isAffine_of_isLimit
    (opensDiagram D i V) (opensCone D c i V) (isLimitOpensCone D c hc i V)
    ((c.π.app i ⁻¹ᵁ V).topIso.inv s)
  let t' : Γ((D.map k.hom ⁻¹ᵁ V).toScheme, ⊤) := t
  have ht' : ((c.π.app k.left).resLE (D.map k.hom ⁻¹ᵁ V) (c.π.app i ⁻¹ᵁ V)
      (by rw [← Scheme.Hom.comp_preimage, c.w k.hom])).appTop t' =
        (c.π.app i ⁻¹ᵁ V).topIso.inv s := ht
  refine ⟨k.left, k.hom, (D.map k.hom ⁻¹ᵁ V).topIso.hom t', ?_⟩
  apply (c.π.app i ⁻¹ᵁ V).topIso.commRingCatIsoToRingEquiv.symm.injective
  change (c.π.app i ⁻¹ᵁ V).topIso.inv
      ((c.π.app k.left).appLE _ _ _ ((D.map k.hom ⁻¹ᵁ V).topIso.hom t')) =
    (c.π.app i ⁻¹ᵁ V).topIso.inv s
  rw [Scheme.Hom.appTop, Scheme.Hom.resLE_app_top] at ht'
  exact ht'
lemma

appLE_eq_zero_of_mem_ker

L53 ↗
AlgebraicGeometry.AffineTransitionImage.appLE_eq_zero_of_mem_ker
Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] [IsCofiltered I]
  (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
  [∀ {i k} (f : i ⟶ k), IsAffineHom (D.map f)]
Lean source · statement
lemma appLE_eq_zero_of_mem_ker {X Y : Scheme.{u}} (f : X ⟶ Y)
    (U : Y.affineOpens) (V : X.Opens) (h : V ≤ f ⁻¹ᵁ U)
    (s : Γ(Y, U)) (hs : s ∈ f.ker.ideal U) : f.appLE U V h s = 0
lemma

mem_ker_of_appLE_eq_zero

L59 ↗
AlgebraicGeometry.AffineTransitionImage.mem_ker_of_appLE_eq_zero
Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] [IsCofiltered I]
  (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
  [∀ {i k} (f : i ⟶ k), IsAffineHom (D.map f)]
Lean source · statement
lemma mem_ker_of_appLE_eq_zero {X Y : Scheme.{u}} (f : X ⟶ Y)
    [QuasiCompact f] (U : Y.affineOpens) (V : X.Opens) (h : V = f ⁻¹ᵁ U)
    (s : Γ(Y, U)) (hs : f.appLE U V h.le s = 0) : s ∈ f.ker.ideal U
lemma

app_eq_zero_of_stage_kernel_le

L67 ↗
AlgebraicGeometry.AffineTransitionImage.app_eq_zero_of_stage_kernel_le
Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] [IsCofiltered I]
  (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
  [∀ {i k} (f : i ⟶ k), IsAffineHom (D.map f)]
Lean source · statement
lemma app_eq_zero_of_stage_kernel_le {X Y Z T : Scheme.{u}}
    (p : X ⟶ Y) [QuasiCompact p] (j : Z ⟶ X) [QuasiCompact j] (g : T ⟶ X)
    (U : Y.affineOpens) (V : X.Opens) (hpre : V = p ⁻¹ᵁ U)
    (s : Γ(X, V)) (t : Γ(Y, U)) (ht : p.appLE U V hpre.le t = s)
    (hjs : j.app V s = 0) (h : (j ≫ p).ker ≤ (g ≫ p).ker) :
    g.app V s = 0
theorem

ker_le_of_stage_ker_le

L91 ↗
AlgebraicGeometry.AffineTransitionImage.ker_le_of_stage_ker_le
Documentation

Kernels into an affine-transition limit are detected by the actual kernels at the ambient stages. The source of the second morphism need not be compact.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] [IsCofiltered I]
  (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
  [∀ {i k} (f : i ⟶ k), IsAffineHom (D.map f)]
include hc in
Lean source · statement
theorem ker_le_of_stage_ker_le [∀ i, QuasiSeparatedSpace (D.obj i)]
    {Z T : Scheme.{u}} (j : Z ⟶ c.pt) [QuasiCompact j] (g : T ⟶ c.pt)
    (h : ∀ i, (j ≫ c.π.app i).ker ≤ (g ≫ c.π.app i).ker) :
    j.ker ≤ g.ker
def

coneIsLimit

L112 ↗
AlgebraicGeometry.AffineTransitionImage.coneIsLimit
Documentation

A closed subscheme of an affine-transition limit is the limit of its actual scheme-theoretic images at the ambient stages.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] [IsCofiltered I]
  (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
  [∀ {i k} (f : i ⟶ k), IsAffineHom (D.map f)]
Lean source · statement
def coneIsLimit [∀ i, QuasiSeparatedSpace (D.obj i)]
    {Z : Scheme.{u}} (j : Z ⟶ c.pt) [IsClosedImmersion j] :
    IsLimit (cone D c j)

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