Nyll.SchemeTheory.Descent.AffineTransitionHomFamily

Module documentation

Simultaneous actual morphism descent for finitely many models

First descend each map, then project its target to the fixed original model. Transport these projected maps along a finite cofiltered cone and reconstruct the maps between stage pullbacks. This retains every original recovery square and does not require an overlap model to be finite over the entire base.

theorem

exists_hom_stage_family

L30 ↗

AlgebraicGeometry.AffineTransitionHom.exists_hom_stage_family

Documentation

Finitely many morphisms of pulled-back qcqs models, with locally finitely presented targets, descend to a single actual coefficient stage.

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_hom_stage_family
    {I : Type u} [Category.{u} I] [IsCofiltered I] {S : Scheme.{u}}
    (D : I ⥤ Over S) (c : Cone D) (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]
    {K : Type v} [Finite K] (Y Z : K → Scheme.{u})
    (f : ∀ k : K, Y k ⟶ S) (g : ∀ k : K, Z k ⟶ S)
    [∀ k : K, QuasiCompact (f k)] [∀ k : K, QuasiSeparated (f k)]
    [∀ k : K, LocallyOfFinitePresentation (g k)]
    (a : ∀ k : K, pullback c.pt.hom (f k) ⟶ pullback c.pt.hom (g k))
    (ha : ∀ k : K, a k ≫ pullback.fst c.pt.hom (g k) = pullback.fst c.pt.hom (f k)) :
    ∃ (i : I) (b : ∀ k : K, pullback (D.obj i).hom (f k) ⟶
      pullback (D.obj i).hom (g k)), ∀ k : K,
        b k ≫ pullback.fst (D.obj i).hom (g k) = pullback.fst (D.obj i).hom (f k) ∧
        (cone D c (f k)).π.app i ≫ b k = a k ≫ (cone D c (g k)).π.app i

Module documentation

Simultaneous actual morphism descent for finitely many models

Declarations

exists_hom_stage_family