Research proof index

The integral model of the base change is the base change of the integral model. Both sides are lifts of E.baseChange l along the injective map 𝒪[l] → l (injectivity from IsFractionRing), and lifts along an injective map are unique: compare coefficientwise via integralModel_a₁_eq on both sides and the commuting square algebraMap_integerMap. (O...

The c₄ of the base change has adic valuation 1. Multiplicative reduction of E makes the canonical valuation |E.c₄| = 1 (via adicValuation_eq_one_iff and integralModel_c₄_eq, as in WeierstrassCurve.valuation_c₄_eq_one); this transfers to l by valuation_algebraMap_eq_one, and converts back to the adic valuation over 𝒪[l]. Shared by `isM...

The discriminant of the base change has adic valuation < 1. Multiplicative reduction of E makes |E.Δ| < 1 (via adicValuation_lt_one_iff and integralModel_Δ_eq, as in WeierstrassCurve.valuation_Δ_lt_one); this transfers to l by valuation_algebraMap_lt_one, and converts back to the adic valuation over 𝒪[l].