Module

PullbackCoherence.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.PullbackCoherence

3 declarations indexed from sourceView source ↗

Module documentation

Coherence of the canonical finite étale pullback comparisons

The comparison isomorphisms are determined by the projections of the actual pullbacks. Their associativity supplies strict composition of pointed fundamental-group maps, rather than composition only up to conjugation.

Imports2

Imported by2

theorem

pullback_map_fst

L31 ↗

AlgebraicGeometry.FiniteEtale.pullback_map_fst

Source context 6 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
variable {W X Y Z : Scheme.{u}}

Lean source · statement

theorem pullback_map_fst
    (f : X ⟶ Y) {A B : FiniteEtale Y} (q : A ⟶ B) :
    ((pullback f).map q).left ≫ Limits.pullback.fst B.hom f =
      Limits.pullback.fst A.hom f ≫ q.left

theorem

pullback_map_snd

L37 ↗

AlgebraicGeometry.FiniteEtale.pullback_map_snd

Source context 6 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
variable {W X Y Z : Scheme.{u}}

Lean source · statement

theorem pullback_map_snd
    (f : X ⟶ Y) {A B : FiniteEtale Y} (q : A ⟶ B) :
    ((pullback f).map q).left ≫ Limits.pullback.snd B.hom f =
      Limits.pullback.snd A.hom f

theorem

pullbackComp_assoc

L46 ↗

AlgebraicGeometry.FiniteEtale.pullbackComp_assoc

Documentation

The two canonical comparisons from a triple composite to its iterated pullback agree. The equation is proved on scheme morphisms by the two pullback projections.

Source context 6 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
variable {W X Y Z : Scheme.{u}}

Lean source · statement

theorem pullbackComp_assoc
    (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) :
    MorphismProperty.Over.pullbackComp
        (P := @IsFiniteEtale) (Q := ⊤) f (g ≫ h) ≪≫
      Functor.isoWhiskerRight
        (MorphismProperty.Over.pullbackComp
          (P := @IsFiniteEtale) (Q := ⊤) g h) (pullback f) =
    MorphismProperty.Over.pullbackComp
        (P := @IsFiniteEtale) (Q := ⊤)
        (f ≫ g) h (f ≫ g ≫ h) (Category.assoc f g h).symm ≪≫
      Functor.isoWhiskerLeft (pullback h)
        (MorphismProperty.Over.pullbackComp
          (P := @IsFiniteEtale) (Q := ⊤) f g) ≪≫
      (Functor.associator (pullback h) (pullback g) (pullback f)).symm

Module documentation

Coherence of the canonical finite étale pullback comparisons

Declarations

pullback_map_fst

pullback_map_snd

pullbackComp_assoc