Module

InverseLimitFractions.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitFractions

6 declarations indexed from sourceView source ↗

Module documentation

Right fractions for actual finite étale models

Directedness supplies a common stage, and the cartesian square supplies the unique lifted numerator. Thus the native model localization has genuine right-fraction representatives, independently of geometric descent.

Imports4

Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitModels
Mathlib.CategoryTheory.Localization.CalculusOfFractions
Mathlib.CategoryTheory.Category.Preorder
Mathlib.Order.Directed

Imported by2

def

refinementObj

L33 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.refinementObj

Documentation

Refine a model along an actual arrow of the indexing diagram.

Source context 6 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
section Refinement
variable {J : Type v} [Category.{w} J] (F : J ⥤ Scheme.{u})

Lean source · full declaration

def refinementObj (A : InverseLimitModel F) {j : J} (a : j ⟶ A.right) :
    InverseLimitModel F where
  left := Limits.pullback A.hom (F.map a)
  right := j
  hom := Limits.pullback.snd A.hom (F.map a)
  prop := MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u}))
    (IsPullback.of_hasPullback A.hom (F.map a)) A.prop

def

refinementHom

L43 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.refinementHom

Documentation

The canonical cartesian arrow from a refinement to its original model.

Source context 6 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
section Refinement
variable {J : Type v} [Category.{w} J] (F : J ⥤ Scheme.{u})

Lean source · full declaration

def refinementHom (A : InverseLimitModel F) {j : J} (a : j ⟶ A.right) :
    refinementObj F A a ⟶ A where
  left := Limits.pullback.fst A.hom (F.map a)
  right := a
  w := Limits.pullback.condition
  prop_hom_left := trivial
  prop_hom_right := trivial

theorem

refinementHom_cartesian

L52 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.refinementHom_cartesian

Documentation

Refinement arrows are cartesian by their defining pullback.

Source context 6 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
section Refinement
variable {J : Type v} [Category.{w} J] (F : J ⥤ Scheme.{u})

Lean source · statement

theorem refinementHom_cartesian (A : InverseLimitModel F) {j : J} (a : j ⟶ A.right) :
    cartesian F (refinementHom F A a)

theorem

hom_ext_of_comp_cartesian

L62 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.hom_ext_of_comp_cartesian

Documentation

A cartesian arrow over a preorder cancels on the right. Its two pullback projections determine a morphism, and the base arrow is unique.

Source context 5 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 v} [Preorder I] (F : Iᵒᵖ ⥤ Scheme.{u})

Lean source · statement

theorem hom_ext_of_comp_cartesian
    {A B C : InverseLimitModel F} (s : B ⟶ C) (hs : cartesian F s)
    {f g : A ⟶ B} (h : f ≫ s = g ≫ s) : f = g

theorem

exists_rightFraction

L78 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.exists_rightFraction

Documentation

The right-fraction Ore condition is supplied by a common index and an actual lift through the denominator's cartesian square.

Source context 6 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 v} [Preorder I] (F : Iᵒᵖ ⥤ Scheme.{u})
variable [IsDirectedOrder I]

Lean source · statement

theorem exists_rightFraction
    {A B : InverseLimitModel F} (φ : (cartesian F).LeftFraction A B) :
    ∃ ψ : (cartesian F).RightFraction A B, ψ.s ≫ φ.f = ψ.f ≫ φ.s

instance

cartesian_hasRightCalculusOfFractions

L118 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.cartesian_hasRightCalculusOfFractions

Documentation

The cartesian transitions in a directed diagram have a right calculus of fractions.

Source context 6 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 v} [Preorder I] (F : Iᵒᵖ ⥤ Scheme.{u})
variable [IsDirectedOrder I]

Lean source · full declaration

instance cartesian_hasRightCalculusOfFractions :
    (cartesian F).HasRightCalculusOfFractions where
  exists_rightFraction := fun {A B} φ ↦ exists_rightFraction F φ
  ext := fun {A B C} f g s hs h ↦ by
    refine ⟨_, 𝟙 _, (cartesian F).id_mem _, ?_⟩
    exact congrArg (fun q ↦ 𝟙 _ ≫ q) (hom_ext_of_comp_cartesian F s hs h)

Module documentation

Right fractions for actual finite étale models

Declarations

refinementObj

refinementHom

refinementHom_cartesian

hom_ext_of_comp_cartesian

exists_rightFraction

cartesian_hasRightCalculusOfFractions