Module

InverseLimitStageCoherence.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.InverseLimitStageCoherence

2 declarations indexed from sourceView source ↗

Module documentation

Coherence of the actual stage cocone

The cartesian stage transitions respect the canonical identity and composition isomorphisms of pullback. Applying the localization functor therefore gives the actual coherent cocone used in its 2-colimit presentation.

Imports2

Imported by2

theorem

transition_comp_app

L34 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.transition_comp_app

Documentation

The two successive cartesian transitions agree with the transition of the composite after the canonical pullback-composition comparison.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale.InverseLimitModel
universe u v w
attribute [local instance] finiteEtaleOverCategoryCoherence
  finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
variable {J : Type v} [Category.{w} J] (F : J ⥤ Scheme.{u})

Lean source · statement

theorem transition_comp_app {i j k : J} (a : i ⟶ j) (b : j ⟶ k)
    (A : FiniteEtale (F.obj k)) :
    (stageInclusion F i).map
        ((MorphismProperty.Over.pullbackComp
          (P := @IsFiniteEtale) (Q := ⊤)
          (F.map a) (F.map b) (F.map (a ≫ b)) (F.map_comp a b)).hom.app A) ≫
      (transition F a).app ((pullback (F.map b)).obj A) ≫
      (transition F b).app A = (transition F (a ≫ b)).app A

theorem

transition_id_app

L49 ↗

AlgebraicGeometry.FiniteEtale.InverseLimitModel.transition_id_app