Module

AffineThickening.lean

Nyll.SchemeTheory.FiniteEtale.AffineThickening

8 declarations indexed from sourceView source ↗

Module documentation

Finite étale covers of affine thickenings

A nil ideal defines a Henselian pair. Thus finite étale covers are unchanged by its quotient. Factoring a surjective ring map through its kernel quotient, and an affine closed immersion through a quotient spectrum, gives the same result for every surjective closed immersion with affine target.

Imports9

Nyll.SchemeTheory.FiniteEtale.AffineEquivalence
Nyll.SchemeTheory.FiniteEtale.Algebra.HenselianBaseChange
Nyll.SchemeTheory.RingTheory.HenselianNilIdeal
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.CategoryTheory.Adjunction.Unique
Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Spectrum.Prime.Topology

Imported by4

instance

finiteEtaleInfStableUnderBaseChangeAffineThickening

L36 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleInfStableUnderBaseChangeAffineThickening

Source context 4 commands

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

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

Lean source · statement

instance finiteEtaleInfStableUnderBaseChangeAffineThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale)

instance

finiteEtaleInfContainsIdentitiesAffineThickening

L41 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleInfContainsIdentitiesAffineThickening

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeAffineThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf

Lean source · full declaration

instance finiteEtaleInfContainsIdentitiesAffineThickening :
    MorphismProperty.ContainsIdentities
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) where
  id_mem X := by
    have h : IsFiniteEtale (𝟙 X) :=
      (inferInstance : MorphismProperty.ContainsIdentities
        (@IsFiniteEtale : MorphismProperty Scheme.{u})).id_mem X
    exact ⟨h.toIsFinite, h.toEtale⟩

instance

finiteEtaleInfStableUnderCompositionAffineThickening

L50 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleInfStableUnderCompositionAffineThickening

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeAffineThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
local instance finiteEtaleInfContainsIdentitiesAffineThickening :
    MorphismProperty.ContainsIdentities
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) where
  id_mem X := by
    have h : IsFiniteEtale (𝟙 X) :=
      (inferInstance : MorphismProperty.ContainsIdentities
        (@IsFiniteEtale : MorphismProperty Scheme.{u})).id_mem X
    exact ⟨h.toIsFinite, h.toEtale⟩

Lean source · full declaration

instance finiteEtaleInfStableUnderCompositionAffineThickening :
    MorphismProperty.IsStableUnderComposition
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) where
  comp_mem f g hf hg := by
    have hf' : IsFiniteEtale f := @IsFiniteEtale.mk _ _ _ hf.1 hf.2
    have hg' : IsFiniteEtale g := @IsFiniteEtale.mk _ _ _ hg.1 hg.2
    have hfg : IsFiniteEtale (f ≫ g) :=
      (inferInstance : MorphismProperty.IsStableUnderComposition
        (@IsFiniteEtale : MorphismProperty Scheme.{u})).comp_mem f g hf' hg'
    exact ⟨hfg.toIsFinite, hfg.toEtale⟩

theorem

pullback_isEquivalence_of_isIso

L62 ↗

AlgebraicGeometry.FiniteEtale.pullback_isEquivalence_of_isIso

Documentation

Pullback by a scheme isomorphism is an equivalence on finite étale covers.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeAffineThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
local instance finiteEtaleInfContainsIdentitiesAffineThickening :
    MorphismProperty.ContainsIdentities
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) where
  id_mem X := by
    have h : IsFiniteEtale (𝟙 X) :=
      (inferInstance : MorphismProperty.ContainsIdentities
        (@IsFiniteEtale : MorphismProperty Scheme.{u})).id_mem X
    exact ⟨h.toIsFinite, h.toEtale⟩
local instance finiteEtaleInfStableUnderCompositionAffineThickening :
    MorphismProperty.IsStableUnderComposition
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) where
  comp_mem f g hf hg := by
    have hf' : IsFiniteEtale f := @IsFiniteEtale.mk _ _ _ hf.1 hf.2
    have hg' : IsFiniteEtale g := @IsFiniteEtale.mk _ _ _ hg.1 hg.2
    have hfg : IsFiniteEtale (f ≫ g) :=
      (inferInstance : MorphismProperty.IsStableUnderComposition
        (@IsFiniteEtale : MorphismProperty Scheme.{u})).comp_mem f g hf' hg'
    exact ⟨hfg.toIsFinite, hfg.toEtale⟩

Lean source · statement

theorem pullback_isEquivalence_of_isIso
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIso f] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ f).IsEquivalence

theorem

pullback_comp_isEquivalence

L76 ↗

AlgebraicGeometry.FiniteEtale.pullback_comp_isEquivalence

Documentation

A composite preserves the finite étale category when each of its two maps does.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeAffineThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
local instance finiteEtaleInfContainsIdentitiesAffineThickening :
    MorphismProperty.ContainsIdentities
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) where
  id_mem X := by
    have h : IsFiniteEtale (𝟙 X) :=
      (inferInstance : MorphismProperty.ContainsIdentities
        (@IsFiniteEtale : MorphismProperty Scheme.{u})).id_mem X
    exact ⟨h.toIsFinite, h.toEtale⟩
local instance finiteEtaleInfStableUnderCompositionAffineThickening :
    MorphismProperty.IsStableUnderComposition
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) where
  comp_mem f g hf hg := by
    have hf' : IsFiniteEtale f := @IsFiniteEtale.mk _ _ _ hf.1 hf.2
    have hg' : IsFiniteEtale g := @IsFiniteEtale.mk _ _ _ hg.1 hg.2
    have hfg : IsFiniteEtale (f ≫ g) :=
      (inferInstance : MorphismProperty.IsStableUnderComposition
        (@IsFiniteEtale : MorphismProperty Scheme.{u})).comp_mem f g hf' hg'
    exact ⟨hfg.toIsFinite, hfg.toEtale⟩

