The field factors of K[X] ⧸ (f) and its square classes

For f a nonzero squarefree polynomial over a field K, the Chinese Remainder Theorem identifies K[X] ⧸ (f) with the product of the fields K[X] ⧸ (p) over the distinct monic irreducible factors p of f (Polynomial.Factors f). This file records that decomposition, the projections onto the factors, and the induced decomposition of the group of n-th power classes of units — the group underlying the 2-Selmer group of an étale algebra.

Throughout, the group of n-th power classes of units of a commutative monoid α is spelled as the quotient αˣ ⧸ (powMonoidHom n).range, matching Mathlib.RingTheory.DedekindDomain.SelmerGroup; the transport of that quotient along an equivalence and its compatibility with products are in TauCeti.GroupTheory.QuotientGroup.PowMonoidHom.

Main definitions

• AdjoinRoot.equivPiFactors: K[X] ⧸ (f) ≃ₐ[K] Π p, K[X] ⧸ (p).
• AdjoinRoot.projFactor: the projection onto the factor K[X] ⧸ (p), as a K-algebra map.
• AdjoinRoot.modPowEquivPiFactors: the n-th power classes of units of K[X] ⧸ (f) are the product of those of its field factors.

Main results

• AdjoinRoot.isSeparable_of_separable: each field factor is a separable extension of K when f is separable — the hypothesis IsIntegralClosure.isDedekindDomain needs.
• AdjoinRoot.modPow_mk_eq_one_iff_forall_factors: a class of units is trivial exactly when all its components at the field factors are.

Implementation notes

equivPiFactors_mk and projFactor_mk hold by rfl, written (rfl): the parenthesised form is elaborated in this module, where the definitions it unfolds are visible, whereas a bare rfl proof of an exported statement would ask for those definitions to be exposed downstream.

Roadmap

TauCetiRoadmap/EllipticCurves/README.md, Layer 6 (Mordell–Weil): the 2-descent map of the weak Mordell–Weil theorem lands in the square classes of K[X] ⧸ (f) for f the Weierstrass cubic, and is controlled one field factor at a time; modPowEquivPiFactors and modPow_mk_eq_one_iff_forall_factors are what let a statement about the classes be checked componentwise. Nothing here mentions a curve.

Provenance

Adapted, with the author's proofs, 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, section EtaleDecomposition. The source abbreviates the group of n-th power classes as Units.modPow; here it is the quotient directly. The source is written against Lean v4.32.0; this is a forward port.

The field factors of K[X] ⧸ (f)

instance AdjoinRoot.instFactIrreducible {K : Type u_1} [Field K] {f : Polynomial K} (p : f.Factors) : Fact (Irreducible ↑p)

instance AdjoinRoot.instFiniteDimensional {K : Type u_1} [Field K] {f : Polynomial K} (p : f.Factors) : FiniteDimensional K (AdjoinRoot ↑p)

theorem AdjoinRoot.minpoly_root_factor {K : Type u_1} [Field K] {f : Polynomial K} (p : f.Factors) : minpoly K (root ↑p) = ↑p

theorem AdjoinRoot.isSeparable_of_separable {K : Type u_1} [Field K] {f : Polynomial K} (hf : f.Separable) (p : f.Factors) : Algebra.IsSeparable K (AdjoinRoot ↑p)

If f is separable, then each field factor of K[X] ⧸ (f) is a separable extension of K. This is what IsIntegralClosure.isDedekindDomain needs.

noncomputable def AdjoinRoot.equivPiFactors {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0) (hsq : Squarefree f) : AdjoinRoot f ≃ₐ[K] (p : f.Factors) → AdjoinRoot ↑p

Chinese Remainder Theorem for AdjoinRoot: for f nonzero and squarefree, K[X] ⧸ (f) is the product of the fields K[X] ⧸ (p) over the monic irreducible factors p of f.

Equations

• AdjoinRoot.equivPiFactors hf hsq = AlgEquiv.ofRingEquiv ⋯

@[simp]

theorem AdjoinRoot.equivPiFactors_mk {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0) (hsq : Squarefree f) (q : Polynomial K) (p : f.Factors) : (equivPiFactors hf hsq) ((mk f) q) p = (mk ↑p) q

noncomputable def AdjoinRoot.projFactor {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0) (hsq : Squarefree f) (p : f.Factors) : AdjoinRoot f →ₐ[K] AdjoinRoot ↑p

The projection of K[X] ⧸ (f) onto the field factor K[X] ⧸ (p), as a K-algebra map.

Equations

• AdjoinRoot.projFactor hf hsq p = (Pi.evalAlgHom K (fun (i : f.Factors) => AdjoinRoot ↑i) p).comp ↑(AdjoinRoot.equivPiFactors hf hsq)

@[simp]

theorem AdjoinRoot.projFactor_mk {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0) (hsq : Squarefree f) (q : Polynomial K) (p : f.Factors) : (projFactor hf hsq p) ((mk f) q) = (mk ↑p) q

Square classes, and n-th power classes, of the factors

noncomputable def AdjoinRoot.modPowEquivPiFactors {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0) (hsq : Squarefree f) (n : ℕ) : (AdjoinRoot f)ˣ ⧸ (powMonoidHom n).range ≃* ((p : f.Factors) → (AdjoinRoot ↑p)ˣ ⧸ (powMonoidHom n).range)

The n-th power classes of units of K[X] ⧸ (f) are the product of those of its field factors.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AdjoinRoot.modPowEquivPiFactors_mk {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0) (hsq : Squarefree f) (n : ℕ) (u : (AdjoinRoot f)ˣ) (p : f.Factors) : (modPowEquivPiFactors hf hsq n) (↑u) p = ↑((Units.map ↑(projFactor hf hsq p).toRingHom) u)

On the class of a unit, modPowEquivPiFactors is componentwise projection to the factors.

theorem AdjoinRoot.modPowEquivPiFactors_unit {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0) (hsq : Squarefree f) (n : ℕ) {a : AdjoinRoot f} (ha : IsUnit a) (p : f.Factors) : (modPowEquivPiFactors hf hsq n) (↑ha.unit) p = ↑⋯.unit

On the class of a unit, modPowEquivPiFactors is componentwise projection to the factors (IsUnit.unit version of modPowEquivPiFactors_mk).

theorem AdjoinRoot.modPow_mk_eq_one_iff_forall_factors {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0) (hsq : Squarefree f) (n : ℕ) (u : (AdjoinRoot f)ˣ) : ↑u = 1 ↔ ∀ (p : f.Factors), ↑((Units.map ↑(projFactor hf hsq p).toRingHom) u) = 1

The class of a unit of K[X] ⧸ (f) is trivial exactly when its components at all field factors are trivial.