Module

PullbackIdentity.lean

Nyll.SchemeTheory.FiniteEtale.BaseChange.PullbackIdentity

5 declarations indexed from sourceView source ↗

Module documentation

Identity coherence for the actual finite étale pullback

The identity comparison uses the first projection of the chosen pullback. Its compatibility with a cone leg is proved by those actual projections.

Imports2

Nyll.SchemeTheory.FiniteEtale.BaseChange.PullbackComposition
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Imported by5

def

pullbackIdSchemeIso

L28 ↗

AlgebraicGeometry.FiniteEtale.pullbackIdSchemeIso

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
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence

Lean source · full declaration

def pullbackIdSchemeIso {A X : Scheme.{u}} (f : A ⟶ X) :
    Limits.pullback f (𝟙 X) ≅ A where
  hom := Limits.pullback.fst f (𝟙 X)
  inv := Limits.pullback.lift (𝟙 A) f
    ((Category.id_comp f).trans (Category.comp_id f).symm)
  hom_inv_id := by
    apply Limits.pullback.hom_ext
    · rw [Category.assoc, Limits.pullback.lift_fst,
        Category.comp_id, Category.id_comp]
    · rw [Category.assoc, Limits.pullback.lift_snd,
        Limits.pullback.condition, Category.comp_id, Category.id_comp]
  inv_hom_id := Limits.pullback.lift_fst _ _ _

def

pullbackIdIso

L43 ↗

AlgebraicGeometry.FiniteEtale.pullbackIdIso

Documentation

The canonical comparison between pullback by the identity and the identity functor on finite étale covers.

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
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence

Lean source · statement

def pullbackIdIso (X : Scheme.{u}) : pullback (𝟙 X) ≅ 𝟭 (FiniteEtale X)

theorem

pullbackIdIso_hom_app_left

L53 ↗

AlgebraicGeometry.FiniteEtale.pullbackIdIso_hom_app_left

Documentation

The identity comparison is the actual first pullback projection.

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
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence

Lean source · statement

theorem pullbackIdIso_hom_app_left (X : Scheme.{u}) (A : FiniteEtale X) :
    ((pullbackIdIso X).hom.app A).left = Limits.pullback.fst A.hom (𝟙 X)

theorem

pullbackComp_hom_app_left_fst_fst

L59 ↗

AlgebraicGeometry.FiniteEtale.pullbackComp_hom_app_left_fst_fst

Documentation

The forward composition comparison preserves the projection to the original cover, with a specified composite morphism.

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
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence

Lean source · statement

theorem pullbackComp_hom_app_left_fst_fst
    {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    (m : X ⟶ Z) (hm : m = f ≫ g) (A : FiniteEtale Z) :
    ((MorphismProperty.Over.pullbackComp
      (P := @IsFiniteEtale) (Q := ⊤) f g m hm).hom.app A).left ≫
      Limits.pullback.fst (Limits.pullback.snd A.hom g) f ≫
      Limits.pullback.fst A.hom g = Limits.pullback.fst A.hom m

theorem

pullbackComp_id_coherence

L71 ↗

AlgebraicGeometry.FiniteEtale.pullbackComp_id_coherence

Documentation

Composing the canonical cone comparison with the identity comparison does not change pullback along that cone leg.

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
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence

Lean source · statement

theorem pullbackComp_id_coherence {X Y : Scheme.{u}} (p : X ⟶ Y) :
    MorphismProperty.Over.pullbackComp
        (P := @IsFiniteEtale) (Q := ⊤) p (𝟙 Y) p (Category.comp_id p).symm ≪≫
      Functor.isoWhiskerRight (pullbackIdIso Y) (pullback p) ≪≫
      Functor.leftUnitor (pullback p) = Iso.refl (pullback p)

Module documentation

Identity coherence for the actual finite étale pullback

Declarations

pullbackIdSchemeIso

pullbackIdIso

pullbackIdIso_hom_app_left

pullbackComp_hom_app_left_fst_fst

pullbackComp_id_coherence