Module

InverseLimitEquivalence.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitEquivalence

3 declarations indexed from sourceView source ↗

Module documentation

Finite étale categories commute with inverse limits

The concrete colimit category is the localization of actual finite-étale models at their cartesian arrows. Its stage inclusions, canonical pullback-transition isomorphisms, unit/composition equations, and functor-category universal property are constructed in the stage modules.

Here the actual object-gluing theorem supplies essential surjectivity. Together with the proved Hom and equality descent, this makes the original base-change functor a localization and gives an actual equivalence with finite étale covers of the limiting scheme.

Imports4

Imported by1

Nyll.EtaleFundamentalGroups.FiniteEtale.All

theorem

baseChange_isLocalization

L44 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.baseChange_isLocalization

Documentation

The actual base-change functor realizes finite-étale covers of the limit as the localization of actual models at cartesian transitions.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale.InverseLimitModel
universe u
variable {I : Type u} [Preorder I] [IsDirectedOrder I] [Nonempty I]
variable (F : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone F) (hs : IsLimit s)
variable [∀ {i j : Iᵒᵖ} (h : i ⟶ j), IsAffineHom (F.map h)]
variable [∀ i : Iᵒᵖ, CompactSpace (F.obj i)]
variable [∀ i : Iᵒᵖ, QuasiSeparatedSpace (F.obj i)]
include hs

Lean source · statement

theorem baseChange_isLocalization :
    (baseChange F s).IsLocalization (cartesian F)

def