Module

ConstantFieldLimit.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.ConstantFieldLimit

17 declarations indexed from sourceView source ↗

Module documentation

Constant-field base changes as an inverse limit

For any field extension, the base change of a scheme is the inverse limit of its base changes by the intermediate fields generated by finite coefficient sets. The transition maps are affine, and the stages inherit quasi-compactness and quasi-separatedness from the original scheme. For algebraic extensions, these intermediate fields are finite-dimensional.

Imports12

Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.AlgebraicGeometry.Morphisms.Affine
Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.Adjunction.Limits
Mathlib.CategoryTheory.Comma.Over.Basic
Mathlib.CategoryTheory.Comma.Over.Pullback
Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Mathlib.CategoryTheory.Limits.Opposites
Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.IntermediateFieldDiagram

Imported by3

def

coefficientSpecFunctor

L35 ↗

EtaleFundamentalGroups.coefficientSpecFunctor

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

def coefficientSpecFunctor :
    (Under (CommRingCat.of k))ᵒᵖ ⥤ Over (Spec (CommRingCat.of k))

def

constantFieldInverseLimitOverDiagram

L40 ↗

EtaleFundamentalGroups.constantFieldInverseLimitOverDiagram

Documentation

The actual constant-field base changes, together with their projections to X.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

def constantFieldInverseLimitOverDiagram (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) : (Finset L)ᵒᵖ ⥤ Over X

def

constantFieldInverseLimitOverCone

L45 ↗

EtaleFundamentalGroups.constantFieldInverseLimitOverCone

Documentation

The native L point and maps to every finite-coefficient stage over X.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

def constantFieldInverseLimitOverCone (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) :
    Cone (constantFieldInverseLimitOverDiagram k L X f)

def

constantFieldInverseLimitOverConeIsLimit

L52 ↗

EtaleFundamentalGroups.constantFieldInverseLimitOverConeIsLimit

Documentation

Base change to L is the inverse limit in the category over X.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

def constantFieldInverseLimitOverConeIsLimit (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) :
    IsLimit (constantFieldInverseLimitOverCone k L X f)

def

constantFieldInverseLimitDiagram

L62 ↗

EtaleFundamentalGroups.constantFieldInverseLimitDiagram

Documentation

The underlying actual constant-field base changes indexed by finite coefficients.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

def constantFieldInverseLimitDiagram (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k)) :
    (Finset L)ᵒᵖ ⥤ Scheme.{u}

def

constantFieldInverseLimitProjection

L67 ↗

EtaleFundamentalGroups.constantFieldInverseLimitProjection

Documentation

The constant-field stages carry their canonical compatible projections to X.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

def constantFieldInverseLimitProjection (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) :
    constantFieldInverseLimitDiagram k L X f ⟶ (Functor.const (Finset L)ᵒᵖ).obj X

def

constantFieldInverseLimitCone

L72 ↗

EtaleFundamentalGroups.constantFieldInverseLimitCone

Documentation

The underlying native cone whose point is base change to L.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

def constantFieldInverseLimitCone (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k)) :
    Cone (constantFieldInverseLimitDiagram k L X f)

theorem

constantFieldInverseLimitCone_π_projection

L77 ↗

EtaleFundamentalGroups.constantFieldInverseLimitCone_π_projection

Documentation

Every component of the inverse-limit cone is a morphism over X.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem constantFieldInverseLimitCone_π_projection (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) :
    (constantFieldInverseLimitCone k L X f).π ≫ constantFieldInverseLimitProjection k L X f =
      (Functor.const (Finset L)ᵒᵖ).map
        (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)

def

constantFieldInverseLimitConeIsLimit

L86 ↗

EtaleFundamentalGroups.constantFieldInverseLimitConeIsLimit

Documentation

Constant-field base change to L is the actual inverse limit of its stages.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

def constantFieldInverseLimitConeIsLimit (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) :
    IsLimit (constantFieldInverseLimitCone k L X f)

theorem

constantFieldInverseLimitOverDiagram_obj_left

L93 ↗

EtaleFundamentalGroups.constantFieldInverseLimitOverDiagram_obj_left

