Nyll.EtaleFundamentalGroups.Inertia.FractionFieldSpecNormalization

Module documentation

The actual function field over a fraction-field spectrum

The algebra defined by the structure morphism of Spec K agrees with the composite of the two canonical fraction-field maps. This comparison is made before installing the scalar tower, so the resulting fraction-ring structure uses precisely the algebra of normalization geometry.

theorem

affineMorphismFunctionFieldAlgebra_isFractionRing

L29 ↗

EtaleFundamentalGroups.Inertia.affineMorphismFunctionFieldAlgebra_isFractionRing

Documentation

The actual function field of the spectrum of a fraction field is a fraction field of the original ring for its geometric structure algebra.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · full declaration

theorem affineMorphismFunctionFieldAlgebra_isFractionRing
    (R K : Type u) [CommRing R] [IsDomain R]
    [Field K] [Algebra R K] [IsFractionRing R K] :
    let : Algebra R (Spec (.of K)).functionField :=
      affineMorphismFunctionFieldAlgebra R
        (Spec.map (CommRingCat.ofHom (algebraMap R K)))
    IsFractionRing R (Spec (.of K)).functionField := by
  let F : Type u := (Spec (.of K)).functionField
  let : Algebra K F := AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (.of K)
  rw [affineMorphismFunctionFieldAlgebra_specMap R K (algebraMap R K)]
  let : Algebra R F := ((algebraMap K F).comp (algebraMap R K)).toAlgebra
  let : IsScalarTower R K F := IsScalarTower.of_algebraMap_eq' rfl
  let : IsFractionRing K F := AlgebraicGeometry.functionField_isFractionRing_of_affine (.of K)
  exact IsFractionRing.trans R K F

Module documentation

The actual function field over a fraction-field spectrum

Declarations

affineMorphismFunctionFieldAlgebra_isFractionRing