Module

AffineTransitionModel.lean

Nyll.SchemeTheory.FiniteEtale.AffineTransitionModel

3 declarations indexed from sourceView source ↗

Module documentation

Finite-etale models for arbitrary inverse systems of affine schemes

The global-sections cocone of the actual affine limit is colimiting. Descend the cover through that ring cocone and transfer it back with isoSpec and the canonical pullback-composition isomorphisms. Recovery is along the original cone projection, without integrality or injectivity assumptions.

Imports5

Nyll.SchemeTheory.FiniteEtale.FilteredColimitSpec
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.AffineTransitionLimit
Mathlib.AlgebraicGeometry.Limits
Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Imported by2

instance

finiteEtaleHasPullbacksAlongTransition

L30 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongTransition

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

instance finiteEtaleHasPullbacksAlongTransition
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f

instance

finiteEtaleStableUnderBaseChangeAlongTransition

L36 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongTransition

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleHasPullbacksAlongTransition
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩

Lean source · statement

instance finiteEtaleStableUnderBaseChangeAlongTransition
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f

theorem

exists_affine_inverse_limit_model

L45 ↗

AlgebraicGeometry.FiniteEtale.exists_affine_inverse_limit_model

Documentation

A finite-etale cover of an actual cofiltered limit of affine schemes descends to an actual stage, with recovery along the original cone map.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleHasPullbacksAlongTransition
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongTransition
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

theorem exists_affine_inverse_limit_model
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [∀ i : I, IsAffine (D.obj i)] (X : FiniteEtale c.pt) :
    ∃ (i : I) (Xᵢ : FiniteEtale (D.obj i)),
      Nonempty ((FiniteEtale.pullback (c.π.app i)).obj Xᵢ ≅ X)

Module documentation

Finite-etale models for arbitrary inverse systems of affine schemes

Declarations

finiteEtaleHasPullbacksAlongTransition

finiteEtaleStableUnderBaseChangeAlongTransition

exists_affine_inverse_limit_model