Module

AffineTransitionOverEquality.lean

Nyll.SchemeTheory.Descent.AffineTransitionOverEquality

3 declarations indexed from sourceView source ↗

Module documentation

Eventual equations of actual relative scheme models

The diagonal and triple objects used in scheme gluing are finite etale over compact overlaps, rather than over the whole ambient stage. Their structural maps to that stage are quasi-compact and locally of finite type. The existing raw affine-transition equality theorem supplies eventual equality of their native Over.pullback maps.

Imports3

Nyll.SchemeTheory.Descent.AffineTransitionHom
Mathlib.CategoryTheory.Comma.Over.Pullback
Mathlib.CategoryTheory.Filtered.Basic

Imported by2

theorem

exists_over_map_eq_later_stage

L31 ↗

AlgebraicGeometry.AffineTransitionHom.exists_over_map_eq_later_stage

Documentation

Morphisms of quasi-compact models into locally finite-type models that agree after limit pullback agree after a later original transition.

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom

Lean source · statement

theorem exists_over_map_eq_later_stage
    {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) {A B : Over (D.obj i)} [QuasiCompact A.hom] [LocallyOfFiniteType B.hom]
    (a b : A ⟶ B)
    (hab : (Over.pullback (c.π.app i)).map a =
      (Over.pullback (c.π.app i)).map b) :
    ∃ (j : I) (hji : j ⟶ i),
      (Over.pullback (D.map hji)).map a =
        (Over.pullback (D.map hji)).map b

theorem

map_eq_of_comparison

L131 ↗

AlgebraicGeometry.AffineTransitionHom.map_eq_of_comparison

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom

Lean source · statement

theorem map_eq_of_comparison
    {C₀ C₁ : Type*} [Category* C₀] [Category* C₁]
    {F G : C₀ ⥤ C₁} (e : F ≅ G) {A B : C₀} (a b : A ⟶ B)
    (h : G.map a = G.map b) : F.map a = F.map b

theorem

exists_over_map_eq_later_stage_family

L140 ↗

AlgebraicGeometry.AffineTransitionHom.exists_over_map_eq_later_stage_family

Documentation

A finite family of relative-scheme equations holds after one common transition when it holds after pullback to the actual limit.

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHom

Lean source · statement

theorem exists_over_map_eq_later_stage_family
    {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) {K : Type v} [Finite K] (A B : K → Over (D.obj i))
    [∀ k : K, QuasiCompact (A k).hom] [∀ k : K, LocallyOfFiniteType (B k).hom]
    (a b : ∀ k : K, A k ⟶ B k)
    (hab : ∀ k : K, (Over.pullback (c.π.app i)).map (a k) =
      (Over.pullback (c.π.app i)).map (b k)) :
    ∃ (j : I) (hji : j ⟶ i), ∀ k : K,
      (Over.pullback (D.map hji)).map (a k) =
        (Over.pullback (D.map hji)).map (b k)

Module documentation

Eventual equations of actual relative scheme models

Declarations

exists_over_map_eq_later_stage

map_eq_of_comparison

exists_over_map_eq_later_stage_family