n-th roots of invertible fractional ideals, and the n-th root class map

Let R be a Dedekind domain with fraction field K. FractionalIdealDivisor.Basic identifies the group of invertible fractional ideals of R with the free Weil-divisor group on the height-one primes, by fractionalIdealDivisorAddEquiv. In a free abelian group, an element all of whose coefficients are divisible by n is n times an element, and for n ≠ 0 that element is unique. This file transports that division back to fractional ideals and records what it says about the ideal class group.

Everything below is stated for all n : ℕ, including the degenerate n = 0. There nDivisible R K 0 is the trivial subgroup (divisibility by 0 is vanishing), nthRootHom R K 0 is constantly 1, and the results remain true but say nothing: 1 ^ 0 = 1 is the only instance of nthRootHom_pow.

Main definitions

• nDivisible R K n: the subgroup of invertible fractional ideals all of whose multiplicities FractionalIdeal.count K v are divisible by n.
• nthRootHom R K n: the n-th root homomorphism from nDivisible R K n to the group of invertible fractional ideals. It is built from a private helper performing coefficientwise integer division of the Weil divisor by n; that helper is deliberately not public, since off nDivisible R K n integer division rounds and the value obeys no law worth depending on. Restricting to the subgroup is what makes it multiplicative for n ≠ 0, integer division being additive on multiples of n; for n = 0 it is constant.
• unitsNDivisible R K n: the subgroup of x : Kˣ whose principal fractional ideal (x) lies in nDivisible R K n.
• nthRootClass R K n: the n-th root class map unitsNDivisible R K n →* ClassGroup R, sending u to the ideal class of the n-th root of (u). Its codomain is taken to be the whole class group, with nthRootClass_pow recording that the image lands in the n-torsion.

Main results

• nthRootHom_pow: the n-th root homomorphism is a genuine n-th root — its value raised to the n-th power is the original ideal.
• mem_nDivisible_iff_exists_pow: nDivisible R K n is exactly the subgroup of n-th powers. The forward direction is exists_pow_eq_of_nDivisible — an invertible fractional ideal whose multiplicities are all divisible by n is an n-th power — and the converse is pow_mem_nDivisible, with pow_mem_unitsNDivisible the corresponding statement for Kˣ.
• nthRootClass_pow: every value of the n-th root class map is n-torsion.
• nthRootClass_eq_one_iff: the n-th root class of u is trivial exactly when u is a unit of R times an n-th power in Kˣ.

The last two are the torsion and kernel statements that will become exactness at the middle term of the fundamental sequence 1 → Rˣ/(Rˣ)ⁿ → K(∅, n) → Cl(R)[n] → 1 once the quotients are formed and the codomain is restricted along nthRootClass_pow. Neither step is taken here: this file supplies the n-th root map, the torsion bound and the kernel description, and states no exactness or finiteness result.

These are ingredients for TauCetiRoadmap/EllipticCurves/README.md, Layer 6 (Mordell–Weil), whose weak Mordell–Weil argument needs the Selmer group K(S, n) of Mathlib.RingTheory.DedekindDomain.SelmerGroup to be finite; Mathlib leaves that finiteness as a TODO and the roadmap assigns it to this repository. The finiteness proof is not in this file.

None of the definitions here is @[expose]: the interface is the membership, coefficient and coercion lemmas, not the construction bodies. The characteristic lemmas that hold by definition are therefore written := (rfl), := (Iff.rfl) and := (proof) rather than bare — the parentheses keep the proof elaborating where the definition is still available, which is what lets the bodies stay unexposed. Do not "simplify" them back.

Adapted from Michael Stoll's elliptic-curves formalisation (github.com/MichaelStollBayreuth/EllipticCurves, EllipticCurves/Mathlib/FractionalIdeal.lean at the roadmap's pin 66889eada51a, Apache 2.0, by Michael Stoll). Following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header. The n-th root is built here by dividing the coefficients of a Weil divisor and transporting along fractionalIdealDivisorAddEquiv, where the source builds it from its own ofFinsupp/toFinsupp pair; that pair duplicates the isomorphism this repository already has, so it is not ported.

The n-th root homomorphism

def TauCeti.AlgebraicGeometry.WeilDivisor.nDivisible (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) : Subgroup (FractionalIdeal (nonZeroDivisors R) K)ˣ

The subgroup of invertible fractional ideals all of whose multiplicities are divisible by n, equivalently those whose Weil divisor is n times a divisor.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.mem_nDivisible {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {n : ℕ} {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ} : I ∈ nDivisible R K n ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), ↑n ∣ FractionalIdeal.count K v ↑I

