NYLL
Module

InverseLimitModels.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitModels
13 declarations indexed from sourceView source ↗

Module documentation

The actual category of finite étale models over an inverse diagram

Objects and arrows are the native finite-étale comma category. Base change along a cone defines a functor on this category, and it inverts the cartesian arrows used in the colimit construction. No descent statement is assumed in these constructions.

Imports3
Imported by4

Declarations

def

InverseLimitModel

L31 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitModel
Documentation

A finite étale scheme over one actual member of the diagram.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u v w
variable {J : Type v} [Category.{w} J]
Lean source · statement
def InverseLimitModel (F : J ⥤ Scheme.{u}) : Type (max v (u + 1))
instance

instCategory

L40 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitModel.instCategory
Documentation

The model category uses the native comma-category instance.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u v w
variable {J : Type v} [Category.{w} J]
namespace InverseLimitModel
variable (F : J ⥤ Scheme.{u})
Lean source · statement
instance instCategory : Category.{max u w} (InverseLimitModel F)
def

cartesian

L46 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitModel.cartesian
Documentation

Cartesian transition arrows in the actual comma category.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u v w
variable {J : Type v} [Category.{w} J]
namespace InverseLimitModel
variable (F : J ⥤ Scheme.{u})
Lean source · statement
def cartesian : MorphismProperty (InverseLimitModel F)
instance

cartesian_isMultiplicative

L49 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitModel.cartesian_isMultiplicative
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u v w
variable {J : Type v} [Category.{w} J]
namespace InverseLimitModel
variable (F : J ⥤ Scheme.{u})
Lean source · full declaration
instance cartesian_isMultiplicative : (cartesian F).IsMultiplicative where
  id_mem A := by
    change IsPullback (𝟙 A.left) A.hom A.hom (F.map (𝟙 A.right))
    rw [F.map_id]
    exact IsPullback.of_id_fst
  comp_mem {A B C} f g hf hg := by
    change IsPullback (f.left ≫ g.left) A.hom C.hom (F.map (f.right ≫ g.right))
    rw [F.map_comp]
    exact hf.paste_horiz hg
def

baseChangeObj

L62 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitModel.baseChangeObj
Documentation

Pull an actual finite étale model back to the vertex of a cone.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u v w
variable {J : Type v} [Category.{w} J]
namespace InverseLimitModel
variable (F : J ⥤ Scheme.{u})
variable (s : Cone F)
Lean source · statement
def baseChangeObj (A : InverseLimitModel F) : FiniteEtale s.pt
def

conePullbackMap

L69 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitModel.conePullbackMap
Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u v w
variable {J : Type v} [Category.{w} J]
namespace InverseLimitModel
variable (F : J ⥤ Scheme.{u})
variable (s : Cone F)
Lean source · statement
def conePullbackMap
    {A B X Y Z : Scheme.{u}} (f : A ⟶ Y) (g : B ⟶ Z)
    (p : X ⟶ Y) (q : X ⟶ Z) (a : A ⟶ B) (b : Y ⟶ Z)
    (ha : a ≫ g = f ≫ b) (hp : p ≫ b = q) :
    Limits.pullback f p ⟶ Limits.pullback g q
def

baseChangeHom

L88 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitModel.baseChangeHom
Documentation

The morphism on actual pullbacks induced by a model arrow.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u v w
variable {J : Type v} [Category.{w} J]
namespace InverseLimitModel
variable (F : J ⥤ Scheme.{u})
variable (s : Cone F)
Lean source · statement
def baseChangeHom {A B : InverseLimitModel F} (f : A ⟶ B) :
    baseChangeObj F s A ⟶ baseChangeObj F s B
theorem

baseChangeHom_fst

L96 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitModel.baseChangeHom_fst
Documentation

The base-change morphism retains the original arrow on the cover.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u v w
variable {J : Type v} [Category.{w} J]
namespace InverseLimitModel
variable (F : J ⥤ Scheme.{u})
variable (s : Cone F)
Lean source · statement
theorem baseChangeHom_fst {A B : InverseLimitModel F} (f : A ⟶ B) :
    (baseChangeHom F s f).left ≫ Limits.pullback.fst B.hom (s.π.app B.right) =
      Limits.pullback.fst A.hom (s.π.app A.right) ≫ f.left
theorem

baseChangeHom_snd

L102 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitModel.baseChangeHom_snd
Documentation

The base-change morphism is over the cone vertex.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u v w
variable {J : Type v} [Category.{w} J]
namespace InverseLimitModel
variable (F : J ⥤ Scheme.{u})
variable (s : Cone F)
Lean source · statement
theorem baseChangeHom_snd {A B : InverseLimitModel F} (f : A ⟶ B) :
    (baseChangeHom F s f).left ≫ Limits.pullback.snd B.hom (s.π.app B.right) =
      Limits.pullback.snd A.hom (s.π.app A.right)
def

baseChange

L108 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitModel.baseChange
Documentation

