NYLL
Module

PureInseparableAffine.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.PureInseparableAffine
15 declarations indexed from sourceView source ↗

Module documentation

Pure Inseparable Affine

The Frobenius power on every algebra, including the zero algebra.

Imports7
Imported by2

Declarations

def

algebraFrobeniusPower

L29 ↗
EtaleFundamentalGroups.algebraFrobeniusPower
Documentation

The Frobenius power on every algebra, including the zero algebra.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
def algebraFrobeniusPower (R : Type u) [CommRing R] [Algebra k R] : R →+* R
theorem

algebraFrobeniusPower_apply

L36 ↗
EtaleFundamentalGroups.algebraFrobeniusPower_apply
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
theorem algebraFrobeniusPower_apply (R : Type u) [CommRing R] [Algebra k R] (x : R) :
    algebraFrobeniusPower k p n R x = x ^ p ^ n
theorem

algebraFrobeniusPower_naturality

L45 ↗
EtaleFundamentalGroups.algebraFrobeniusPower_naturality
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
theorem algebraFrobeniusPower_naturality
    (R B : Type u) [CommRing R] [Algebra k R] [CommRing B] [Algebra k B] (f : R →+* B) :
    f.comp (algebraFrobeniusPower k p n R) =
      (algebraFrobeniusPower k p n B).comp f
theorem

specAlgebraFrobeniusPower_surjective

L53 ↗
EtaleFundamentalGroups.specAlgebraFrobeniusPower_surjective
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
theorem specAlgebraFrobeniusPower_surjective
    (R : Type u) [CommRing R] [Algebra k R] :
    Surjective (Spec.map (CommRingCat.ofHom (algebraFrobeniusPower k p n R)))
theorem

specAlgebraFrobeniusPower_universallyInjective

L63 ↗
EtaleFundamentalGroups.specAlgebraFrobeniusPower_universallyInjective
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
theorem specAlgebraFrobeniusPower_universallyInjective
    (R : Type u) [CommRing R] [Algebra k R] :
    UniversallyInjective (Spec.map (CommRingCat.ofHom (algebraFrobeniusPower k p n R)))
abbrev

affineCoordinateAlgebra

L85 ↗
EtaleFundamentalGroups.affineCoordinateAlgebra
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
abbrev affineCoordinateAlgebra (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) :
    Algebra k Γ(X, ⊤)
def

affineSchemeFrobeniusPower

L90 ↗
EtaleFundamentalGroups.affineSchemeFrobeniusPower
Documentation

Frobenius power on an affine scheme over a field.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
def affineSchemeFrobeniusPower (X : Scheme.{u}) [IsAffine X]
    (f : X ⟶ Spec (.of k)) : X ⟶ X
theorem

affineSchemeFrobeniusPower_naturality

L96 ↗
EtaleFundamentalGroups.affineSchemeFrobeniusPower_naturality
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
theorem affineSchemeFrobeniusPower_naturality
    (X Y : Scheme.{u}) [IsAffine X] [IsAffine Y]
    (f : X ⟶ Spec (.of k)) (g : Y ⟶ Spec (.of k)) (a : X ⟶ Y) :
    a ≫ affineSchemeFrobeniusPower k p n Y g =
      affineSchemeFrobeniusPower k p n X f ≫ a
theorem

affineSchemeFrobeniusPower_surjective

L116 ↗
EtaleFundamentalGroups.affineSchemeFrobeniusPower_surjective
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
theorem affineSchemeFrobeniusPower_surjective
    (X : Scheme.{u}) [IsAffine X] (f : X ⟶ Spec (.of k)) :
    Surjective (affineSchemeFrobeniusPower k p n X f)
theorem

affineSchemeFrobeniusPower_universallyInjective

L126 ↗
EtaleFundamentalGroups.affineSchemeFrobeniusPower_universallyInjective
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
theorem affineSchemeFrobeniusPower_universallyInjective
    (X : Scheme.{u}) [IsAffine X] (f : X ⟶ Spec (.of k)) :
    UniversallyInjective (affineSchemeFrobeniusPower k p n X f)
def

affineSchemeRelativeFrobenius

L137 ↗
EtaleFundamentalGroups.affineSchemeRelativeFrobenius
Documentation

Relative Frobenius, with the actual scheme pullback as its target.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
def affineSchemeRelativeFrobenius
    (X Y : Scheme.{u}) [IsAffine X] [IsAffine Y]
    (g : Y ⟶ Spec (.of k)) (a : X ⟶ Y) :
    X ⟶ pullback (affineSchemeFrobeniusPower k p n Y g) a
theorem

affineSchemeRelativeFrobenius_isIso

L145 ↗
EtaleFundamentalGroups.affineSchemeRelativeFrobenius_isIso
Documentation

Relative Frobenius on affine étale schemes is invertible, including empty schemes.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
theorem affineSchemeRelativeFrobenius_isIso
    (X Y : Scheme.{u}) [IsAffine X] [IsAffine Y]
    (g : Y ⟶ Spec (.of k)) (a : X ⟶ Y) [Etale a] :
    IsIso (affineSchemeRelativeFrobenius k p n X Y g a)
def

affineFrobeniusPullbackObjIso

L183 ↗
EtaleFundamentalGroups.affineFrobeniusPullbackObjIso
Documentation

Pullback by Frobenius recovers each actual finite étale cover of an affine scheme.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
def affineFrobeniusPullbackObjIso
    (X : Scheme.{u}) [IsAffine X] (f : X ⟶ Spec (.of k))
    (Z : AlgebraicGeometry.FiniteEtale X) :
    Z ≅ (AlgebraicGeometry.FiniteEtale.pullback
      (affineSchemeFrobeniusPower k p n X f)).obj Z
theorem

affineSchemeFrobeniusPower_spec

L198 ↗
EtaleFundamentalGroups.affineSchemeFrobeniusPower_spec
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
theorem affineSchemeFrobeniusPower_spec
    (R : Type u) [CommRing R] [Algebra k R] (f : Spec (.of R) ⟶ Spec (.of k)) :
    affineSchemeFrobeniusPower k p n (Spec (.of R)) f =
      Spec.map (CommRingCat.ofHom (algebraFrobeniusPower k p n R))
theorem

exists_affine_purelyInseparable_model

L219 ↗
EtaleFundamentalGroups.exists_affine_purelyInseparable_model
Documentation

Every finite étale cover after a finite purely inseparable constant extension has an actual model over the original affine scheme.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k : Type u) [Field k] (p n : ℕ) [ExpChar k p]
Lean source · statement
theorem exists_affine_purelyInseparable_model
    (L : Type u) [Field L] [Algebra k L] [IsPurelyInseparable k L]
    [FiniteDimensional k L] (X : Scheme.{u}) [IsAffine X]
    (f : X ⟶ Spec (.of k))
    (Z : AlgebraicGeometry.FiniteEtale
      (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)) :
    ∃ M : AlgebraicGeometry.FiniteEtale X,
      Nonempty ((AlgebraicGeometry.FiniteEtale.pullback
        (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)).obj M ≅ Z)

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