NYLL
Module

InverseLimitRawCharts.lean

Nyll.SchemeTheory.FiniteEtale.InverseLimitRawCharts
2 declarations indexed from sourceView source ↗

Module documentation

Actual raw chart models of an inverse-limit cover

The finite affine chart models already constructed from the original cover are transported through their proved cartesian chart squares to the literal Over.pullback charts. This supplies exactly the recovery data consumed by the generic raw-chart and overlap constructions.

Imports3
Imported by2

Declarations

def

cartesianChartRecoveryIso

L30 ↗
AlgebraicGeometry.Scheme.Cover.cartesianChartRecoveryIso
Documentation

Recovery on a cartesian chart transfers to recovery on the literal chosen pullback chart. The comparison is constructed from the square.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
Lean source · statement
def cartesianChartRecoveryIso
    {S L U C : Scheme.{u}} (ψ : L ⟶ S) (u : U ⟶ S)
    (a : C ⟶ U) (b : C ⟶ L) (h : IsPullback a b u ψ)
    (M : Over U) (X : Over L)
    (e : (Over.pullback a).obj M ≅ (Over.pullback b).obj X) :
    (Over.pullback (pullback.fst u ψ)).obj M ≅
      (Over.pullback (pullback.snd u ψ)).obj X
theorem

exists_recovered_raw_chart_models

L57 ↗
AlgebraicGeometry.FiniteEtale.exists_recovered_raw_chart_models
Documentation

An original finite-etale cover of the actual limit has finite-etale models over a finite affine cover of a stage, with recovery on the literal native pullback charts. No local model or recovery is assumed as input.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
open AlgebraicGeometry.Scheme.Cover
Lean source · statement
theorem exists_recovered_raw_chart_models
    {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)] (X : FiniteEtale c.pt) :
    ∃ (j : I) (𝒰 : (D.obj j).OpenCover.{u}) (_ : Fintype 𝒰.I₀)
      (M : ∀ k : 𝒰.I₀, Over (𝒰.X k)),
      (∀ k : 𝒰.I₀, IsAffine (𝒰.X k)) ∧
      (∀ k : 𝒰.I₀, IsFiniteEtale (M k).hom) ∧
      Nonempty (∀ k : 𝒰.I₀,
        (Over.pullback (pullback.fst (𝒰.f k) (c.π.app j))).obj (M k) ≅
          (Over.pullback (pullback.snd (𝒰.f k) (c.π.app j))).obj
            ((FiniteEtale.forget c.pt).obj X))

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