Module

GeometricStalkFractionFieldMap.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkFractionFieldMap

2 declarations indexed from sourceView source ↗

Module documentation

The actual strict generic field map over a normal local domain

The actual geometric stalk is a domain, and its local structure map is faithfully flat and injective. Localizing this injection constructs the map between the actual fraction fields and its compatibility with the original structure map. Neither a DVR nor a generic tensor comparison is required.

Imports3

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkNormalDomain
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkFlat
Mathlib.RingTheory.Localization.FractionRing

Imported by11

def

geometricStalkFractionFieldMap

L34 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkFractionFieldMap

Documentation

The actual field map obtained from the actual geometric-stalk injection.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [IsLocalRing R] [Field Ω] (φ : R →+* Ω) [IsLocalHom φ]

Lean source · statement

def geometricStalkFractionFieldMap :
    FractionRing R →+* FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ)))

theorem

geometricStalkFractionFieldMap_algebraMap

L39 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkFractionFieldMap_algebraMap