NYLL
Module

AffineTransitionOverHomFamily.lean

Nyll.SchemeTheory.Descent.AffineTransitionOverHomFamily
2 declarations indexed from sourceView source ↗

Module documentation

Actual native over-category morphism families at a common stage

The real qcqs/LFP scheme Hom supplier is transported through pullback symmetry. Recovery uses the native cone comparison, with both projection equations proved from the chosen pullbacks. This applies to raw gluing overlaps over the ambient base without claiming that those overlaps are finite there.

Imports2
Imported by2

Declarations

theorem

overTransition_eq_symmetry

L27 ↗
AlgebraicGeometry.AffineTransitionHom.overTransition_eq_symmetry
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 overTransition_eq_symmetry
    {I : Type u} [Category.{u} I] {S : Scheme.{u}}
    (D : I ⥤ Over S) (c : Cone D) (A : Over S) (i : I) :
    overInverseLimitTransition D c A i =
      (pullbackSymmetry c.pt.hom A.hom).inv ≫ (cone D c A.hom).π.app i ≫
        (pullbackSymmetry (D.obj i).hom A.hom).hom
theorem

exists_over_hom_stage_family

L42 ↗
AlgebraicGeometry.AffineTransitionHom.exists_over_hom_stage_family
Documentation

Finitely many native Over morphisms descend to one coefficient stage, retaining the exact native pullback-comparison recovery equations.

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_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] (A B : K → Over S)
    [∀ k : K, QuasiCompact (A k).hom] [∀ k : K, QuasiSeparated (A k).hom]
    [∀ k : K, LocallyOfFinitePresentation (B k).hom]
    (a : ∀ k : K, (Over.pullback c.pt.hom).obj (A k) ⟶
      (Over.pullback c.pt.hom).obj (B k)) :
    ∃ (i : I) (b : ∀ k : K, (Over.pullback (D.obj i).hom).obj (A k) ⟶
      (Over.pullback (D.obj i).hom).obj (B k)), ∀ k : K,
        (overInverseLimitPullbackComparison D c i).hom.app (A k) ≫
            (Over.pullback (c.π.app i).left).map (b k) =
          a k ≫ (overInverseLimitPullbackComparison D c i).hom.app (B k)

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