Complements on AdjoinRoot

Mathlib's AdjoinRoot.map sends a ring homomorphism f : R →+* S, together with a divisibility q ∣ p.map f, to a ring homomorphism AdjoinRoot p →+* AdjoinRoot q. It records the action on AdjoinRoot.of and on AdjoinRoot.root (map_of, map_root) but not the action on the class of a general polynomial, and says nothing about surjectivity. Both are added here, together with the description of the R-linear endomorphisms of AdjoinRoot g, for g monic, that commute with multiplication by the root, and the annihilators of the powers of the root in the truncated polynomial ring R[X]/(X ^ n).

Main results

• AdjoinRoot.map_mk: the map sends the class of x to the class of x.map f. Mathlib states this only in the specialised form WeierstrassCurve.Affine.CoordinateRing.map_mk. Marked @[simp], like its neighbours AdjoinRoot.map_of and AdjoinRoot.map_root.
• AdjoinRoot.map_surjective: the map is surjective when f is.
• AdjoinRoot.exists_degree_lt_mk_eq, AdjoinRoot.mk_eq_mk_iff_of_degree_lt: for a monic relator, every class is represented by a polynomial of degree less than that of the relator, and that representative is unique. Mathlib has division with remainder by a monic polynomial but does not record what it says about AdjoinRoot.
• AdjoinRoot.eq_mulRight_of_root_mul: an R-linear endomorphism of AdjoinRoot g, for g monic, that commutes with multiplication by the root is multiplication by its value at 1. Its consumers are the truncated polynomial algebras of TauCeti.RepresentationTheory.Quiver.OneLoop.FiniteRepType and TauCeti.RepresentationTheory.Quiver.Kronecker.FiniteRepType, whose endomorphism algebras it pins down, but nothing beyond monicity of the relator enters the proof.
• AdjoinRoot.root_X_pow_pow_mul_eq_zero_iff: in the truncated polynomial ring R[X]/(X ^ n), for i ≤ n, the annihilator of x ^ i is generated by x ^ (n - i), where x is the root.
• AdjoinRoot.finrank_quotient_span_root_X_pow_pow: for p ≤ n and R nontrivial, the quotient of R[X]/(X ^ n) by x ^ p has rank p.
• AdjoinRoot.finrank_quotient_span_op_root_X_pow_pow, AdjoinRoot.finrank_quotient_map_mkQ_span_op_root_X_pow_pow: the same count for the cyclic right modules M_j, the quotients of the opposite ring by op (x ^ j), and the quotient of M_j by the image of x ^ m, which has rank min j m.

Stated over arbitrary commutative rings.

This is consumed by TauCeti/AlgebraicGeometry/EllipticCurve/Affine/CoordinateRingMap.lean, which specialises it to the coordinate ring of a Weierstrass curve for the Hasse strand of TauCetiRoadmap/EllipticCurves/README.md, Layer 3.

Provenance

The surjectivity argument — lift a class to a polynomial, then lift that polynomial along f — is adapted from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, pinned by that roadmap at dev/hasse-weil @ 513e83879e2f), HasseWeil/WeilPairing/FrobeniusFunctionFieldEquiv.lean, declaration coordRingMap_bijective. There it is carried out for the coordinate ring of a Weierstrass curve and only for a base ring equivalence; here it is stated for AdjoinRoot.map along any surjective base homomorphism, with map_mk — which the source does not isolate — extracted as the step that makes it routine. AdjoinRoot.exists_degree_lt_mk_eq and AdjoinRoot.mk_eq_mk_iff_of_degree_lt are adapted from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, pinned by TauCetiRoadmap/EllipticCurves/README.md at 66889eada51a), EllipticCurves/Mathlib/Basic.lean. There the reduction step the first one uses is a separate lemma; here that step is Mathlib's AdjoinRoot.mk_leftInverse. The source proves the second from a named helper eq_zero_of_monic_dvd_of_degree_lt; that helper is a one-line composition of Mathlib's Polynomial.modByMonic_eq_self_iff and Polynomial.modByMonic_eq_zero_iff_dvd, so it is inlined here rather than re-declared. They are harvested here rather than in the file that consumes them because nothing about elliptic curves enters either statement.

@[simp]

theorem AdjoinRoot.map_mk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} {p : Polynomial R} {q : Polynomial S} (h : q ∣ Polynomial.map f p) (x : Polynomial R) : (map f p q h) ((mk p) x) = (mk q) (Polynomial.map f x)