Membership in nDivisible R K n is divisibility of every multiplicity by n.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.pow_mem_nDivisible (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) (J : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : J ^ n ∈ nDivisible R K n

An n-th power is n-divisible: every multiplicity of J ^ n is n times one of J. This is the introduction rule for nDivisible R K n, converse to exists_pow_eq_of_nDivisible.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.nthRootHom (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) : ↥(nDivisible R K n) →* (FractionalIdeal (nonZeroDivisors R) K)ˣ

The n-th root homomorphism: on the subgroup of ideals whose multiplicities are all divisible by n, dividing every multiplicity by n is a group homomorphism. For n ≠ 0 the restriction is what makes this multiplicative, integer division being additive on multiples of n and not in general; for n = 0 the map is constantly 1 and the subgroup is trivial.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.count_nthRootHom {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) (I : ↥(nDivisible R K n)) (v : IsDedekindDomain.HeightOneSpectrum R) : FractionalIdeal.count K v ↑((nthRootHom R K n) I) = FractionalIdeal.count K v ↑↑I / ↑n

The multiplicities of the n-th root are those of I, divided by n. Together with units_eq_of_forall_count_eq this determines nthRootHom completely, so no lemma below needs to unfold it.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.nthRootHom_pow (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) (I : ↥(nDivisible R K n)) : (nthRootHom R K n) I ^ n = ↑I

The n-th root homomorphism is a genuine n-th root: raising its value to the n-th power returns the original ideal.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.exists_pow_eq_of_nDivisible (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ} (hI : I ∈ nDivisible R K n) : ∃ (J : (FractionalIdeal (nonZeroDivisors R) K)ˣ), J ^ n = I

n-th roots of invertible fractional ideals. An invertible fractional ideal all of whose multiplicities are divisible by n is an n-th power.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.mem_nDivisible_iff_exists_pow {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {n : ℕ} {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ} : I ∈ nDivisible R K n ↔ ∃ (J : (FractionalIdeal (nonZeroDivisors R) K)ˣ), J ^ n = I

nDivisible R K n is exactly the subgroup of n-th powers. Combining exists_pow_eq_of_nDivisible with its converse pow_mem_nDivisible.

The n-th root class map

def TauCeti.AlgebraicGeometry.WeilDivisor.unitsNDivisible (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) : Subgroup Kˣ

The subgroup of those x : Kˣ whose principal fractional ideal (x) has all multiplicities divisible by n. These are exactly the elements for which an n-th root of (x) exists, so they are exactly the elements the n-th root class map is defined on.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.unitsNDivisible R K n = Subgroup.comap (toPrincipalIdeal R K) (TauCeti.AlgebraicGeometry.WeilDivisor.nDivisible R K n)

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.mem_unitsNDivisible {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {n : ℕ} {u : Kˣ} : u ∈ unitsNDivisible R K n ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), ↑n ∣ FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors R) ↑u)

Membership in unitsNDivisible R K n is divisibility by n of every multiplicity of the principal fractional ideal generated by u.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.pow_mem_unitsNDivisible (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) (w : Kˣ) : w ^ n ∈ unitsNDivisible R K n

An n-th power of a unit of K lies in unitsNDivisible R K n: the introduction rule, and the reason the subgroup contains the n-th powers that the quotient Kˣ/(Kˣ)ⁿ divides out.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.unitsNDivisibleToNDivisible (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) : ↥(unitsNDivisible R K n) →* ↥(nDivisible R K n)

The principal-ideal map restricted to unitsNDivisible R K n, with codomain cut down to the subgroup nDivisible R K n that it lands in by definition.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.coe_unitsNDivisibleToNDivisible (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) (u : ↥(unitsNDivisible R K n)) : ↑((unitsNDivisibleToNDivisible R K n) u) = (toPrincipalIdeal R K) ↑u

Underneath the codomain restriction, unitsNDivisibleToNDivisible is toPrincipalIdeal.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.nthRootClass (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) : ↥(unitsNDivisible R K n) →* ClassGroup R

The n-th root class map: send u : Kˣ whose principal ideal (u) is n-divisible to the ideal class of the n-th root of (u). This is the map that becomes the right-hand map of 1 → Rˣ/(Rˣ)ⁿ → K(∅, n) → Cl(R)[n] → 1 once quotients are formed and the codomain is cut down to the n-torsion; here it is taken with its full codomain ClassGroup R.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.nthRootClass_apply (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) (u : ↥(unitsNDivisible R K n)) : (nthRootClass R K n) u = (ClassGroup.mk K) ((nthRootHom R K n) ((unitsNDivisibleToNDivisible R K n) u))

The n-th root class map is the class of the n-th root of the principal ideal, by definition.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.nthRootClass_pow (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) (u : ↥(unitsNDivisible R K n)) : (nthRootClass R K n) u ^ n = 1

Every value of the n-th root class map is n-torsion. The n-th power of the class of the n-th root of (u) is the class of (u) itself, which is trivial because (u) is principal. This is what lets a consumer cut the codomain down to the n-torsion of ClassGroup R.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.nthRootClass_eq_one_iff (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {n : ℕ} (u : ↥(unitsNDivisible R K n)) : (nthRootClass R K n) u = 1 ↔ ∃ (a : Rˣ) (w : Kˣ), (Units.map ↑(algebraMap R K)) a * w ^ n = ↑u

The kernel of the n-th root class map. The n-th root class of u is trivial exactly when u is a unit of R times an n-th power in Kˣ. Passing to quotients, this is what will give exactness at the middle term of 1 → Rˣ/(Rˣ)ⁿ → K(∅, n) → Cl(R)[n] → 1; the quotients are not formed here.