NYLL
Module

RadicialDescentIso.lean

Nyll.SchemeTheory.FiniteEtale.RadicialDescentIso
13 declarations indexed from sourceView source ↗

Module documentation

Canonical comparison for finite étale covers along a radicial morphism

The diagonal of a separated universally injective morphism is a surjective closed immersion. Its fully faithful pullback therefore lifts the canonical comparison between the two iterated pullbacks to a unique natural isomorphism. The comparison is normalized by the common pullback along the identity.

Imports5
Imported by2

Declarations

abbrev

finiteEtaleProperty

L35 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleProperty
Documentation

The morphism property of being both finite and etale.

Source context 4 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale

/- The intersection is used throughout the comparison. Giving it a name avoids
relying on notation expansion inside qualified names such as `P.Over`. -/
Lean source · statement
abbrev finiteEtaleProperty : MorphismProperty Scheme.{u}
instance

finiteEtalePropertyStableUnderBaseChange

L38 ↗
AlgebraicGeometry.FiniteEtale.finiteEtalePropertyStableUnderBaseChange
Source context 4 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale

/- The intersection is used throughout the comparison. Giving it a name avoids
relying on notation expansion inside qualified names such as `P.Over`. -/
Lean source · statement
instance finiteEtalePropertyStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange (finiteEtaleProperty : MorphismProperty Scheme.{u})
def

radicialDiagonalFstIso

L46 ↗
AlgebraicGeometry.FiniteEtale.radicialDiagonalFstIso
Documentation

Pullback along the first projection followed by the diagonal is canonically pullback along the identity.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale

/- The intersection is used throughout the comparison. Giving it a name avoids
relying on notation expansion inside qualified names such as `P.Over`. -/
local instance finiteEtalePropertyStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange (finiteEtaleProperty : MorphismProperty Scheme.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y : Scheme.{u}}
Lean source · statement
def radicialDiagonalFstIso (f : X ⟶ Y) :
    MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (𝟙 X) ≅
      MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (Limits.pullback.fst f f) ⋙
        MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (Limits.pullback.diagonal f)
def

radicialDiagonalSndIso

L56 ↗
AlgebraicGeometry.FiniteEtale.radicialDiagonalSndIso
Documentation

Pullback along the second projection followed by the diagonal is canonically pullback along the identity.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale

/- The intersection is used throughout the comparison. Giving it a name avoids
relying on notation expansion inside qualified names such as `P.Over`. -/
local instance finiteEtalePropertyStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange (finiteEtaleProperty : MorphismProperty Scheme.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y : Scheme.{u}}
Lean source · statement
def radicialDiagonalSndIso (f : X ⟶ Y) :
    MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (𝟙 X) ≅
      MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (Limits.pullback.snd f f) ⋙
        MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (Limits.pullback.diagonal f)
def

radicialDescentIso

L66 ↗
AlgebraicGeometry.FiniteEtale.radicialDescentIso
Documentation

The two pullbacks of a finite étale cover along a separated universally injective morphism are canonically isomorphic, naturally in the cover.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale

/- The intersection is used throughout the comparison. Giving it a name avoids
relying on notation expansion inside qualified names such as `P.Over`. -/
local instance finiteEtalePropertyStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange (finiteEtaleProperty : MorphismProperty Scheme.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y : Scheme.{u}}
Lean source · statement
def radicialDescentIso (f : X ⟶ Y) [IsSeparated f] [UniversallyInjective f] :
    MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (Limits.pullback.fst f f) ≅
      MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (Limits.pullback.snd f f)
theorem

radicialDescentIso_map_hom_app

L80 ↗
AlgebraicGeometry.FiniteEtale.radicialDescentIso_map_hom_app
Documentation

Pulling the canonical comparison back to the diagonal gives precisely the comparison through the common identity pullback.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale

/- The intersection is used throughout the comparison. Giving it a name avoids
relying on notation expansion inside qualified names such as `P.Over`. -/
local instance finiteEtalePropertyStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange (finiteEtaleProperty : MorphismProperty Scheme.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y : Scheme.{u}}
Lean source · statement
theorem radicialDescentIso_map_hom_app
    (f : X ⟶ Y) [IsSeparated f] [UniversallyInjective f] (V : finiteEtaleProperty.Over ⊤ X) :
    (MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (Limits.pullback.diagonal f)).map
        ((radicialDescentIso f).hom.app V) =
      (radicialDiagonalFstIso f).inv.app V ≫ (radicialDiagonalSndIso f).hom.app V
theorem

radicialDescentIso_mapIso

L93 ↗
AlgebraicGeometry.FiniteEtale.radicialDescentIso_mapIso
Documentation

The isomorphism form of the diagonal comparison formula.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale

/- The intersection is used throughout the comparison. Giving it a name avoids
relying on notation expansion inside qualified names such as `P.Over`. -/
local instance finiteEtalePropertyStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange (finiteEtaleProperty : MorphismProperty Scheme.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y : Scheme.{u}}
Lean source · statement
theorem radicialDescentIso_mapIso
    (f : X ⟶ Y) [IsSeparated f] [UniversallyInjective f] (V : finiteEtaleProperty.Over ⊤ X) :
    (MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (Limits.pullback.diagonal f)).mapIso
        ((radicialDescentIso f).app V) =
      ((radicialDiagonalFstIso f).app V).symm ≪≫ (radicialDiagonalSndIso f).app V
theorem

radicialDescentIso_diagonal

L104 ↗
AlgebraicGeometry.FiniteEtale.radicialDescentIso_diagonal
Documentation

With the canonical identifications on both sides, the diagonal restriction of the comparison is the identity.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale

/- The intersection is used throughout the comparison. Giving it a name avoids
relying on notation expansion inside qualified names such as `P.Over`. -/
local instance finiteEtalePropertyStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange (finiteEtaleProperty : MorphismProperty Scheme.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y : Scheme.{u}}
Lean source · statement
theorem radicialDescentIso_diagonal
    (f : X ⟶ Y) [IsSeparated f] [UniversallyInjective f] (V : finiteEtaleProperty.Over ⊤ X) :
    (radicialDiagonalFstIso f).hom.app V ≫
        (MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (Limits.pullback.diagonal f)).map
          ((radicialDescentIso f).hom.app V) ≫
        (radicialDiagonalSndIso f).inv.app V =
      𝟙 ((MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (𝟙 X)).obj V)
theorem

radicialDescentIso_hom_app_unique

L116 ↗
AlgebraicGeometry.FiniteEtale.radicialDescentIso_hom_app_unique
Documentation

Diagonal normalization characterizes the comparison on every finite étale cover; no choice of a preimage changes it.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale

/- The intersection is used throughout the comparison. Giving it a name avoids
relying on notation expansion inside qualified names such as `P.Over`. -/
local instance finiteEtalePropertyStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange (finiteEtaleProperty : MorphismProperty Scheme.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y : Scheme.{u}}
Lean source · statement
theorem radicialDescentIso_hom_app_unique
    (f : X ⟶ Y) [IsSeparated f] [UniversallyInjective f] (V : finiteEtaleProperty.Over ⊤ X)
    (a : (MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (Limits.pullback.fst f f)).obj V ⟶
      (MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (Limits.pullback.snd f f)).obj V)
    (ha : (radicialDiagonalFstIso f).hom.app V ≫
        (MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (Limits.pullback.diagonal f)).map a ≫
        (radicialDiagonalSndIso f).inv.app V =
      𝟙 ((MorphismProperty.Over.pullback finiteEtaleProperty ⊤ (𝟙 X)).obj V)) :
    a = (radicialDescentIso f).hom.app V
def

radicialDiagonalFstSection

L135 ↗
AlgebraicGeometry.FiniteEtale.radicialDiagonalFstSection
Documentation

The diagonal section of the first pullback.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale

/- The intersection is used throughout the comparison. Giving it a name avoids
relying on notation expansion inside qualified names such as `P.Over`. -/
local instance finiteEtalePropertyStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange (finiteEtaleProperty : MorphismProperty Scheme.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y : Scheme.{u}}
Lean source · statement
def radicialDiagonalFstSection (f : X ⟶ Y) (V : finiteEtaleProperty.Over ⊤ X) :
    V.left ⟶ Limits.pullback V.hom (Limits.pullback.fst f f)
def

radicialDiagonalSndSection

L142 ↗
AlgebraicGeometry.FiniteEtale.radicialDiagonalSndSection
Documentation

The diagonal section of the second pullback.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale

/- The intersection is used throughout the comparison. Giving it a name avoids
relying on notation expansion inside qualified names such as `P.Over`. -/
local instance finiteEtalePropertyStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange (finiteEtaleProperty : MorphismProperty Scheme.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y : Scheme.{u}}
Lean source · statement
def radicialDiagonalSndSection (f : X ⟶ Y) (V : finiteEtaleProperty.Over ⊤ X) :
    V.left ⟶ Limits.pullback V.hom (Limits.pullback.snd f f)
theorem

pullbackComp_identitySection

L148 ↗
AlgebraicGeometry.FiniteEtale.pullbackComp_identitySection
Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale

/- The intersection is used throughout the comparison. Giving it a name avoids
relying on notation expansion inside qualified names such as `P.Over`. -/
local instance finiteEtalePropertyStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange (finiteEtaleProperty : MorphismProperty Scheme.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y : Scheme.{u}}
Lean source · full declaration
theorem pullbackComp_identitySection
    {A B : Scheme.{u}} (j : A ⟶ B) (q : B ⟶ A) (hj : j ≫ q = 𝟙 A)
    (V : finiteEtaleProperty.Over ⊤ A) :
    Limits.pullback.lift (𝟙 V.left) V.hom (by simp) ≫
        ((MorphismProperty.Over.pullbackComp
          (P := finiteEtaleProperty) (Q := ⊤) j q (𝟙 A) hj.symm).hom.app V).left ≫
        Limits.pullback.fst (Limits.pullback.snd V.hom q) j =
      Limits.pullback.lift (𝟙 V.left) (V.hom ≫ j)
        (by simp [Category.assoc, hj]) := by
  change Limits.pullback.lift (𝟙 V.left) V.hom _ ≫
      ((Limits.pullback.congrHom (f₁ := V.hom) rfl hj.symm).hom ≫
        (pullbackLeftPullbackSndIso V.hom q j).inv) ≫
          Limits.pullback.fst (Limits.pullback.snd V.hom q) j = _
  apply Limits.pullback.hom_ext
  · simp only [Category.assoc, pullbackLeftPullbackSndIso_inv_fst,
      Limits.pullback.congrHom_hom,
      Category.comp_id, Limits.pullback.lift_fst]
  · simp only [Category.assoc, pullbackLeftPullbackSndIso_inv_fst_snd,
      Limits.pullback.congrHom_hom,
      Category.id_comp, Limits.pullback.lift_snd_assoc, Limits.pullback.lift_snd]
theorem

radicialDescentIso_diagonal_section

L171 ↗
AlgebraicGeometry.FiniteEtale.radicialDescentIso_diagonal_section
Documentation

On the actual diagonal sections, the canonical comparison is the identity on the original finite étale cover.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u
namespace AlgebraicGeometry.FiniteEtale

/- The intersection is used throughout the comparison. Giving it a name avoids
relying on notation expansion inside qualified names such as `P.Over`. -/
local instance finiteEtalePropertyStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange (finiteEtaleProperty : MorphismProperty Scheme.{u}) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {X Y : Scheme.{u}}
Lean source · statement
theorem radicialDescentIso_diagonal_section
    (f : X ⟶ Y) [IsSeparated f] [UniversallyInjective f] (V : finiteEtaleProperty.Over ⊤ X) :
    radicialDiagonalFstSection f V ≫ ((radicialDescentIso f).hom.app V).left =
      radicialDiagonalSndSection f V

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.