NYLL
Module

AdicCoverTower.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.AdicCoverTower
27 declarations indexed from sourceView source ↗

Module documentation

The actual adic tower of a finite étale closed-fibre cover

Starting from a finite étale cover of X × Spec (A / I), successive thickening invariance constructs covers of X × Spec (A / I^(n+1)). The transition morphisms are obtained from the actual Limits.pullback recovery isomorphisms, and their squares are proved cartesian.

This supplies the finite-cover system used in the proof of Stacks 0A48/0GS2 before applying 09ZT. It does not construct a cover of X; the effectivity step of Grothendieck existence is a separate, still required theorem.

Mathematical sources: https://stacks.math.columbia.edu/tag/0A48 https://stacks.math.columbia.edu/tag/0GS2 https://stacks.math.columbia.edu/tag/09ZT

Imports13
  • Nyll.EtaleFundamentalGroups.FiniteEtale.Thickening
  • Mathlib.AlgebraicGeometry.Morphisms.Proper
  • Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
  • Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
  • Mathlib.CategoryTheory.EssentialImage
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  • Mathlib.CategoryTheory.MorphismProperty.Comma
  • Mathlib.CategoryTheory.MorphismProperty.Composition
  • Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
  • Mathlib.RingTheory.Ideal.Operations
  • Mathlib.RingTheory.Ideal.Quotient.Defs
  • Mathlib.RingTheory.Nilpotent.Lemmas
  • Mathlib.RingTheory.Spectrum.Prime.Topology
Imported by1

Declarations

instance

finiteEtaleInfStableUnderBaseChangeAdicTower

L49 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.finiteEtaleInfStableUnderBaseChangeAdicTower
Source context 4 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
Lean source · statement
instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale)
def

levelIdeal

L57 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.levelIdeal
Documentation

Positive ideal powers, with the zeroth entry literally the given ideal.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
Lean source · full declaration
def levelIdeal (I : Ideal A) : ℕ → Ideal A
  | 0 => I
  | n + 1 => levelIdeal I n * I
theorem

levelIdeal_eq_pow

L61 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.levelIdeal_eq_pow
Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
Lean source · statement
theorem levelIdeal_eq_pow (I : Ideal A) (n : ℕ) : levelIdeal I n = I ^ (n + 1)
theorem

levelIdeal_succ_le

L68 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.levelIdeal_succ_le
Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
Lean source · statement
theorem levelIdeal_succ_le (I : Ideal A) (n : ℕ) :
    levelIdeal I (n + 1) ≤ levelIdeal I n
def

base

L73 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.base
Documentation

The actual quotient spectrum at the n+1-st ideal power.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
Lean source · statement
def base (I : Ideal A) (n : ℕ) : Scheme.{u}
def

baseInclusion

L77 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.baseInclusion
Documentation

The actual closed immersion from an ideal-power quotient spectrum.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
Lean source · statement
def baseInclusion (I : Ideal A) (n : ℕ) : base I n ⟶ Spec (CommRingCat.of A)
def

baseTransition

L81 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.baseTransition
Documentation

The quotient map induces the successive nilpotent thickening.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
Lean source · statement
def baseTransition (I : Ideal A) (n : ℕ) : base I n ⟶ base I (n + 1)
theorem

baseTransition_comp

L84 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.baseTransition_comp
Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
Lean source · statement
theorem baseTransition_comp (I : Ideal A) (n : ℕ) :
    baseTransition I n ≫ baseInclusion I (n + 1) = baseInclusion I n
theorem

baseTransition_isClosedImmersion

L91 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.baseTransition_isClosedImmersion
Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
Lean source · statement
theorem baseTransition_isClosedImmersion (I : Ideal A) (n : ℕ) :
    IsClosedImmersion (baseTransition I n)
theorem

factor_ker_le_nilradical

L97 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.factor_ker_le_nilradical
Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
Lean source · statement
theorem factor_ker_le_nilradical (I : Ideal A) (n : ℕ) :
    RingHom.ker (Ideal.Quotient.factor (levelIdeal_succ_le I n)) ≤
      nilradical (A ⧸ levelIdeal I (n + 1))
theorem

baseTransition_surjective

L113 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.baseTransition_surjective
Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
Lean source · statement
theorem baseTransition_surjective (I : Ideal A) (n : ℕ) :
    Surjective (baseTransition I n)
abbrev

level

L132 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.level
Documentation

The actual base change of X at level n+1.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
Lean source · statement
abbrev level (n : ℕ) : Scheme.{u}
def

transition

L135 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.transition
Documentation

The morphism between the actual successive base changes.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
Lean source · statement
def transition (n : ℕ) : level f I n ⟶ level f I (n + 1)
theorem

transition_fst

L153 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.transition_fst
Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
Lean source · statement
theorem transition_fst (n : ℕ) :
    transition f I n ≫ Limits.pullback.fst f (baseInclusion I (n + 1)) =
      Limits.pullback.fst f (baseInclusion I n)
theorem

transition_snd

