AlgebraicCurve.CurveModel.mem_openKummerUnits_of_finiteEtale_generic_root
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace AlgebraicCurve.CurveModel
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
variable {K F : Type} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]Lean source · statement
theorem mem_openKummerUnits_of_finiteEtale_generic_root
(M : CurveModel K F) {X : Scheme} [IsIntegral X]
(j : X ⟶ M.C) [IsOpenImmersion j]
(L : Type) [Field L] [Algebra X.functionField L]
{Y : Scheme} (f : Y ⟶ X) [IsFinite f] [Etale f]
(e : pullback f (X.fromSpecStalk (genericPoint X)) ≅ Spec (.of L))
(he : e.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap X.functionField L)) =
pullback.snd f (X.fromSpecStalk (genericPoint X)))
(a : X.functionFieldˣ) (b : L) (n : ℕ+)
(hb : b ^ (n : ℕ) = algebraMap X.functionField L (a : X.functionField)) :
Units.map (M.ffEquiv.trans j.functionFieldRingEquivOfIsOpenImmersion).symm.toMonoidHom a ∈
Pic0.openKummerUnits K F (M.openBoundaryPlaces j) n