AlgebraicCurve.CurveModel.ramificationIndexAlong_eq_one_outside_openBoundary
The actual formally unramified open restriction forces ramification index one at every place of its interior.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
open AlgebraicCurves.Models.Proofs
open CurveModel_ramificationIndexAlong_pointEquivPlace_eq_one_of_formallyUnramified
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smoothLean source · statement
theorem ramificationIndexAlong_eq_one_outside_openBoundary
{K F E : Type} [Field K] [IsAlgClosed K]
[Field F] [Field E] [Algebra K F] [Algebra K E]
(M : CurveModel K F) (N : CurveModel K E)
(φ : F →ₐ[K] E) (hφ : φ.toRingHom.IsIntegral)
(d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase)
(hgen : N.C.fromSpecStalk (genericPoint N.C) ≫ d =
Spec.map (CommRingCat.ofHom (N.ffEquiv.toRingHom.comp
(φ.toRingHom.comp M.ffEquiv.symm.toRingHom))) ≫
M.C.fromSpecStalk (genericPoint M.C))
{Y : Scheme} (k : Y ⟶ N.C) [IsOpenImmersion k]
[FormallyUnramified (k ≫ d)]
(w : Place K E) (hw : w ∉ N.openBoundaryPlaces k) :
Place.ramificationIndexAlong φ w = 1