Module

FilteredColimitSpec.lean

Nyll.SchemeTheory.FiniteEtale.FilteredColimitSpec

1 declaration indexed from sourceView source ↗

Module documentation

Finite-etale covers of spectra of filtered ring colimits

The actual finite-etale algebra model over a stage is transferred across the existing affine equivalence. Its native base-change comparison yields recovery along the literal Spec map of the given cocone component.

Imports5

Nyll.SchemeTheory.FiniteEtale.Algebra.FilteredColimitModel
Nyll.SchemeTheory.FiniteEtale.AffineEquivalence
Mathlib.CategoryTheory.Functor.FullyFaithful
Mathlib.CategoryTheory.Limits.Opposites
Mathlib.RingTheory.Etale.Finite

Imported by2

theorem

exists_filtered_colimit_spec_model

L32 ↗

AlgebraicGeometry.FiniteEtale.exists_filtered_colimit_spec_model

Documentation

Every finite-etale cover of the spectrum of a filtered ring colimit is the native pullback of a finite-etale cover over one actual ring stage.

Source context 5 commands

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

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

Lean source · statement

theorem exists_filtered_colimit_spec_model
    {J : Type u} [Category.{u} J] [IsFiltered J]
    (F : J ⥤ CommRingCat.{u}) (c : Cocone F) (hc : IsColimit c)
    (X : FiniteEtale (Spec c.pt)) :
    ∃ (i : J) (Xᵢ : FiniteEtale (Spec (F.obj i))),
      Nonempty ((FiniteEtale.pullback (Spec.map (c.ι.app i))).obj Xᵢ ≅ X)

Module documentation

Finite-etale covers of spectra of filtered ring colimits

Declarations

exists_filtered_colimit_spec_model