Module

PointedComposition.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.PointedComposition

5 declarations indexed from sourceView source ↗

Module documentation

Canonical pointed composition

The collapse of three actual pullbacks is independent of parenthesization. This is the comparison needed when an inverse-system transition preserves a specified geometric point by an equality of morphisms.

Imports2

Imported by3

instance

finiteEtaleOverCategoryPointedComposition

L26 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategoryPointedComposition

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

instance finiteEtaleOverCategoryPointedComposition (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X)

instance

finiteEtaleHasPullbacksAlongPointedComposition

L31 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongPointedComposition

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
local instance finiteEtaleOverCategoryPointedComposition (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X

Lean source · statement

instance finiteEtaleHasPullbacksAlongPointedComposition
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f

instance

finiteEtaleStableUnderBaseChangeAlongPointedComposition

L37 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongPointedComposition

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
local instance finiteEtaleOverCategoryPointedComposition (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongPointedComposition
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩

Lean source · statement

instance finiteEtaleStableUnderBaseChangeAlongPointedComposition
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f

theorem

pullbackComp_assoc_of_eq

L47 ↗

AlgebraicGeometry.FiniteEtale.pullbackComp_assoc_of_eq

Documentation

Associativity of canonical comparisons with a specified composite map.

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
local instance finiteEtaleOverCategoryPointedComposition (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongPointedComposition
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongPointedComposition
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {W X Y Z : Scheme.{u}}

Lean source · statement

theorem pullbackComp_assoc_of_eq
    (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z)
    (m : W ⟶ Z) (hm : m = f ≫ g ≫ h) :
    MorphismProperty.Over.pullbackComp
        (P := @IsFiniteEtale) (Q := ⊤) f (g ≫ h) m hm ≪≫
      Functor.isoWhiskerRight
        (MorphismProperty.Over.pullbackComp
          (P := @IsFiniteEtale) (Q := ⊤) g h) (pullback f) =
    MorphismProperty.Over.pullbackComp
        (P := @IsFiniteEtale) (Q := ⊤)
        (f ≫ g) h m (hm.trans (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

theorem

pullbackComp_collapse_app

L67 ↗

AlgebraicGeometry.FiniteEtale.pullbackComp_collapse_app

Documentation

Expanding the last two pullbacks and then collapsing twice equals the single canonical collapse to the specified composite.

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
local instance finiteEtaleOverCategoryPointedComposition (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongPointedComposition
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongPointedComposition
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {W X Y Z : Scheme.{u}}

Lean source · statement

theorem pullbackComp_collapse_app
    (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z)
    (m : W ⟶ Z) (hm : m = f ≫ g ≫ h) (A : FiniteEtale Z) :
    (pullback f).map
        ((MorphismProperty.Over.pullbackComp
          (P := @IsFiniteEtale) (Q := ⊤) g h).hom.app A) ≫
      (MorphismProperty.Over.pullbackComp
        (P := @IsFiniteEtale) (Q := ⊤) f g).inv.app ((pullback h).obj A) ≫
      (MorphismProperty.Over.pullbackComp
        (P := @IsFiniteEtale) (Q := ⊤)
        (f ≫ g) h m (hm.trans (Category.assoc f g h).symm)).inv.app A =
    (MorphismProperty.Over.pullbackComp
      (P := @IsFiniteEtale) (Q := ⊤) f (g ≫ h) m hm).inv.app A

Module documentation

Canonical pointed composition

Declarations

finiteEtaleOverCategoryPointedComposition

finiteEtaleHasPullbacksAlongPointedComposition

finiteEtaleStableUnderBaseChangeAlongPointedComposition

pullbackComp_assoc_of_eq

pullbackComp_collapse_app