Module

ConstantFieldCover.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.ConstantFieldCover

4 declarations indexed from sourceView source ↗

Module documentation

Open covers after constant-field extension

The constant-field base change of an open cover retains its index type and literal pullback charts. Its chart inclusions preserve both projections, and affine charts remain affine.

Imports5

Mathlib.AlgebraicGeometry.Cover.Open
Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Mathlib.AlgebraicGeometry.Morphisms.Affine
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Imported by4

def

constantFieldOpenCover

L27 ↗

EtaleFundamentalGroups.constantFieldOpenCover

Documentation

Base change of an open cover, with chart objects the literal constant-field base changes of the original charts and the same index type.

Source context 5 commands

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

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

Lean source · statement

def constantFieldOpenCover (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
    (𝒰 : Scheme.OpenCover.{v} X) :
    Scheme.OpenCover.{v} (pullback (Spec.map (CommRingCat.ofHom (algebraMap k E))) f)

theorem

constantFieldOpenCover_f_fst

L46 ↗

EtaleFundamentalGroups.constantFieldOpenCover_f_fst

Documentation

The literal chart inclusion preserves the coefficient projection.

Source context 5 commands

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

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

Lean source · statement

theorem constantFieldOpenCover_f_fst (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) (𝒰 : Scheme.OpenCover.{v} X) (i : 𝒰.I₀) :
    (constantFieldOpenCover k E X f 𝒰).f i ≫
        pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k E))) f =
      pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k E))) (𝒰.f i ≫ f)

theorem

constantFieldOpenCover_f_snd

L54 ↗

EtaleFundamentalGroups.constantFieldOpenCover_f_snd

Documentation

The literal chart inclusion lies over the original chart inclusion.

Source context 5 commands

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

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

Lean source · statement

theorem constantFieldOpenCover_f_snd (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) (𝒰 : Scheme.OpenCover.{v} X) (i : 𝒰.I₀) :
    (constantFieldOpenCover k E X f 𝒰).f i ≫
        pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k E))) f =
      pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k E))) (𝒰.f i ≫ f) ≫ 𝒰.f i

theorem

constantFieldOpenCover_isAffine

L62 ↗

EtaleFundamentalGroups.constantFieldOpenCover_isAffine

Documentation

Affine charts stay affine under the literal constant-field cover construction.

Source context 5 commands

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

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

Lean source · statement

theorem constantFieldOpenCover_isAffine (X : Scheme.{u})
    (f : X ⟶ Spec (CommRingCat.of k)) (𝒰 : Scheme.OpenCover.{v} X)
    (i : 𝒰.I₀) [IsAffine (𝒰.X i)] :
    IsAffine ((constantFieldOpenCover k E X f 𝒰).X i)

Module documentation

Open covers after constant-field extension

Declarations

constantFieldOpenCover

constantFieldOpenCover_f_fst

constantFieldOpenCover_f_snd

constantFieldOpenCover_isAffine