Module

ExtensionAcrossSourceIso.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.ExtensionAcrossSourceIso

6 declarations indexed from sourceView source ↗

Module documentation

Transporting finite-etale extensions across a source isomorphism

An extension problem is unchanged when its source is replaced by an isomorphic scheme. This file records the comparison at the level of actual finite-etale objects and actual pullback isomorphisms.

Imports2

Imported by2

instance

finiteEtaleOverCategorySourceIso

L27 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategorySourceIso

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

instance finiteEtaleOverCategorySourceIso (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S)

instance

finiteEtaleHasPullbacksAlongSourceIso

L32 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongSourceIso

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategorySourceIso (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  inferInstanceAs (Category (FiniteEtale S))

Lean source · statement

instance finiteEtaleHasPullbacksAlongSourceIso
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f

instance

finiteEtaleStableUnderBaseChangeAlongSourceIso

L38 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongSourceIso

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategorySourceIso (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  inferInstanceAs (Category (FiniteEtale S))
local instance finiteEtaleHasPullbacksAlongSourceIso
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩

Lean source · statement

instance finiteEtaleStableUnderBaseChangeAlongSourceIso
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f

def

sourceIsoPulledSupportComplementOver

L53 ↗

AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.sourceIsoPulledSupportComplementOver

Documentation

The canonical identification of a pullback component with the pulled boundary complement, with the isomorphism to the whole pullback made explicit so that its structural equation is definitionally visible.

Source context 10 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategorySourceIso (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  inferInstanceAs (Category (FiniteEtale S))
local instance finiteEtaleHasPullbacksAlongSourceIso
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongSourceIso
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
namespace OpenNormalPullbackModel
variable {Y : Scheme.{u}} [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]

Lean source · statement

def sourceIsoPulledSupportComplementOver
    [IsIntegral Y] [IsNormalIntegral Y] [IsLocallyNoetherian Y]
    (I : Y.IdealSheafData) [ConnectedSpace I.supportComplement]
    [Nonempty I.supportComplement]
    (xi : Spec (.of Omega) ⟶ I.supportComplement)
    (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U) :
    M.sourceScheme ≅ (I.comap M.targetCover.hom).supportComplement

theorem

sourceIsoPulledSupportComplementOver_hom_comp_ι

L73 ↗

AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.sourceIsoPulledSupportComplementOver_hom_comp_ι

Documentation

The explicit component/complement identification is over the ambient target cover.

Source context 10 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategorySourceIso (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  inferInstanceAs (Category (FiniteEtale S))
local instance finiteEtaleHasPullbacksAlongSourceIso
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongSourceIso
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
namespace OpenNormalPullbackModel
variable {Y : Scheme.{u}} [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]

Lean source · statement

theorem sourceIsoPulledSupportComplementOver_hom_comp_ι
    [IsIntegral Y] [IsNormalIntegral Y] [IsLocallyNoetherian Y]
    (I : Y.IdealSheafData) [ConnectedSpace I.supportComplement]
    [Nonempty I.supportComplement]
    (xi : Spec (.of Omega) ⟶ I.supportComplement)
    (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ I.supportComplement.ι))
    (M : OpenNormalPullbackModel I.supportComplement.ι xi U) :
    (M.sourceIsoPulledSupportComplementOver I xi U).hom ≫
        (I.comap M.targetCover.hom).supportComplement.ι =
      M.hom

def

extensionOfSourceIso

L120 ↗

AlgebraicGeometry.FiniteEtale.extensionOfSourceIso

Documentation

If f is identified with e.hom ≫ j, an extension after transporting the source cover along e gives an extension along f itself.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategorySourceIso (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  inferInstanceAs (Category (FiniteEtale S))
local instance finiteEtaleHasPullbacksAlongSourceIso
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongSourceIso
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

def extensionOfSourceIso
    {X X' Y : Scheme.{u}}
    (e : X ≅ X') (j : X' ⟶ Y) (f : X ⟶ Y)
    (h : e.hom ≫ j = f)
    (W : FiniteEtale X)
    (extension :
      Σ Z : FiniteEtale Y,
        (pullback j).obj Z ≅
          (pullback e.inv).obj W) :
    Σ Z : FiniteEtale Y, (pullback f).obj Z ≅ W

Module documentation

Transporting finite-etale extensions across a source isomorphism

Declarations

finiteEtaleOverCategorySourceIso

finiteEtaleHasPullbacksAlongSourceIso

finiteEtaleStableUnderBaseChangeAlongSourceIso

sourceIsoPulledSupportComplementOver

sourceIsoPulledSupportComplementOver_hom_comp_ι

extensionOfSourceIso