Base change along a cone is a genuine functor on the category of models.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u v w
variable {J : Type v} [Category.{w} J]
namespace InverseLimitModel
variable (F : J ⥤ Scheme.{u})
variable (s : Cone F)
Lean source · full declaration
def baseChange : InverseLimitModel F ⥤ FiniteEtale s.pt where
  obj := baseChangeObj F s
  map := baseChangeHom F s
  map_id A := by
    apply MorphismProperty.Over.Hom.ext
    apply Limits.pullback.hom_ext
    · change (baseChangeHom F s (𝟙 A)).left ≫
        Limits.pullback.fst A.hom (s.π.app A.right) =
        𝟙 _ ≫ Limits.pullback.fst A.hom (s.π.app A.right)
      rw [baseChangeHom_fst, Category.id_comp]
      exact Category.comp_id _
    · change (baseChangeHom F s (𝟙 A)).left ≫
        Limits.pullback.snd A.hom (s.π.app A.right) =
        𝟙 _ ≫ Limits.pullback.snd A.hom (s.π.app A.right)
      rw [baseChangeHom_snd, Category.id_comp]
  map_comp {A B C} f g := by
    let XA : Scheme := A.left
    let XB : Scheme := B.left
    let XC : Scheme := C.left
    let fA : XA ⟶ F.obj A.right := A.hom
    let fB : XB ⟶ F.obj B.right := B.hom
    let fC : XC ⟶ F.obj C.right := C.hom
    let PA : Scheme := Limits.pullback fA (s.π.app A.right)
    let PB : Scheme := Limits.pullback fB (s.π.app B.right)
    let PC : Scheme := Limits.pullback fC (s.π.app C.right)
    let f₀ : XA ⟶ XB := f.left
    let g₀ : XB ⟶ XC := g.left
    let u : PA ⟶ PB := (baseChangeHom F s f).left
    let v : PB ⟶ PC := (baseChangeHom F s g).left
    let uv : PA ⟶ PC := (baseChangeHom F s (f ≫ g)).left
    let pA : PA ⟶ XA := Limits.pullback.fst fA (s.π.app A.right)
    let pB : PB ⟶ XB := Limits.pullback.fst fB (s.π.app B.right)
    let pC : PC ⟶ XC := Limits.pullback.fst fC (s.π.app C.right)
    let qA : PA ⟶ s.pt := Limits.pullback.snd fA (s.π.app A.right)
    let qB : PB ⟶ s.pt := Limits.pullback.snd fB (s.π.app B.right)
    let qC : PC ⟶ s.pt := Limits.pullback.snd fC (s.π.app C.right)
    have hu : u ≫ pB = pA ≫ f₀ := baseChangeHom_fst F s f
    have hv : v ≫ pC = pB ≫ g₀ := baseChangeHom_fst F s g
    have huv : uv ≫ pC = pA ≫ (f₀ ≫ g₀) := baseChangeHom_fst F s (f ≫ g)
    have huS : u ≫ qB = qA := baseChangeHom_snd F s f
    have hvS : v ≫ qC = qB := baseChangeHom_snd F s g
    have huvS : uv ≫ qC = qA := baseChangeHom_snd F s (f ≫ g)
    apply MorphismProperty.Over.Hom.ext
    change uv = u ≫ v
    apply Limits.pullback.hom_ext
    · change uv ≫ pC = (u ≫ v) ≫ pC
      calc
        uv ≫ pC = pA ≫ (f₀ ≫ g₀) := huv
        _ = (pA ≫ f₀) ≫ g₀ := (Category.assoc pA f₀ g₀).symm
        _ = (u ≫ pB) ≫ g₀ := congrArg (fun t : PA ⟶ XB ↦ t ≫ g₀) hu.symm
        _ = u ≫ (pB ≫ g₀) := Category.assoc u pB g₀
        _ = u ≫ (v ≫ pC) := congrArg (fun t : PB ⟶ XC ↦ u ≫ t) hv.symm
        _ = (u ≫ v) ≫ pC := (Category.assoc u v pC).symm
    · change uv ≫ qC = (u ≫ v) ≫ qC
      calc
        uv ≫ qC = qA := huvS
        _ = u ≫ qB := huS.symm
        _ = u ≫ (v ≫ qC) := congrArg (fun t : PB ⟶ s.pt ↦ u ≫ t) hvS.symm
        _ = (u ≫ v) ≫ qC := (Category.assoc u v qC).symm
theorem

baseChange_inverts_cartesian

L169 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitModel.baseChange_inverts_cartesian
Documentation

Cartesian arrows become isomorphisms after base change along the cone.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u v w
variable {J : Type v} [Category.{w} J]
namespace InverseLimitModel
variable (F : J ⥤ Scheme.{u})
variable (s : Cone F)
Lean source · statement
theorem baseChange_inverts_cartesian : (cartesian F).IsInvertedBy (baseChange F s)
def

localizedBaseChange

L189 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitModel.localizedBaseChange
Documentation

The actual comparison functor out of the localization of models.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u v w
variable {J : Type v} [Category.{w} J]
namespace InverseLimitModel
variable (F : J ⥤ Scheme.{u})
variable (s : Cone F)
Lean source · statement
def localizedBaseChange : (cartesian F).Localization ⥤ FiniteEtale s.pt
theorem

q_comp_localizedBaseChange

L194 ↗
AlgebraicGeometry.FiniteEtale.InverseLimitModel.q_comp_localizedBaseChange
Documentation

Restricting the localized comparison to the model category recovers the actual base-change functor.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u v w
variable {J : Type v} [Category.{w} J]
namespace InverseLimitModel
variable (F : J ⥤ Scheme.{u})
variable (s : Cone F)
Lean source · statement
theorem q_comp_localizedBaseChange :
    (cartesian F).Q ⋙ localizedBaseChange F s = baseChange F s

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.