Module

AffineLocalFactorDescent.lean

Nyll.SchemeTheory.Etale.AffineLocalFactorDescent

2 declarations indexed from sourceView source ↗

Module documentation

Descending local factorizations to an affine finite-FP model

A Zariski-local factorization of the actual integral affine limit map through a locally finitely presented morphism descends to one of its finite-FP stages. The finite affine cover and its local maps are descended using the native affine-transition limit owners. No local maps on overlaps are glued or required to agree.

The local-factorization input is the predicate already constructed by the integral-refinement theorem. Applying that theorem to a general integral source still requires its canonical affine iso connection; this file does not assert the completed finite-FP refinement theorem or a globalization.

Imports9

Nyll.SchemeTheory.Descent.AffineIntegralLimit
Nyll.SchemeTheory.Etale.IntegralRefinement
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.AffineTransitionLimit
Mathlib.AlgebraicGeometry.Restrict
Mathlib.CategoryTheory.Filtered.Basic
Mathlib.Topology.Sets.OpenCover
Mathlib.Topology.Sets.Opens
Mathlib.Tactic.Choose

Imported by3

theorem

descend_open_factor

L44 ↗

AlgebraicGeometry.AffineIntegralLimit.descend_open_factor

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite Algebra TopologicalSpace
namespace AlgebraicGeometry.AffineIntegralLimit
variable {R B : Type u} [CommRing R] [CommRing B] [Algebra R B]
  [Algebra.IsIntegral R B]

Lean source · statement

theorem descend_open_factor {U : Scheme.{u}}
    (f : U ⟶ Spec (CommRingCat.of R)) [LocallyOfFinitePresentation f]
    (i : (FinitePresentationModel R B)ᵒᵖ)
    (V : ((diagram R B).obj i).Opens) (hV : IsAffineOpen V)
    (a : (opensCone (diagram R B) (cone R B) i V).pt ⟶ U)
    (ha : a ≫ f = ((cone R B).π.app i ⁻¹ᵁ V).ι ≫
      Spec.map (CommRingCat.ofHom (algebraMap R B))) :
    ∃ (j : Over i) (b : (opensDiagram (diagram R B) i V).obj j ⟶ U),
      b ≫ f = (opensDiagramι (diagram R B) i V).app j ≫ (baseMap R B).app j.left

theorem

exists_stage_locally_factors

L85 ↗

AlgebraicGeometry.AffineIntegralLimit.exists_stage_locally_factors

Documentation

An existing local factorization of the actual integral affine limit map through an LFP morphism descends to one finite-FP model stage.