Module

InverseLimitFaithfulness.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitFaithfulness

2 declarations indexed from sourceView source ↗

Module documentation

Faithfulness of the finite etale model localization

Geometric equality descent for the original inverse limit supplies eventual equality at an actual stage. The categorical fraction argument then makes the comparison from the cartesian model localization faithful.

Imports3

Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitEventualFaithfulness
Nyll.SchemeTheory.FiniteEtale.InverseLimitEquality
Mathlib.CategoryTheory.Filtered.Basic

Imported by2

theorem

exists_refinement_map_eq

L36 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.exists_refinement_map_eq

Documentation

Two actual model arrows which agree at the limit agree after a cartesian refinement of their original source.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
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)]
include hs

Lean source · statement

theorem exists_refinement_map_eq
    {A B : InverseLimitModel F} (f g : A ⟶ B)
    (hfg : (baseChange F s).map f = (baseChange F s).map g) :
    ∃ (j : Iᵒᵖ) (h : j ⟶ A.right),
      refinementHom F A h ≫ f = refinementHom F A h ≫ g

theorem

localizedBaseChange_faithful

L46 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.localizedBaseChange_faithful