Module

PullbackComposition.lean

Nyll.SchemeTheory.FiniteEtale.BaseChange.PullbackComposition

5 declarations indexed from sourceView source ↗

Module documentation

Projection formulas for canonical finite étale pullback composition

These scheme-level formulas are shared by geometric descent and pointed fundamental-group comparison. They retain the actual chosen pullbacks.

Imports2

Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Imported by12

instance

finiteEtaleOverCategoryCoherence

L25 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategoryCoherence

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 finiteEtaleOverCategoryCoherence (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X)

instance

finiteEtaleHasPullbacksAlongCoherence

L30 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongCoherence

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

Lean source · statement

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

instance

finiteEtaleStableUnderBaseChangeAlongCoherence

L36 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongCoherence

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

Lean source · statement

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

theorem

pullbackComp_inv_app_left_fst

L47 ↗

AlgebraicGeometry.FiniteEtale.pullbackComp_inv_app_left_fst

Documentation

The inverse comparison between a composite and an iterated pullback preserves the projection to the original covering scheme.

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 finiteEtaleOverCategoryCoherence (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongCoherence
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCoherence
    {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_inv_app_left_fst
    (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).inv.app A).left ≫
        Limits.pullback.fst A.hom m =
      Limits.pullback.fst (Limits.pullback.snd A.hom g) f ≫
        Limits.pullback.fst A.hom g

theorem

pullbackComp_inv_app_left_snd

L65 ↗

AlgebraicGeometry.FiniteEtale.pullbackComp_inv_app_left_snd

Documentation

The inverse comparison preserves the projection to the new base.

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 finiteEtaleOverCategoryCoherence (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongCoherence
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCoherence
    {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_inv_app_left_snd
    (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).inv.app A).left ≫
        Limits.pullback.snd A.hom m =
      Limits.pullback.snd (Limits.pullback.snd A.hom g) f

Module documentation

Projection formulas for canonical finite étale pullback composition

Declarations

finiteEtaleOverCategoryCoherence

finiteEtaleHasPullbacksAlongCoherence

finiteEtaleStableUnderBaseChangeAlongCoherence

pullbackComp_inv_app_left_fst

pullbackComp_inv_app_left_snd