AdjoinRoot.map on the class of a polynomial is the class of its image. Mathlib states this for WeierstrassCurve.Affine.CoordinateRing.map but not for the underlying AdjoinRoot.map.

theorem AdjoinRoot.map_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Surjective ⇑f) {p : Polynomial R} {q : Polynomial S} (h : q ∣ Polynomial.map f p) : Function.Surjective ⇑(map f p q h)

AdjoinRoot.map is surjective when the base map is.

theorem AdjoinRoot.exists_degree_lt_mk_eq {R : Type u_1} [CommRing R] [Nontrivial R] {g : Polynomial R} (hg : g.Monic) (a : AdjoinRoot g) : ∃ (p : Polynomial R), p.degree < g.degree ∧ a = (mk g) p

Every class in AdjoinRoot g, for g monic, is represented by a polynomial of degree less than deg g. Division with remainder by a monic polynomial supplies the representative.

theorem AdjoinRoot.mk_eq_mk_iff_of_degree_lt {R : Type u_1} [CommRing R] [Nontrivial R] {g : Polynomial R} (hg : g.Monic) {p q : Polynomial R} (hp : p.degree < g.degree) (hq : q.degree < g.degree) : (mk g) p = (mk g) q ↔ p = q

Two polynomials of degree less than that of a monic relator have the same class in AdjoinRoot only if they are equal. Together with AdjoinRoot.exists_degree_lt_mk_eq this says that the polynomials of degree < deg g are a set of unique representatives.

theorem AdjoinRoot.eq_mulRight_of_root_mul {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) {f : AdjoinRoot g →ₗ[R] AdjoinRoot g} (hf : ∀ (x : AdjoinRoot g), f (root g * x) = root g * f x) : f = LinearMap.mulRight R (f 1)

An R-linear endomorphism of AdjoinRoot g commuting with multiplication by the root is multiplication by its value at 1. It commutes with multiplication by every power of the root, and for a monic relator those powers are a basis (AdjoinRoot.powerBasis').

theorem AdjoinRoot.root_X_pow_pow_mul_eq_zero_iff {R : Type u_1} [CommRing R] {n i : ℕ} (hi : i ≤ n) (c : AdjoinRoot (Polynomial.X ^ n)) : root (Polynomial.X ^ n) ^ i * c = 0 ↔ root (Polynomial.X ^ n) ^ (n - i) ∣ c

The annihilator of x ^ i in R[X]/(X ^ n) is generated by x ^ (n - i), for i ≤ n and x the class of X: x ^ i * c = 0 exactly when x ^ (n - i) divides c. Thus x ^ i and x ^ (n - i) each generate the annihilator of the other.

theorem AdjoinRoot.finrank_quotient_span_root_X_pow_pow {R : Type u_1} [CommRing R] [Nontrivial R] {n p : ℕ} (hp : p ≤ n) : Module.finrank R (AdjoinRoot (Polynomial.X ^ n) ⧸ Ideal.span {root (Polynomial.X ^ n) ^ p}) = p

The quotient of R[X]/(X ^ n) by x ^ p has rank p, for p ≤ n and x the class of X. This quotient is R[X]/(X ^ p).

theorem AdjoinRoot.finrank_quotient_span_op_root_X_pow_pow {R : Type u_1} [CommRing R] [Nontrivial R] {n p : ℕ} (hp : p ≤ n) : Module.finrank R ((AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ ⧸ Ideal.span {MulOpposite.op (root (Polynomial.X ^ n) ^ p)}) = p

The quotient of the opposite of R[X]/(X ^ n) by op (x ^ p) has rank p, for p ≤ n and x the class of X. This is the form in which the quotient appears as a cyclic right module over R[X]/(X ^ n).

theorem AdjoinRoot.finrank_quotient_map_mkQ_span_op_root_X_pow_pow {R : Type u_1} [CommRing R] [Nontrivial R] {n j : ℕ} (hj : j ≤ n) (m : ℕ) : Module.finrank R (((AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ ⧸ Ideal.span {MulOpposite.op (root (Polynomial.X ^ n) ^ j)}) ⧸ Submodule.restrictScalars R (Submodule.map (Submodule.mkQ (Ideal.span {MulOpposite.op (root (Polynomial.X ^ n) ^ j)})) (Ideal.span {MulOpposite.op (root (Polynomial.X ^ n) ^ m)}))) = min j m

The quotient of M_j by the image of x ^ m has rank min j m, where M_j is the quotient of the opposite of R[X]/(X ^ n) by op (x ^ j), for j ≤ n and x the class of X. This quotient is M_(min j m).