Documentation

Every stage is the literal pullback by its finitely generated intermediate field.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem constantFieldInverseLimitOverDiagram_obj_left (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) (s : (Finset L)ᵒᵖ) :
    ((constantFieldInverseLimitOverDiagram k L X f).obj s).left =
      pullback (Spec.map (CommRingCat.ofHom
        (algebraMap k (IntermediateField.adjoin k (s.unop : Set L))))) f

theorem

constantFieldInverseLimitOverDiagram_obj_hom

L101 ↗

EtaleFundamentalGroups.constantFieldInverseLimitOverDiagram_obj_hom

Documentation

The stage projection to X is the literal second pullback projection.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem constantFieldInverseLimitOverDiagram_obj_hom (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) (s : (Finset L)ᵒᵖ) :
    ((constantFieldInverseLimitOverDiagram k L X f).obj s).hom =
      pullback.snd (Spec.map (CommRingCat.ofHom
        (algebraMap k (IntermediateField.adjoin k (s.unop : Set L))))) f

theorem

constantFieldInverseLimitOverCone_pt_left

L109 ↗

EtaleFundamentalGroups.constantFieldInverseLimitOverCone_pt_left

Documentation

The cone point is the literal pullback by L.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem constantFieldInverseLimitOverCone_pt_left (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) :
    (constantFieldInverseLimitOverCone k L X f).pt.left =
      pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f

theorem

constantFieldInverseLimitOverCone_pt_hom

L116 ↗

EtaleFundamentalGroups.constantFieldInverseLimitOverCone_pt_hom

Documentation

The cone point projection to X is the literal second pullback projection.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem constantFieldInverseLimitOverCone_pt_hom (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) :
    (constantFieldInverseLimitOverCone k L X f).pt.hom =
      pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f

theorem

constantFieldInverseLimitDiagram_map_isAffineHom

L123 ↗

EtaleFundamentalGroups.constantFieldInverseLimitDiagram_map_isAffineHom

Documentation

The constant-field inverse system has affine transition maps.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem constantFieldInverseLimitDiagram_map_isAffineHom (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k))
    {i j : (Finset L)ᵒᵖ} (g : i ⟶ j) :
    IsAffineHom ((constantFieldInverseLimitDiagram k L X f).map g)

theorem

constantFieldInverseLimitDiagram_obj_compactSpace

L145 ↗

EtaleFundamentalGroups.constantFieldInverseLimitDiagram_obj_compactSpace

Documentation

Constant-field stages of a quasi-compact scheme are quasi-compact.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem constantFieldInverseLimitDiagram_obj_compactSpace (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) [CompactSpace X]
    (s : (Finset L)ᵒᵖ) :
    CompactSpace ((constantFieldInverseLimitDiagram k L X f).obj s)

theorem

constantFieldInverseLimitDiagram_obj_quasiSeparatedSpace

L159 ↗

EtaleFundamentalGroups.constantFieldInverseLimitDiagram_obj_quasiSeparatedSpace

Documentation

Constant-field stages of a quasi-separated scheme are quasi-separated.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem constantFieldInverseLimitDiagram_obj_quasiSeparatedSpace (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) [QuasiSeparatedSpace X]
    (s : (Finset L)ᵒᵖ) :
    QuasiSeparatedSpace ((constantFieldInverseLimitDiagram k L X f).obj s)

theorem

constantFieldInverseLimitCone_π_app_fst

L173 ↗

EtaleFundamentalGroups.constantFieldInverseLimitCone_π_app_fst

Documentation

The cone maps preserve the coefficient projection along the literal field inclusion.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem constantFieldInverseLimitCone_π_app_fst
    (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k)) (s : Finset L) :
    (constantFieldInverseLimitCone k L X f).π.app (op s) ≫
        pullback.fst (Spec.map (CommRingCat.ofHom
          (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f =
      pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k L))) f ≫
        Spec.map (CommRingCat.ofHom
          (IntermediateField.adjoin k (s : Set L)).val.toRingHom)

Module documentation

Constant-field base changes as an inverse limit

Declarations