AlgebraicCurve.Place.ord_algebraMap_eq_mul_ord_of_constant_extension
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_algebraMap_eq_mul_ord_of_constant_extension
attribute [-instance]
AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
instIsScalarTowerResidueFieldRestrictPushforward
instAlgebraResidueFieldRestrictPushforward
instIsLocalHomRestrictInclusion
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Pic.baseChange_mk
AlgebraicCurve.Place.forgetConstants_toValuationSubring
AlgebraicCurve.Place.constantFieldEquiv_symm_apply AlgebraicCurve.Place.ord_forgetConstants
AlgebraicCurve.Place.extendConstants_toValuationSubring
AlgebraicCurve.Place.constantFieldEquiv_apply_toValuationSubring
AlgebraicCurve.Place.mem_fiberConstants AlgebraicCurve.Place.restrictConstants_toValuationSubring
AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
AlgebraicCurve.Pic0.coe_pullbackDegZeroHom AlgebraicCurve.Place.placeOfPrime_toValuationSubring
AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.ord_algebraMap_eq_mul_ord_of_constant_extension
{k K E F E' F' : Type*} [Field k] [Field K] [Field E] [Field F] [Field E'] [Field F']
[Algebra k K] [Algebra.IsAlgebraic k K] [Algebra.IsSeparable k K]
[Algebra k E] [Algebra k F] [Algebra E F] [IsScalarTower k E F]
[Algebra K E'] [Algebra K F'] [Algebra E' F'] [IsScalarTower K E' F']
[Algebra E E'] [Algebra F F'] [Algebra k E'] [Algebra k F']
[IsScalarTower k K E'] [IsScalarTower k E E'] [IsScalarTower k K F'] [IsScalarTower k F F']
(hsq : ∀ e : E, algebraMap F F' (algebraMap E F e) = algebraMap E' F' (algebraMap E E' e))
(hgenE : Algebra.adjoin E (Set.range (algebraMap K E')) = ⊤)
(hgenF : Algebra.adjoin F (Set.range (algebraMap K F')) = ⊤)
(x : Place k F) (y : Place k E) (x' : Place K F') (y' : Place K E')
(hx : x'.toValuationSubring.comap (algebraMap F F') = x.toValuationSubring)
(hy : y'.toValuationSubring.comap (algebraMap E E') = y.toValuationSubring)
(hx'y' : x'.toValuationSubring.comap (algebraMap E' F') = y'.toValuationSubring)
(n : ℕ) (u : E) (hu : y.ord u = 1) (hn : x.ord (algebraMap E F u) = n) :
∀ f : E', x'.ord (algebraMap E' F' f) = n * y'.ord f