EtaleFundamentalGroups.StrictHenselian.geometricStalkFractionFieldMap_comp_fractionStalkToSupportComplement
The actual strict generic Cartier morphism factors through the actual local fraction field using the induced field map over a normal domain stalk.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe uLean source · statement
theorem geometricStalkFractionFieldMap_comp_fractionStalkToSupportComplement
{X : Scheme.{u}} (D : X.EffectiveCartierDivisor) (x : X)
[IsDomain (X.presheaf.stalk x)] [IsIntegrallyClosed (X.presheaf.stalk x)]
{Ω : Type u} [Field Ω] [IsSepClosed Ω]
(φ : X.presheaf.stalk x →+* Ω) [IsLocalHom φ] :
Spec.map (CommRingCat.ofHom (geometricStalkFractionFieldMap φ)) ≫
D.2.fractionStalkToSupportComplement x =
geometricStalkFractionFieldToComplement D x φ