Evaluating a substitution over coefficients that need not be discrete #
Mathlib evaluates a substitution only over discrete coefficients: MvPowerSeries.eval₂_subst and
MvPowerSeries.comp_subst_apply both carry [DiscreteUniformity R] [DiscreteUniformity S] on the
two coefficient rings. That is unsatisfiable exactly where the statement is wanted. Substituting a
parameter into a formal expansion over an adic ring and evaluating back into that same ring needs
the coefficients and the evaluation target to be the same type, and one type cannot carry both
the adic and the discrete uniformity as instances.
MvPowerSeries.aeval_subst is that conclusion with an arbitrary uniform structure on the
coefficients. Nothing topological beyond a uniformity is asked of the ring the substituted family
lives over, and the evaluation target carries exactly the hypotheses of MvPowerSeries.comp_aeval.
That generality is available because Mathlib's evaluation API asks for no discreteness anywhere:
discreteness enters its substitution API only through MvPowerSeries.substAlgHom_eq_aeval, from
how subst is tied to aeval, and not from the composition fact itself. So all three rings may
be instantiated at one adic ring with no letI at the use site.
Discreteness is recovered inside the proof, where it belongs. MvPowerSeries.subst is by
definition an evaluation for the discrete uniformities; the pi topology those induce is finer than
the ambient one (MvPowerSeries.WithPiTopology.instTopologicalSpace_mono); and a map continuous
for the ambient source topology is continuous for a finer one (continuous_le_dom). In the
discrete world both sides are therefore continuous algebra homomorphisms out of
MvPowerSeries σ R; MvPowerSeries.aeval_unique identifies each with an evaluation; and the two
evaluations agree because both send X s to ε (a s). Every ambient fact is taken before the
uniformities are shadowed, so the evaluation the statement is about is never re-elaborated.
Main results #
MvPowerSeries.aeval_subst: a continuous algebra homomorphism applied to a substitution is the evaluation at the substituted family.PowerSeries.aeval_subst: the same for a substitution into a univariate series.PowerSeries.eval₂_toMvPowerSeriesandPowerSeries.eval₂_id_toMvPowerSeries: evaluating a univariate series viewed in several variables is evaluating it at the matching entry of the family — the case ofaeval_substat a single variable, which is how a one-variable series meets a two-variable evaluation.MvPowerSeries.hasSubst_pair: a pair of series with vanishing constant coefficient is a legitimate substitution family for the two variables indexed byUnit ⊕ Unit.MvPowerSeries.coordSpecialize,MvPowerSeries.hasSubst_coordSpecializeand the twosubst_coordSpecialize_X_*lemmas : the substitution sending one coordinate variable toXand every other to0, for an index type of any size.MvPowerSeries.ne_of_subst_eq_X_of_subst_eq_zero: a substitution sending one series toXand another to0separates them.
Separating multivariable parameters #
The second group of results above is about distinguishing series rather than evaluating them.
Two series of MvPowerSeries σ' O can be told apart by exhibiting a substitution that sends one
to X and the other to 0, since X ≠ 0 in a nontrivial coefficient ring; coordSpecialize i
is the substitution that does this for the coordinate variables, specializing X i to X and
every other coordinate to 0. Together they turn a distinctness obligation into a computation
with subst, which is how a multivariable identity proved by comparing parametrized points gets
its "the parameters are pairwise distinct" hypotheses. hasSubst_pair is the companion for the
two-variable case, packaging the substitutability side condition that every substitution into a
two-variable series has to discharge.
The two aeval_subst results are wanted for the formal group of an elliptic curve over a complete
local ring, where the group law is a power series over the very ring it is evaluated in: the
involution relating the w-expansion to the formal inverse is an identity between two such
evaluated substitutions. The two toMvPowerSeries results serve the same development from the
other side: the chord construction is a two-variable series, and its identities are proved by
evaluating one-variable series — w, the slope, the formal inverse — at entries of the pair.
Provenance #
Adapted from Michael Stoll's EllipticCurves (github.com/MichaelStollBayreuth/EllipticCurves,
Apache-2.0) at commit 66889eada51a74c2f5dfb7fb5909b0b5a0a2d96e, file
EllipticCurves/Mathlib/Chabauty/MvPSeries.lean, where this is
ChabautyColeman.MvPSeries.eval_subst, stated for a single ring and for that development's own
eval. Here the three rings are independent and the statement is about Mathlib's
MvPowerSeries.aeval; it equally generalises Mathlib's MvPowerSeries.eval₂_subst, whose
DiscreteUniformity hypotheses it removes.
PowerSeries.eval₂_toMvPowerSeries and PowerSeries.eval₂_id_toMvPowerSeries are the same
source file's eval_pair_rename and eval_pair_subst_single, respelled: the source moves a
one-variable series into two variables along MvPowerSeries.rename (fun _ ↦ i), whereas these
transport along PowerSeries.toMvPowerSeries i.
The proof is not the source's. That one establishes continuity of subst for the ambient product
topologies (its own MvPowerSeries.continuous_subst') and applies uniqueness there; refining the
source topology to the discrete one instead lets Mathlib's own MvPowerSeries.continuous_subst do
the work, so no new continuity lemma is needed.
Applying a continuous algebra homomorphism to a substitution is evaluating at the substituted family — with no discreteness asked of either coefficient ring.
This is MvPowerSeries.comp_subst_apply without its DiscreteUniformity hypotheses; the
evaluation target carries exactly the hypotheses of MvPowerSeries.comp_aeval. The evaluation of
the substituted family is a hypothesis rather than MvPowerSeries.HasSubst.hasEval, because that
one is stated for the discrete topology on S, which is not the topology this statement is
about.
The substitution family determined by an ordered pair, for the two variables indexed by
Unit ⊕ Unit: the left variable goes to q₁ and the right to q₂.
Substituting a pair of series into a two-variable one is subst (pairSubstitution q₁ q₂) f.
It is a reducible abbreviation, so Sum.elim_inl and Sum.elim_inr evaluate it at the two
variables; hasSubst_pair says it is substitutable as soon as both series vanish at the origin.
Equations
- q₁.pairSubstitution q₂ = Sum.elim (fun (x : Unit) => q₁) fun (x : Unit) => q₂
Instances For
A pair of series with vanishing constant coefficient is a legitimate substitution family for
the two variables indexed by Unit ⊕ Unit.
This packages the rintro-and-simpa discharge of hasSubst_of_constantCoeff_zero's hypothesis
for the two-variable case, which is otherwise repeated at every substitution into a two-variable
series.
The substitution sending the coordinate variable i to X and every other coordinate to 0.
Specializing to it separates the coordinate i from all the others: with
ne_of_subst_eq_X_of_subst_eq_zero, two series that this substitution sends to X and to 0
respectively are distinct.
Equations
- MvPowerSeries.coordSpecialize i j = if j = i then PowerSeries.X else 0
Instances For
The coordinate specialization at i is a legitimate substitution family, for an index type of
any size: every image is X or 0, so every constant coefficient vanishes, and the coordinates
carrying a given coefficient all lie in the singleton {i}.
The specialization at i sends the i-th coordinate to X.
The specialization at i kills every other coordinate.
A substitution that sends one series to X and another to 0 separates them: it is how a
distinctness hypothesis is discharged by specializing one coordinate to X and the rest to
0.
MvPowerSeries.aeval_subst for a substitution into a univariate power series: applying a
continuous algebra homomorphism to PowerSeries.subst a f evaluates f at the value of a.
Evaluating the image of a univariate series under PowerSeries.toMvPowerSeries i at a family
a is evaluating the series itself at the entry a i: sending the single variable to the i-th
one and then evaluating is evaluating at a i.
toMvPowerSeries is a substitution, so this is aeval_subst at the family MvPowerSeries.X i;
it is stated for eval₂ rather than aeval because the evaluation of a family is what consumers
hold, and the aeval form would carry the HasEval proof in a position where two propositionally
equal parameters are not definitionally equal.
PowerSeries.eval₂_toMvPowerSeries at the identity ring homomorphism.
The specialization exists so that consumers phrased over RingHom.id need not perform the
normalization themselves. algebraMap R R and RingHom.id R are definitionally equal but not
syntactically so, and algebraMap is not reducible; that is easy to discharge once, as the
simpa below does, but it means the general lemma does not fire as a simp rewrite rule
against a goal phrased over RingHom.id. An evaluation layer whose coefficients and values are
the same ring — what the formal group of a curve over an adic ring needs — is phrased that way
throughout, so it is this form its simp sets can use.