NYLL
Module

Model.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.Model
1 declaration indexed from sourceView source ↗

Module documentation

Affine finite-field models of finite étale schemes

An actual finite étale cover of Spec (R ⊗[k] L) for an algebraic extension L/k is the pullback of an actual finite étale cover over a finite constant extension. The pullback uses the literal tensor map of the field inclusion.

Imports8
Imported by2

Declarations

theorem

exists_finiteIntermediateField_affine_model

L37 ↗
AlgebraicGeometry.FiniteEtale.exists_finiteIntermediateField_affine_model
Documentation

An actual finite étale cover of an affine constant extension descends along the literal coefficient inclusion to an actual finite intermediate field.

Source context 7 commands

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

noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace AlgebraicGeometry.FiniteEtale
variable (k L R : Type u) [Field k] [Field L] [CommRing R]
variable [Algebra k L] [Algebra k R]
Lean source · statement
theorem exists_finiteIntermediateField_affine_model
    [Algebra.IsAlgebraic k L]
    (X : AlgebraicGeometry.FiniteEtale (Spec (CommRingCat.of (R ⊗[k] L)))) :
    ∃ F : IntermediateField k L, FiniteDimensional k F ∧
      ∃ X₀ : AlgebraicGeometry.FiniteEtale (Spec (CommRingCat.of (R ⊗[k] F))),
        Nonempty ((AlgebraicGeometry.FiniteEtale.pullback
          (Spec.map (CommRingCat.ofHom
            (Algebra.TensorProduct.map (R := k) (S := R) (AlgHom.id R R) F.val).toRingHom))).obj
              X₀ ≅ X)

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