Module

InverseLimitEventualFaithfulness.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitEventualFaithfulness

2 declarations indexed from sourceView source ↗

Module documentation

Eventual equality and the faithful comparison of finite etale models

For a directed system of schemes with any cone, equality of arrows after restriction to the cone vertex implies equality in the cartesian model localization whenever it is detected at a later stage. The proof factors arbitrary model arrows through an actual common stage and uses the right calculus of fractions. No limiting property of the cone is required.

This separates the categorical argument from the geometric equality supplier, allowing both scheme inverse limits and germs along a subscheme to use the same concrete model localization.

Imports3

Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitStages
Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Mathlib.CategoryTheory.Filtered.Basic

Imported by3

theorem

exists_refinement_map_eq_of_stage_equality

L44 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.exists_refinement_map_eq_of_stage_equality

Documentation

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

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.InverseLimitModel
universe u v
variable {I : Type v} [Preorder I]
variable (F : Iᵒᵖ ⥤ Scheme.{u}) (s : Cone F)
variable (heq : ∀ (i : Iᵒᵖ) {A B : FiniteEtale (F.obj i)} (a b : A ⟶ B),
  (pullback (s.π.app i)).map a = (pullback (s.π.app i)).map b →
    ∃ (j : Iᵒᵖ) (h : j ⟶ i),
      (pullback (F.map h)).map a = (pullback (F.map h)).map b)
include heq

Lean source · statement

theorem exists_refinement_map_eq_of_stage_equality
    {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_of_stage_equality

L107 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.localizedBaseChange_faithful_of_stage_equality