Lean source · statement

theorem pullback_comp_isEquivalence
    {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    [(MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ f).IsEquivalence]
    [(MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ g).IsEquivalence] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ (f ≫ g)).IsEquivalence

theorem

pullback_quotient_isEquivalence_of_le_nilradical

L89 ↗

AlgebraicGeometry.FiniteEtale.pullback_quotient_isEquivalence_of_le_nilradical

Documentation

Reduction by an arbitrary nil ideal leaves finite étale covers unchanged.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeAffineThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
local instance finiteEtaleInfContainsIdentitiesAffineThickening :
    MorphismProperty.ContainsIdentities
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) where
  id_mem X := by
    have h : IsFiniteEtale (𝟙 X) :=
      (inferInstance : MorphismProperty.ContainsIdentities
        (@IsFiniteEtale : MorphismProperty Scheme.{u})).id_mem X
    exact ⟨h.toIsFinite, h.toEtale⟩
local instance finiteEtaleInfStableUnderCompositionAffineThickening :
    MorphismProperty.IsStableUnderComposition
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) where
  comp_mem f g hf hg := by
    have hf' : IsFiniteEtale f := @IsFiniteEtale.mk _ _ _ hf.1 hf.2
    have hg' : IsFiniteEtale g := @IsFiniteEtale.mk _ _ _ hg.1 hg.2
    have hfg : IsFiniteEtale (f ≫ g) :=
      (inferInstance : MorphismProperty.IsStableUnderComposition
        (@IsFiniteEtale : MorphismProperty Scheme.{u})).comp_mem f g hf' hg'
    exact ⟨hfg.toIsFinite, hfg.toEtale⟩

Lean source · statement

theorem pullback_quotient_isEquivalence_of_le_nilradical
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I ≤ nilradical R) :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))).IsEquivalence

theorem

pullback_specMap_isEquivalence_of_surjective_of_ker_le_nilradical

L100 ↗

AlgebraicGeometry.FiniteEtale.pullback_specMap_isEquivalence_of_surjective_of_ker_le_nilradical

Documentation

A surjective ring map with nil kernel induces an equivalence on finite étale covers of spectra.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeAffineThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
local instance finiteEtaleInfContainsIdentitiesAffineThickening :
    MorphismProperty.ContainsIdentities
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) where
  id_mem X := by
    have h : IsFiniteEtale (𝟙 X) :=
      (inferInstance : MorphismProperty.ContainsIdentities
        (@IsFiniteEtale : MorphismProperty Scheme.{u})).id_mem X
    exact ⟨h.toIsFinite, h.toEtale⟩
local instance finiteEtaleInfStableUnderCompositionAffineThickening :
    MorphismProperty.IsStableUnderComposition
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) where
  comp_mem f g hf hg := by
    have hf' : IsFiniteEtale f := @IsFiniteEtale.mk _ _ _ hf.1 hf.2
    have hg' : IsFiniteEtale g := @IsFiniteEtale.mk _ _ _ hg.1 hg.2
    have hfg : IsFiniteEtale (f ≫ g) :=
      (inferInstance : MorphismProperty.IsStableUnderComposition
        (@IsFiniteEtale : MorphismProperty Scheme.{u})).comp_mem f g hf' hg'
    exact ⟨hfg.toIsFinite, hfg.toEtale⟩

Lean source · statement

theorem pullback_specMap_isEquivalence_of_surjective_of_ker_le_nilradical
    {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S)
    (hf : Function.Surjective f) (hker : RingHom.ker f ≤ nilradical R) :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤
      (Spec.map (CommRingCat.ofHom f))).IsEquivalence

theorem

pullback_isEquivalence_of_isAffine_of_surjective_closedImmersion

L126 ↗

AlgebraicGeometry.FiniteEtale.pullback_isEquivalence_of_isAffine_of_surjective_closedImmersion

Documentation

Pullback along a surjective closed immersion with affine target is an equivalence on the canonical category of finite étale covers.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeAffineThickening :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
local instance finiteEtaleInfContainsIdentitiesAffineThickening :
    MorphismProperty.ContainsIdentities
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) where
  id_mem X := by
    have h : IsFiniteEtale (𝟙 X) :=
      (inferInstance : MorphismProperty.ContainsIdentities
        (@IsFiniteEtale : MorphismProperty Scheme.{u})).id_mem X
    exact ⟨h.toIsFinite, h.toEtale⟩
local instance finiteEtaleInfStableUnderCompositionAffineThickening :
    MorphismProperty.IsStableUnderComposition
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) where
  comp_mem f g hf hg := by
    have hf' : IsFiniteEtale f := @IsFiniteEtale.mk _ _ _ hf.1 hf.2
    have hg' : IsFiniteEtale g := @IsFiniteEtale.mk _ _ _ hg.1 hg.2
    have hfg : IsFiniteEtale (f ≫ g) :=
      (inferInstance : MorphismProperty.IsStableUnderComposition
        (@IsFiniteEtale : MorphismProperty Scheme.{u})).comp_mem f g hf' hg'
    exact ⟨hfg.toIsFinite, hfg.toEtale⟩

Lean source · statement

theorem pullback_isEquivalence_of_isAffine_of_surjective_closedImmersion
    {X Y : Scheme.{u}} [IsAffine Y] (i : X ⟶ Y)
    [IsClosedImmersion i] [Surjective i] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ i).IsEquivalence

Module documentation

Finite étale covers of affine thickenings

Declarations