L158 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.transition_snd
Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
Lean source · statement
theorem transition_snd (n : ℕ) :
    transition f I n ≫ Limits.pullback.snd f (baseInclusion I (n + 1)) =
      Limits.pullback.snd f (baseInclusion I n) ≫ baseTransition I n
theorem

transition_isPullback

L163 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.transition_isPullback
Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
Lean source · statement
theorem transition_isPullback (n : ℕ) :
    IsPullback (transition f I n) (Limits.pullback.snd f (baseInclusion I n))
      (Limits.pullback.snd f (baseInclusion I (n + 1))) (baseTransition I n)
theorem

transition_isClosedImmersion

L171 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.transition_isClosedImmersion
Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
Lean source · statement
theorem transition_isClosedImmersion (n : ℕ) :
    IsClosedImmersion (transition f I n)
theorem

transition_surjective

L176 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.transition_surjective
Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
Lean source · statement
theorem transition_surjective (n : ℕ) :
    Surjective (transition f I n)
def

cover

L187 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.cover
Documentation

The covers are constructed by recursion from the supplied closed-fibre cover.

Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
section LiftedCover
variable (V : MorphismProperty.Over
  ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ (level f I 0))
Lean source · statement
def cover (n : ℕ) :
    MorphismProperty.Over
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ (level f I n)
theorem

cover_zero

L206 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.cover_zero
Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
section LiftedCover
variable (V : MorphismProperty.Over
  ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ (level f I 0))
Lean source · statement
theorem cover_zero : cover f I V 0 = V
def

coverRecoveryIso

L209 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.coverRecoveryIso
Documentation

The chosen lifts recover the previous level under the literal pullback functor.

Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
section LiftedCover
variable (V : MorphismProperty.Over
  ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ (level f I 0))
Lean source · statement
def coverRecoveryIso (n : ℕ) :
    (MorphismProperty.Over.pullback
          ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ (transition f I n)).obj
        (cover f I V (n + 1)) ≅
      cover f I V n
def

underlyingRecoveryIso

L227 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.underlyingRecoveryIso
Documentation

The recovery isomorphism on the actual underlying pullback schemes.

Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
section LiftedCover
variable (V : MorphismProperty.Over
  ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ (level f I 0))
Lean source · statement
def underlyingRecoveryIso (n : ℕ) :
    Limits.pullback (cover f I V (n + 1)).hom (transition f I n) ≅ (cover f I V n).left
theorem

recovery_inv_snd

L233 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.recovery_inv_snd
Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
section LiftedCover
variable (V : MorphismProperty.Over
  ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ (level f I 0))
Lean source · statement
theorem recovery_inv_snd (n : ℕ) :
    (underlyingRecoveryIso f I V n).inv ≫
        Limits.pullback.snd (cover f I V (n + 1)).hom (transition f I n) =
      (cover f I V n).hom
def

coverTransition

L240 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.coverTransition
Documentation

The actual scheme morphism joining consecutive lifted covers.

Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
section LiftedCover
variable (V : MorphismProperty.Over
  ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ (level f I 0))
Lean source · statement
def coverTransition (n : ℕ) :
    (cover f I V n).left ⟶ (cover f I V (n + 1)).left
theorem

coverTransition_comm

L245 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.coverTransition_comm
Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
section LiftedCover
variable (V : MorphismProperty.Over
  ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ (level f I 0))
Lean source · statement
theorem coverTransition_comm (n : ℕ) :
    coverTransition f I V n ≫ (cover f I V (n + 1)).hom =
      (cover f I V n).hom ≫ transition f I n
theorem

coverTransition_isPullback

L254 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.coverTransition_isPullback
Documentation

Every successor square in the constructed cover tower is cartesian.

Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
section LiftedCover
variable (V : MorphismProperty.Over
  ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ (level f I 0))
Lean source · statement
theorem coverTransition_isPullback (n : ℕ) :
    IsPullback (coverTransition f I V n) (cover f I V n).hom
      (cover f I V (n + 1)).hom (transition f I n)
theorem

exists_proper_finiteEtale_cover_tower

L264 ↗
AlgebraicGeometry.FiniteEtale.AdicCoverTower.exists_proper_finiteEtale_cover_tower
Documentation

For a proper original scheme this is the actual finite-cover input of 09ZT. No completeness or Noetherian hypothesis is needed to construct the tower itself.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.FiniteEtale.AdicCoverTower
local instance finiteEtaleInfStableUnderBaseChangeAdicTower :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf
variable {A : Type u} [CommRing A]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) (I : Ideal A)
Lean source · statement
theorem exists_proper_finiteEtale_cover_tower [IsProper f]
    (V : MorphismProperty.Over
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤
      (Limits.pullback f (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))))) :
    ∃ W : (n : ℕ) → MorphismProperty.Over
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ (level f I n),
      ∃ r : (n : ℕ) → (W n).left ⟶ (W (n + 1)).left,
        W 0 = V ∧
        (∀ n : ℕ, IsPullback (r n) (W n).hom (W (n + 1)).hom (transition f I n)) ∧
        (∀ n : ℕ, IsProper ((W n).hom ≫ Limits.pullback.snd f (baseInclusion I n)))

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