Module

InverseLimitFullness.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitFullness

5 declarations indexed from sourceView source ↗

Module documentation

Fullness of the finite étale model localization

Actual finite-étale Hom descent produces a right fraction representing each morphism over the limiting scheme. Fullness is a conclusion of that geometric theorem, with the original qcqs and affine-transition inputs.

Imports3

Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitStages
Nyll.SchemeTheory.FiniteEtale.InverseLimitHom
Mathlib.CategoryTheory.Filtered.Basic

Imported by2

theorem

iso_square_inv

L27 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.iso_square_inv

Source context 4 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 w

Lean source · statement

theorem iso_square_inv
    {C : Type v} [Category.{w} C] {X X' Y Y' : C}
    (eX : X ≅ X') (eY : Y ≅ Y') (a : X ⟶ Y) (b : X' ⟶ Y')
    (h : eX.hom ≫ b = a ≫ eY.hom) : eX.inv ≫ a = b ≫ eY.inv

theorem

cancel_fraction_target

L40 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.cancel_fraction_target

Source context 4 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 w

Lean source · statement

theorem cancel_fraction_target
    {C : Type v} [Category.{w} C] {P Q R S T : C}
    (d : P ⟶ Q) (a : Q ⟶ R) (e : S ≅ R) (r : T ⟶ P) (n : T ⟶ S)
    (h : r ≫ (d ≫ a ≫ e.inv) = n) : (r ≫ d) ≫ a = n ≫ e.hom

theorem

exists_stage_fraction

L58 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.exists_stage_fraction

Documentation

For two covers at the same stage, actual Hom descent supplies a right fraction whose evaluation is the prescribed morphism at the limit.

Source context 10 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 w
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 exists_stage_fraction
    (i : Iᵒᵖ) (A B : FiniteEtale (F.obj i))
    (a : (pullback (s.π.app i)).obj A ⟶ (pullback (s.π.app i)).obj B) :
    ∃ φ : (cartesian F).RightFraction
        ((stageInclusion F i).obj A) ((stageInclusion F i).obj B),
      (baseChange F s).map φ.s ≫ a = (baseChange F s).map φ.f

theorem

exists_fraction

L87 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.exists_fraction

Documentation

Common refinement reduces arbitrary model sources and targets to one stage, where the actual finite-étale Hom-descent theorem applies.

Source context 10 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 w
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 exists_fraction
    (A B : InverseLimitModel F)
    (a : (baseChange F s).obj A ⟶ (baseChange F s).obj B) :
    ∃ φ : (cartesian F).RightFraction A B,
      (baseChange F s).map φ.s ≫ a = (baseChange F s).map φ.f

theorem

localizedBaseChange_full

L121 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.localizedBaseChange_full

Documentation

The actual comparison out of the localization of finite-étale models is full. This is derived from native scheme Hom descent, not assumed.

Source context 10 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 w
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 localizedBaseChange_full : (localizedBaseChange F s).Full

Module documentation

Fullness of the finite étale model localization

Declarations

iso_square_inv

cancel_fraction_target

exists_stage_fraction

exists_fraction

localizedBaseChange_full