Material for Mathlib

Source: MichaelStollBayreuth/EllipticCurves at commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f. Exact-pin changes are documented in PORTING.md.

This file collects the general-purpose results developed for EllipticCurves.WeakMordellWeil that have nothing to do with elliptic curves and look like candidates for Mathlib.

• MonoidHom.ofMapMulMulEqOne: build a MonoidHom from f 1 = 1 and a * b * c = 1 → f a * f b * f c = 1.
• Valuation.map_eval_eq_of_one_lt and Valuation.le_one_of_root_monic: dominance of the leading term of a monic polynomial with integral coefficients, and integrality of its roots. Valuation.eq_one_of_mul_eq_one: a factor of a unit is a unit, provided both factors are integral.
• IsDedekindDomain.HeightOneSpectrum.finite_setOf_valuation_ne_one, .below (the prime lying below a prime of an integral extension), .primesAbove and its finiteness .primesAbove_finite, IsDedekindDomain.selmerGroupAbove, .valuationOfNeZero_eq_iff, .dvd_toAdd_valuationOfNeZero and .valuationOfNeZeroMod_mk_eq_one_iff, which turns the Selmer condition into a divisibility of valuations; Set.integer_mono and Set.unit_mono, monotonicity of the S-integers and S-units in S. (Mathlib.RingTheory.DedekindDomain.SelmerGroup has a TODO about the Multiplicative/Additive defeq abuse in valuationOfNeZeroMod and provides no API for it.)
• Units.modPow, the group of n-th power classes of units, which Mathlib.RingTheory.DedekindDomain.SelmerGroup has only as a local notation, together with map, congr and piEquiv.
• Division with remainder by a monic polynomial: Polynomial.Monic.divByMonic_mul_add, .modByMonic_mul_add, modByMonic_mem_degreeLT, divByMonic_mem_degreeLT.
• isIntegralClosure_int_integralClosure, NumberField.finite_classGroup_integralClosure and NumberField.fg_units_integralClosure: the class number theorem and the finite generation of the unit group for the integral closure of 𝓞 K in a finite extension of a number field K; NumberField.subsingleton_classGroup_integralClosure and NumberField.finrank_additive_units_integralClosure transport triviality of the class group and the unit rank from 𝓞 L.
• AdjoinRoot.discr_powerBasis_eq_discr, NumberField.exists_eq_discr_mul_sq, RingOfIntegers.isPrincipalIdealRing_of_finrank_eq_three_of_abs_discr_le and RingOfIntegers.finrank_additive_units_of_discr_neg/_pos: the discriminant of the power basis of K[X]/(f) is f.discr; the field discriminant is any integral power-basis discriminant divided by a square; a cubic field with |discr| ≤ 49 has trivial class group (Minkowski bound), and the sign of its discriminant determines the unit rank (Dirichlet).
• AdjoinRoot.norm_mk_eq_resultant: for monic g, the norm of AdjoinRoot.mk g p is the resultant of g and p. This links Polynomial.resultant to Algebra.norm.
• AdjoinRoot.equivPiFactors: for nonzero squarefree f, K[X]/(f) is the product of the fields K[X]/(p) over the monic irreducible factors p of f, and the induced AdjoinRoot.modPowEquivPiFactors on n-th power classes of units.
• Polynomial.discr_X_sub_C_mul: splitting off a linear factor multiplies the discriminant by the square of the evaluation, ((X - C x) * g).discr = g.discr * g.eval x ^ 2.
• Matrix.det_blockDiagonal', LinearMap.det_pi', Algebra.norm_prod, Algebra.norm_pi: determinants and norms on (dependent) products decompose as products; together with AdjoinRoot.norm_eq_prod_norm_projFactor, the norm on K[X]/(f) as the product of the norms on the field factors.
• General helpers extracted from the rank example: Squarefree.map (transport along a MulEquiv), Polynomial.Monic.irreducible_map_fraction_map_of_irreducible_map (irreducibility over the fraction field via reduction modulo a prime), Polynomial.Factors.coe_eq, AdjoinRoot.isIntegralElem_root_of_map, AdjoinRoot.finrank_eq_natDegree, and the IsPrincipalIdealRing (𝓞 ℚ) instance.

def MonoidHom.ofMapMulMulEqOne {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf₁ : f 1 = 1) (hf : ∀ (a b c : G), a * b * c = 1 → f a * f b * f c = 1) : G →* H

A map f between groups with f 1 = 1 that sends triples with product 1 to triples with product 1 is a homomorphism. Useful when a map is naturally defined via a symmetric ternary relation, like collinearity on a cubic curve.

Equations

• MonoidHom.ofMapMulMulEqOne hf₁ hf = MonoidHom.ofMapMulInv f ⋯

def AddMonoidHom.ofMapAddAddEqZero {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf₁ : f 0 = 0) (hf : ∀ (a b c : G), a + b + c = 0 → f a + f b + f c = 0) : G →+ H

A map f between additive groups with f 0 = 0 that sends triples with sum 0 to triples with sum 0 is a homomorphism. Useful when a map is naturally defined via a symmetric ternary relation, like collinearity on a cubic curve.

Equations

• AddMonoidHom.ofMapAddAddEqZero hf₁ hf = AddMonoidHom.ofMapAddNeg f ⋯

@[simp]

theorem MonoidHom.coe_ofMapMulMulEqOne {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf₁ : f 1 = 1) (hf : ∀ (a b c : G), a * b * c = 1 → f a * f b * f c = 1) : ⇑(ofMapMulMulEqOne hf₁ hf) = f

@[simp]

theorem AddMonoidHom.coe_ofMapAddAddEqZero {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf₁ : f 0 = 0) (hf : ∀ (a b c : G), a + b + c = 0 → f a + f b + f c = 0) : ⇑(ofMapAddAddEqZero hf₁ hf) = f

theorem Subgroup.finite_comap_of_injective {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G →* H} (hf : Function.Injective ⇑f) (S : Subgroup H) [Finite ↥S] : Finite ↥(comap f S)

The preimage of a finite subgroup under an injective group homomorphism is finite.

theorem AddSubgroup.finite_comap_of_injective {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G →+ H} (hf : Function.Injective ⇑f) (S : AddSubgroup H) [Finite ↥S] : Finite ↥(comap f S)

instance Subgroup.instFinitePi {ι : Type u_3} [Finite ι] {G : ι → Type u_4} [(i : ι) → Group (G i)] {S : (i : ι) → Subgroup (G i)} [∀ (i : ι), Finite ↥(S i)] : Finite ↥(pi Set.univ S)

A product of finitely many finite subgroups is finite.

instance AddSubgroup.instFinitePi {ι : Type u_3} [Finite ι] {G : ι → Type u_4} [(i : ι) → AddGroup (G i)] {S : (i : ι) → AddSubgroup (G i)} [∀ (i : ι), Finite ↥(S i)] : Finite ↥(pi Set.univ S)

theorem IsUnit.exists_pow_eq_unit_iff {α : Type u_1} [Monoid α] {a : α} (h : IsUnit a) (n : ℕ) : (∃ (x : αˣ), x ^ n = h.unit) ↔ ∃ (x : α), x ^ n = a

theorem IsAddUnit.exists_nsmul_eq_addUnit_iff {α : Type u_1} [AddMonoid α] {a : α} (h : IsAddUnit a) (n : ℕ) : (∃ (x : AddUnits α), n • x = h.addUnit) ↔ ∃ (x : α), n • x = a

theorem Squarefree.map {α : Type u_1} [Monoid α] {β : Type u_2} [Monoid β] (e : α ≃* β) {r : α} (h : Squarefree r) : Squarefree (e r)

A multiplicative equivalence preserves squarefreeness.

theorem IsAlgClosed.of_ringEquiv' {k : Type u_1} {K : Type u_2} [Field k] [Field K] [IsAlgClosed k] (e : k ≃+* K) : IsAlgClosed K

Algebraic closedness transfers along a ring isomorphism. This is IsAlgClosed.of_ringEquiv without its restriction of both fields to a common universe (needed e.g. to transfer IsAlgClosed ℂ to a completion of a number field F : Type* at a complex place).

@[reducible, inline]

abbrev Units.modPow (α : Type u_1) [CommMonoid α] (n : ℕ) : Type u_1

The group of n-th power classes of units of α. This is the group underlying the Selmer groups of Mathlib.RingTheory.DedekindDomain.SelmerGroup, where it only exists as a local notation.

Equations

• Units.modPow α n = (αˣ ⧸ (powMonoidHom n).range)

def QuotientGroup.congrRangePowMonoidHom {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] (e : G ≃* H) (n : ℕ) : G ⧸ (powMonoidHom n).range ≃* H ⧸ (powMonoidHom n).range

A multiplicative equivalence of commutative groups induces one on the quotients by the subgroups of n-th powers.

Equations

• QuotientGroup.congrRangePowMonoidHom e n = QuotientGroup.congr (powMonoidHom n).range (powMonoidHom n).range e ⋯

theorem Units.modPow.unit_eq_one_iff {α : Type u_1} [CommMonoid α] {a : α} (ha : IsUnit a) (n : ℕ) : ↑ha.unit = 1 ↔ ∃ (z : α), z ^ n = a

theorem Units.modPow.unit_mul_unit_mul_unit_eq_one_iff {α : Type u_1} [CommMonoid α] {a b c : α} (ha : IsUnit a) (hb : IsUnit b) (hc : IsUnit c) (n : ℕ) : ↑ha.unit * ↑hb.unit * ↑hc.unit = 1 ↔ ∃ (z : α), z ^ n = a * b * c

theorem Units.modPow.mk_eq_one_iff {α : Type u_1} [CommMonoid α] {u : αˣ} (n : ℕ) : ↑u = 1 ↔ ∃ (w : αˣ), w ^ n = u

theorem Units.modPow.mk_eq_mk_iff {α : Type u_1} [CommMonoid α] {u v : αˣ} (n : ℕ) : ↑u = ↑v ↔ ∃ (w : αˣ), v = u * w ^ n

theorem Units.modPow.mk_eq_one_iff_isSquare {α : Type u_1} [CommMonoid α] {u : αˣ} : ↑u = 1 ↔ IsSquare ↑u

The class of a unit is trivial in Units.modPow α 2 exactly when the unit is a square in α.

@[simp]

theorem Units.modPow.pow_eq_one {α : Type u_1} [CommMonoid α] {n : ℕ} (m : modPow α n) : m ^ n = 1

theorem Units.modPow.subsingleton_of_forall_exists_pow {α : Type u_1} [CommMonoid α] {n : ℕ} (h : ∀ (u : αˣ), ∃ (w : αˣ), w ^ n = u) : Subsingleton (modPow α n)

If every unit of α is an n-th power, then the group of n-th power classes of units is trivial.

theorem Units.modPow.subsingleton_of_isAlgClosed (K : Type u_3) [Field K] [IsAlgClosed K] {n : ℕ} (hn : n ≠ 0) : Subsingleton (modPow K n)

Over an algebraically closed field, the group of n-th power classes of units is trivial (for n ≠ 0).

def Units.modPow.map {α : Type u_1} {β : Type u_2} [CommMonoid α] [CommMonoid β] (φ : α →* β) (n : ℕ) : modPow α n →* modPow β n

A monoid homomorphism α →* β induces a homomorphism on n-th power classes of units.

Equations

• Units.modPow.map φ n = QuotientGroup.map (powMonoidHom n).range (powMonoidHom n).range (Units.map φ) ⋯

@[simp]

theorem Units.modPow.map_mk {α : Type u_1} {β : Type u_2} [CommMonoid α] [CommMonoid β] (φ : α →* β) (n : ℕ) (u : αˣ) : (map φ n) ↑u = ↑((Units.map φ) u)

@[simp]

theorem Units.modPow.map_id {α : Type u_1} [CommMonoid α] (n : ℕ) : map (MonoidHom.id α) n = MonoidHom.id (modPow α n)

theorem Units.modPow.map_comp {α : Type u_1} {β : Type u_2} [CommMonoid α] [CommMonoid β] {γ : Type u_3} [CommMonoid γ] (ψ : β →* γ) (φ : α →* β) (n : ℕ) : (map ψ n).comp (map φ n) = map (ψ.comp φ) n

theorem Units.modPow.map_unit {α : Type u_1} {β : Type u_2} [CommMonoid α] [CommMonoid β] {a : α} (φ : α →* β) (n : ℕ) (ha : IsUnit a) : (map φ n) ↑ha.unit = ↑⋯.unit

def Units.modPow.congr {α : Type u_1} {β : Type u_2} [CommMonoid α] [CommMonoid β] (e : α ≃* β) (n : ℕ) : modPow α n ≃* modPow β n

A multiplicative equivalence α ≃* β induces one on n-th power classes of units.

Equations

• Units.modPow.congr e n = QuotientGroup.congrRangePowMonoidHom (Units.mapEquiv e) n

theorem Units.modPow.subsingleton_of_isAlgClosed_of_isIntegral (k : Type u_3) (K : Type u_4) [Field k] [IsAlgClosed k] [CommRing K] [IsDomain K] [Algebra k K] [Algebra.IsIntegral k K] {n : ℕ} (hn : n ≠ 0) : Subsingleton (modPow K n)

The group of n-th power classes of units of a domain that is integral over an algebraically closed field is trivial (for n ≠ 0) — the algebra map is then bijective, so this extends Units.modPow.subsingleton_of_isAlgClosed; e.g., it applies to the residue fields L[X]/(p) of an étale algebra over an algebraically closed field.

theorem Units.modPow.bijective_map {α : Type u_1} {β : Type u_2} [CommMonoid α] [CommMonoid β] {φ : α →* β} (hφ : Function.Bijective ⇑φ) (n : ℕ) : Function.Bijective ⇑(map φ n)

The map on n-th power classes of units induced by a bijective homomorphism is bijective.

noncomputable def Units.modPow.piEquiv {ι : Type u_3} (α : ι → Type u_4) [(i : ι) → CommMonoid (α i)] (n : ℕ) : modPow ((i : ι) → α i) n ≃* ((i : ι) → modPow (α i) n)

Taking n-th power classes of units commutes with products.

Equations

• Units.modPow.piEquiv α n = (QuotientGroup.congrRangePowMonoidHom MulEquiv.piUnits n).trans (QuotientGroup.mulEquivPiModRangePowMonoidHom (fun (i : ι) => (α i)ˣ) n)

@[simp]

theorem Units.modPow.piEquiv_mk {ι : Type u_3} (α : ι → Type u_4) [(i : ι) → CommMonoid (α i)] (n : ℕ) (u : ((i : ι) → α i)ˣ) (i : ι) : (piEquiv α n) (↑u) i = ↑(MulEquiv.piUnits u i)

theorem Ideal.comap_ne_bot_of_comap_comap_ne_bot {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] {ρ : R →+* S} {φ : S →+* T} (hρ : Function.Injective ⇑ρ) {I : Ideal T} (h : comap ρ (comap φ I) ≠ ⊥) : comap φ I ≠ ⊥

An ideal contraction is nonzero as soon as its further contraction along an injective ring homomorphism is nonzero.

theorem linearIndependent_of_diagonal {ι : Type u_1} {A : Type u_2} [CommRing A] [NoZeroDivisors A] {u : ι → ι → A} (hd : ∀ (i : ι), u i i ≠ 0) (ho : ∀ (i j : ι), j ≠ i → u i j = 0) : LinearIndependent A u

A "diagonal" family of vectors — supported at the family index with nonzero value there — is linearly independent.

theorem Matrix.det_blockDiagonal' {ι : Type u_1} [Fintype ι] [DecidableEq ι] {η : ι → Type u_2} [(i : ι) → Fintype (η i)] [(i : ι) → DecidableEq (η i)] {R : Type u_3} [CommRing R] (M : (i : ι) → Matrix (η i) (η i) R) : (blockDiagonal' M).det = ∏ i : ι, (M i).det

The determinant of a block diagonal matrix with (possibly) non-uniform block sizes is the product of the determinants of the blocks. Dependent version of Matrix.det_blockDiagonal.

theorem LinearMap.det_pi' {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] {S : ι → Type u_3} [(i : ι) → AddCommGroup (S i)] [(i : ι) → Module R (S i)] [∀ (i : ι), Module.Free R (S i)] [∀ (i : ι), Module.Finite R (S i)] (f : (i : ι) → S i →ₗ[R] S i) : LinearMap.det (pi fun (i : ι) => f i ∘ₗ proj i) = ∏ i : ι, LinearMap.det (f i)

The determinant of a component-wise endomorphism of a finite product of finite free modules is the product of the determinants of the components. Dependent version of LinearMap.det_pi.

theorem Valuation.map_natCast_le_one {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {R : Type u_3} [Ring R] (ν : Valuation R Γ) (n : ℕ) : ν ↑n ≤ 1

theorem Valuation.eq_one_of_mul_eq_one {L : Type u_1} {Γ : Type u_2} [CommRing L] [LinearOrderedCommGroupWithZero Γ] (ν : Valuation L Γ) {a b : L} (ha : ν a ≤ 1) (hb : ν b ≤ 1) (hab : ν (a * b) = 1) : ν a = 1

If a product of two integral elements is a unit, then each factor is a unit.

theorem Valuation.map_eval_eq_of_one_lt {L : Type u_1} {Γ : Type u_2} [CommRing L] [LinearOrderedCommGroupWithZero Γ] (ν : Valuation L Γ) {t : L} {p : Polynomial L} (hp : p.Monic) (hcoeff : ∀ i < p.natDegree, ν (p.coeff i) ≤ 1) (ht : 1 < ν t) : ν (Polynomial.eval t p) = ν t ^ p.natDegree

If p is monic with coefficients that are integral for the valuation ν and 1 < ν t, then the value of p at t is dominated by the leading term: ν (p.eval t) = ν t ^ p.natDegree. In particular, p.eval t ≠ 0.

theorem Valuation.le_one_of_root_monic {L : Type u_1} {Γ : Type u_2} [CommRing L] [LinearOrderedCommGroupWithZero Γ] (ν : Valuation L Γ) {t : L} {p : Polynomial L} (hp : p.Monic) (hcoeff : ∀ i < p.natDegree, ν (p.coeff i) ≤ 1) (hdeg : p.natDegree ≠ 0) (heq : Polynomial.eval t p = 0) : ν t ≤ 1

A root of a monic polynomial of positive degree with coefficients that are integral for the valuation ν is itself integral. (This is a concrete form of the fact that valuation rings are integrally closed.)

theorem IsDedekindDomain.HeightOneSpectrum.finite_setOf_valuation_ne_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {x : K} (hx : x ≠ 0) : {v : HeightOneSpectrum R | (valuation K v) x ≠ 1}.Finite

A nonzero element of the fraction field of a Dedekind domain has trivial valuation at all but finitely many primes.

theorem Set.integer_mono {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S T : Set (IsDedekindDomain.HeightOneSpectrum R)} (hST : S ⊆ T) : S.integer K ≤ T.integer K

theorem Set.unit_mono {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S T : Set (IsDedekindDomain.HeightOneSpectrum R)} (hST : S ⊆ T) : S.unit K ≤ T.unit K

theorem IsDedekindDomain.HeightOneSpectrum.le_count_iff_le {A : Type u_3} [CommRing A] [IsDedekindDomain A] (v : HeightOneSpectrum A) {J : Ideal A} (hJ : J ≠ ⊥) (k : ℕ) : k ≤ (Associates.mk v.asIdeal).count (Associates.mk J).factors ↔ J ≤ v.asIdeal ^ k

Ideal-level divisibility characterization of Associates.count: the multiplicity of v in J is at least k iff v ^ k divides J.

theorem IsDedekindDomain.HeightOneSpectrum.le_count_iff {A : Type u_3} [CommRing A] [IsDedekindDomain A] (v : HeightOneSpectrum A) {x : A} (hx : x ≠ 0) (k : ℕ) : k ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors ↔ x ∈ v.asIdeal ^ k

Divisibility characterization of Associates.count for a height one prime: the v-adic valuation of x is at least k iff x ∈ v ^ k.

theorem IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (u : Kˣ) (m : Multiplicative ℤ) : v.valuationOfNeZero u = m ↔ (valuation K v) ↑u = ↑m

The Multiplicative ℤ-valued valuation of a unit is determined by the ℤᵐ⁰-valued one.

theorem IsDedekindDomain.HeightOneSpectrum.dvd_toAdd_valuationOfNeZero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {n : ℕ} {u z : Kˣ} (h : (valuation K v) ↑u = (valuation K v) ↑z ^ n) : ↑n ∣ Multiplicative.toAdd (v.valuationOfNeZero u)

If the valuation of a unit u is the n-th power of the valuation of a unit z, then the v-adic order of u is divisible by n.

theorem IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroMod_mk_eq_one_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (n : ℕ) (u : Kˣ) : (v.valuationOfNeZeroMod n) ↑u = 1 ↔ ↑n ∣ Multiplicative.toAdd (v.valuationOfNeZero u)

The class of a unit u in Units.modPow K n has trivial image under the v-adic valuation mod n exactly when the v-adic valuation of u is divisible by n.

theorem IsDedekindDomain.HeightOneSpectrum.valuation_algebraMap_eq_one_of_pow_eq_span {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v w : HeightOneSpectrum R} (hne : w ≠ v) {n : ℕ} {π : R} (h : v.asIdeal ^ n = Ideal.span {π}) : (valuation K w) ((algebraMap R K) π) = 1

If a power of the prime v is generated by π, then π is a w-adic unit at every prime w ≠ v.

theorem IsDedekindDomain.HeightOneSpectrum.exp_neg_one_le_valuation_algebraMap {R : Type u_3} [CommRing R] [IsDedekindDomain R] {K : Type u_4} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {r : R} (hr : r ∉ v.asIdeal ^ 2) : WithZero.exp (-1) ≤ (valuation K v) ((algebraMap R K) r)

The valuation of an element of R not lying in v ^ 2 is at least exp (-1): it can vanish at v at most to first order.

theorem IsDedekindDomain.HeightOneSpectrum.notMem_pow_two_of_squarefree {R : Type u_3} [CommRing R] [IsPrincipalIdealRing R] (v : HeightOneSpectrum R) {r : R} (hr : Squarefree r) : r ∉ v.asIdeal ^ 2

In a principal ideal domain, a squarefree element lies in no square of a maximal ideal.

def IsDedekindDomain.HeightOneSpectrum.primesAbove (R : Type u_1) [CommRing R] (B : Type u_3) [CommRing B] [Algebra R B] (S : Set (HeightOneSpectrum R)) : Set (HeightOneSpectrum B)

The primes of B lying above a set S of primes of R.

Equations

• IsDedekindDomain.HeightOneSpectrum.primesAbove R B S = {w : IsDedekindDomain.HeightOneSpectrum B | ∃ v ∈ S, v.asIdeal = Ideal.under R w.asIdeal}

theorem IsDedekindDomain.HeightOneSpectrum.primesAbove_mono (R : Type u_1) [CommRing R] (B : Type u_3) [CommRing B] [Algebra R B] {S T : Set (HeightOneSpectrum R)} (hST : S ⊆ T) : primesAbove R B S ⊆ primesAbove R B T

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.primesAbove_empty (R : Type u_1) [CommRing R] (B : Type u_3) [CommRing B] [Algebra R B] : primesAbove R B ∅ = ∅

def IsDedekindDomain.HeightOneSpectrum.below (R : Type u_1) [CommRing R] [IsDedekindDomain R] (B : Type u_3) [CommRing B] [IsDedekindDomain B] [Algebra R B] [Algebra.IsIntegral R B] (w : HeightOneSpectrum B) : HeightOneSpectrum R

The prime of R lying below a prime w of an integral extension B.

Equations

• IsDedekindDomain.HeightOneSpectrum.below R B w = { asIdeal := Ideal.under R w.asIdeal, isPrime := ⋯, ne_bot := ⋯ }

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.below_asIdeal (R : Type u_1) [CommRing R] [IsDedekindDomain R] (B : Type u_3) [CommRing B] [IsDedekindDomain B] [Algebra R B] [Algebra.IsIntegral R B] (w : HeightOneSpectrum B) : (below R B w).asIdeal = Ideal.under R w.asIdeal

instance IsDedekindDomain.HeightOneSpectrum.instLiesOverBelow (R : Type u_1) [CommRing R] [IsDedekindDomain R] (B : Type u_3) [CommRing B] [IsDedekindDomain B] [Algebra R B] [Algebra.IsIntegral R B] (w : HeightOneSpectrum B) : w.asIdeal.LiesOver (below R B w).asIdeal

theorem IsDedekindDomain.HeightOneSpectrum.mem_primesAbove_iff (R : Type u_1) [CommRing R] [IsDedekindDomain R] (B : Type u_3) [CommRing B] [IsDedekindDomain B] [Algebra R B] [Algebra.IsIntegral R B] (S : Set (HeightOneSpectrum R)) (w : HeightOneSpectrum B) : w ∈ primesAbove R B S ↔ below R B w ∈ S

theorem IsDedekindDomain.HeightOneSpectrum.primesAbove_finite (R : Type u_1) [CommRing R] [IsDedekindDomain R] (B : Type u_3) [CommRing B] [IsDedekindDomain B] [Algebra R B] [Algebra.IsIntegral R B] [Module.IsTorsionFree R B] {S : Set (HeightOneSpectrum R)} (hS : S.Finite) : (primesAbove R B S).Finite

Only finitely many primes of B lie above a finite set of primes of R: each fiber injects into Ideal.primesOver, which is finite for a Dedekind extension.

def IsDedekindDomain.selmerGroupAbove (R : Type u_1) [CommRing R] (B : Type u_3) [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra B L] [IsFractionRing B L] (S : Set (HeightOneSpectrum R)) (n : ℕ) : Subgroup (Units.modPow L n)

The S-Selmer group of L, where B is a Dedekind domain with fraction field L and S is a set of primes of R: the classes of Lˣ modulo n-th powers whose valuation is divisible by n at every prime of B not lying above S.

Equations

• IsDedekindDomain.selmerGroupAbove R B L S n = IsDedekindDomain.selmerGroup

theorem IsDedekindDomain.mem_selmerGroupAbove_iff (R : Type u_1) [CommRing R] (B : Type u_3) [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra B L] [IsFractionRing B L] (S : Set (HeightOneSpectrum R)) (n : ℕ) (x : Units.modPow L n) : x ∈ selmerGroupAbove R B L S n ↔ ∀ w ∉ HeightOneSpectrum.primesAbove R B S, (w.valuationOfNeZeroMod n) x = 1

theorem IsDedekindDomain.selmerGroupAbove_empty (R : Type u_1) [CommRing R] (B : Type u_3) [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra B L] [IsFractionRing B L] (n : ℕ) : selmerGroupAbove R B L ∅ n = selmerGroup

@[simp]

theorem IsDiscreteValuationRing.asIdeal_maximalIdeal (A : Type u_4) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] : (maximalIdeal A).asIdeal = IsLocalRing.maximalIdeal A

theorem IsDedekindDomain.HeightOneSpectrum.eq_maximalIdeal {A : Type u_4} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (P : HeightOneSpectrum A) : P = IsDiscreteValuationRing.maximalIdeal A

The maximal ideal is the only height-one prime of a discrete valuation ring.

def IsDedekindDomain.HeightOneSpectrum.comapOfNeBot {B : Type u_4} {C : Type u_5} [CommRing B] [CommRing C] (ψ : B →+* C) (w : HeightOneSpectrum C) (hne : Ideal.comap ψ w.asIdeal ≠ ⊥) : HeightOneSpectrum B

The height-one prime of B obtained by contracting a height-one prime along a ring homomorphism ψ : B →+* C, given that the contraction is nonzero.

Equations

• IsDedekindDomain.HeightOneSpectrum.comapOfNeBot ψ w hne = { asIdeal := Ideal.comap ψ w.asIdeal, isPrime := ⋯, ne_bot := hne }

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.comapOfNeBot_asIdeal {B : Type u_4} {C : Type u_5} [CommRing B] [CommRing C] (ψ : B →+* C) (w : HeightOneSpectrum C) (hne : Ideal.comap ψ w.asIdeal ≠ ⊥) : (comapOfNeBot ψ w hne).asIdeal = Ideal.comap ψ w.asIdeal

theorem IsDedekindDomain.HeightOneSpectrum.exists_valuationOfNeZero_map_eq {B : Type u_4} {C : Type u_5} [CommRing B] [IsDedekindDomain B] [CommRing C] [IsDedekindDomain C] {L : Type u_6} {N : Type u_7} [Field L] [Algebra B L] [IsFractionRing B L] [Field N] [Algebra C N] [IsFractionRing C N] (φ : L →+* N) (ψ : B →+* C) (hcomp : (algebraMap C N).comp ψ = φ.comp (algebraMap B L)) (w : HeightOneSpectrum C) (hne : Ideal.comap ψ w.asIdeal ≠ ⊥) : ∃ (e : ℕ), ∀ (u : Lˣ), w.valuationOfNeZero ((Units.map ↑φ) u) = (comapOfNeBot ψ w hne).valuationOfNeZero u ^ e

The w-adic valuation of φ u is the valuation of u at the contracted prime, raised to a fixed positive power (the ramification index), for an embedding φ of fraction fields compatible with an embedding ψ of Dedekind domains.

theorem IsDedekindDomain.HeightOneSpectrum.dvd_toAdd_valuationOfNeZero_map {B : Type u_4} {C : Type u_5} [CommRing B] [IsDedekindDomain B] [CommRing C] [IsDedekindDomain C] {L : Type u_6} {N : Type u_7} [Field L] [Algebra B L] [IsFractionRing B L] [Field N] [Algebra C N] [IsFractionRing C N] (φ : L →+* N) (ψ : B →+* C) (hcomp : (algebraMap C N).comp ψ = φ.comp (algebraMap B L)) (w : HeightOneSpectrum C) (hne : Ideal.comap ψ w.asIdeal ≠ ⊥) {n : ℕ} (u : Lˣ) (h : ↑n ∣ Multiplicative.toAdd ((comapOfNeBot ψ w hne).valuationOfNeZero u)) : ↑n ∣ Multiplicative.toAdd (w.valuationOfNeZero ((Units.map ↑φ) u))

Divisibility of adic valuations transports along compatible embeddings: if the valuation of u at the contracted prime is divisible by n, so is the w-adic valuation of φ u.

theorem IsDedekindDomain.HeightOneSpectrum.comap_maximalIdeal_adicCompletionIntegers (R : Type u_1) [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Ideal.comap (algebraMap R ↥(adicCompletionIntegers K v)) (IsLocalRing.maximalIdeal ↥(adicCompletionIntegers K v)) = v.asIdeal

The maximal ideal of the ring of integers of the completion of K at v contracts to v itself.

theorem Polynomial.resultant_C_sub_X {R : Type u_1} [CommRing R] (f : Polynomial R) (x : R) (m : ℕ) (hm : f.natDegree ≤ m) : f.resultant (C x - X) m 1 = eval x f

The resultant of f with the linear polynomial C x - X is f.eval x. Note the absence of a sign: C x - X is -(X - C x), and the two signs cancel.

theorem Polynomial.Monic.resultant_one_right {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (n : ℕ) : g.resultant 1 g.natDegree n = 1

theorem Polynomial.Monic.resultant_congr_right {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) {p : Polynomial R} {n₁ n₂ : ℕ} (h₁ : p.natDegree ≤ n₁) (h₂ : n₁ ≤ n₂) : g.resultant p g.natDegree n₂ = g.resultant p g.natDegree n₁

For monic g, the resultant does not depend on the size parameter used for the second argument, as long as it is at least its degree.

theorem Polynomial.discr_X_sub_C_mul {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (hdeg : 0 < g.natDegree) (x : R) : ((X - C x) * g).discr = g.discr * eval x g ^ 2

The discriminant of (X - C x) * g for monic g of positive degree is g.discr * g.eval x ^ 2.

theorem Polynomial.mem_degreeLT_natDegree_iff {R : Type u_1} [CommRing R] {g q : Polynomial R} (hg : g ≠ 0) : q ∈ degreeLT R g.natDegree ↔ q.degree < g.degree

theorem Polynomial.eval_pos_of_monic_of_irreducible_of_natDegree_eq_two {q : Polynomial ℝ} (hm : q.Monic) (hirr : Irreducible q) (hd : q.natDegree = 2) (x : ℝ) : 0 < eval x q

A monic real polynomial that is irreducible of degree 2 is positive definite: being irreducible of degree > 1 it has no real root, and its leading coefficient is 1 > 0.

theorem Polynomial.exists_eq_C_mul_X_sub_C_of_natDegree_le_one {R : Type u_1} [CommRing R] [Nontrivial R] {p : Polynomial R} (hdeg : p.natDegree ≤ 1) {x : R} (hx : p.IsRoot x) : ∃ (γ : R), p = C γ * (X - C x)

theorem Polynomial.modByMonic_mem_degreeLT {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] (hg : g.Monic) (q : Polynomial R) : q %ₘ g ∈ degreeLT R g.natDegree

theorem Polynomial.divByMonic_mem_degreeLT {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] {q : Polynomial R} {n : ℕ} (hg : g.Monic) (hq : q ∈ degreeLT R (g.natDegree + n)) : q /ₘ g ∈ degreeLT R n

theorem Polynomial.eq_zero_of_monic_dvd_of_degree_lt {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] {q : Polynomial R} (hg : g.Monic) (hdvd : g ∣ q) (hq : q.degree < g.degree) : q = 0

theorem Polynomial.Monic.divByMonic_mul_add {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] (hg : g.Monic) (v u : Polynomial R) : (g * v + u) /ₘ g = v + u /ₘ g

theorem Polynomial.Monic.modByMonic_mul_add {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] (hg : g.Monic) (v u : Polynomial R) : (g * v + u) %ₘ g = u %ₘ g

The norm on AdjoinRoot g is the resultant

Write m = g.natDegree and n = p.natDegree. The Sylvester map S : R[X]_m × R[X]_n →ₗ R[X]_(m+n), (u, v) ↦ g * v + p * u, has the Sylvester matrix as its matrix, so det S = resultant g p m n.

Taking p = 1 gives a map Ψ : (u, v) ↦ g * v + u, which is a linear equivalence when g is monic (its inverse is q ↦ (q %ₘ g, q /ₘ g)), and det Ψ = resultant g 1 m n = 1.

Now S = Ψ ∘ₗ B where B := Ψ⁻¹ ∘ₗ S is the endomorphism (u, v) ↦ ((p * u) %ₘ g, v + (p * u) /ₘ g) of R[X]_m × R[X]_n, by modByMonic_add_div. In the block decomposition the matrix of B is lower triangular with diagonal blocks mulModByMonic hg p and 1, so det B = det (mulModByMonic hg p).

Finally mk g : R[X]_m ≃ₗ AdjoinRoot g conjugates mulModByMonic hg p into multiplication by mk g p, whose determinant is by definition Algebra.norm R (mk g p).

No signs appear anywhere: B is an endomorphism, so the two blocks are never reordered.

noncomputable def Polynomial.mulModByMonic {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] (hg : g.Monic) (p : Polynomial R) : ↥(degreeLT R g.natDegree) →ₗ[R] ↥(degreeLT R g.natDegree)

Multiplication by p on R[X]_(g.natDegree), that is, q ↦ (p * q) %ₘ g. This is the map that mk g : R[X]_(g.natDegree) ≃ₗ AdjoinRoot g turns into multiplication by mk g p.

Equations

• Polynomial.mulModByMonic hg p = { toFun := fun (q : ↥(Polynomial.degreeLT R g.natDegree)) => ⟨p * ↑q %ₘ g, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Polynomial.mulModByMonic_apply_coe {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] (hg : g.Monic) (p : Polynomial R) (q : ↥(degreeLT R g.natDegree)) : ↑((mulModByMonic hg p) q) = p * ↑q %ₘ g

noncomputable def Polynomial.sylvesterEquivOne {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] (hg : g.Monic) (n : ℕ) : (↥(degreeLT R g.natDegree) × ↥(degreeLT R n)) ≃ₗ[R] ↥(degreeLT R (g.natDegree + n))

For monic g, the Sylvester map of g and 1, namely (u, v) ↦ g * v + u, is a linear equivalence R[X]_(g.natDegree) × R[X]_n ≃ₗ R[X]_(g.natDegree + n). Its inverse is q ↦ (q %ₘ g, q /ₘ g).

Equations

• Polynomial.sylvesterEquivOne hg n = LinearEquiv.ofBijective (g.sylvesterMap 1 ⋯ ⋯) ⋯

@[simp]

theorem Polynomial.coe_sylvesterEquivOne {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] (hg : g.Monic) (n : ℕ) : ↑(sylvesterEquivOne hg n) = g.sylvesterMap 1 ⋯ ⋯

theorem Polynomial.coe_sylvesterEquivOne_symm {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] (hg : g.Monic) (n : ℕ) (q : ↥(degreeLT R (g.natDegree + n))) : ↑((sylvesterEquivOne hg n).symm q).1 = ↑q %ₘ g ∧ ↑((sylvesterEquivOne hg n).symm q).2 = ↑q /ₘ g

The inverse of Ψ is division with remainder by g.

noncomputable def Polynomial.sylvesterBlock {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] {n : ℕ} (hg : g.Monic) (p : Polynomial R) (hp : p.natDegree ≤ n) : ↥(degreeLT R g.natDegree) × ↥(degreeLT R n) →ₗ[R] ↥(degreeLT R g.natDegree) × ↥(degreeLT R n)

The block-triangular endomorphism B = Ψ⁻¹ ∘ₗ S of R[X]_(g.natDegree) × R[X]_n.

Equations

• Polynomial.sylvesterBlock hg p hp = ↑(Polynomial.sylvesterEquivOne hg n).symm ∘ₗ g.sylvesterMap p ⋯ hp

theorem Polynomial.coe_sylvesterBlock_apply_fst {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] {n : ℕ} (hg : g.Monic) (p : Polynomial R) (hp : p.natDegree ≤ n) (u : ↥(degreeLT R g.natDegree)) (v : ↥(degreeLT R n)) : ↑((sylvesterBlock hg p hp) (u, v)).1 = p * ↑u %ₘ g

The first coordinate of B (u, v) is (p * u) %ₘ g.

theorem Polynomial.coe_sylvesterBlock_apply_snd {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] {n : ℕ} (hg : g.Monic) (p : Polynomial R) (hp : p.natDegree ≤ n) (u : ↥(degreeLT R g.natDegree)) (v : ↥(degreeLT R n)) : ↑((sylvesterBlock hg p hp) (u, v)).2 = ↑v + p * ↑u /ₘ g

The second coordinate of B (u, v) is v + (p * u) /ₘ g.

theorem Polynomial.det_sylvesterBlock {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] {n : ℕ} (hg : g.Monic) (p : Polynomial R) (hp : p.natDegree ≤ n) : LinearMap.det (sylvesterBlock hg p hp) = LinearMap.det (mulModByMonic hg p)

The determinant of the block-triangular map B is the determinant of its upper-left block.

theorem Polynomial.Monic.irreducible_map_fraction_map_of_irreducible_map {R : Type u_1} [CommRing R] {g : Polynomial R} [IsIntegrallyClosed R] [IsDomain R] {S : Type u_2} {K : Type u_3} [CommRing S] [IsDomain S] [Field K] [Algebra R K] [IsFractionRing R K] (hg : g.Monic) (φ : R →+* S) (h : Irreducible (Polynomial.map φ g)) : Irreducible (Polynomial.map (algebraMap R K) g)

To show that a monic polynomial over an integrally closed domain is irreducible over its fraction field, it suffices to exhibit an irreducible image under some ring homomorphism to a domain, e.g. reduction modulo a prime.

@[simp]

theorem AdjoinRoot.mk_modByMonic {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (q : Polynomial R) : (mk g) (q %ₘ g) = (mk g) q

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

theorem AdjoinRoot.mk_eq_mk_iff_of_degree_lt {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial 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

noncomputable def AdjoinRoot.degreeLTEquiv {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] (hg : g.Monic) : ↥(Polynomial.degreeLT R g.natDegree) ≃ₗ[R] AdjoinRoot g

mk g is a linear equivalence from the polynomials of degree < g.natDegree onto AdjoinRoot g, for g monic.

Equations

• AdjoinRoot.degreeLTEquiv hg = LinearEquiv.ofBijective ((AdjoinRoot.mkₐ g).toLinearMap ∘ₗ (Polynomial.degreeLT R g.natDegree).subtype) ⋯

@[simp]

theorem AdjoinRoot.degreeLTEquiv_apply {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] (hg : g.Monic) (q : ↥(Polynomial.degreeLT R g.natDegree)) : (degreeLTEquiv hg) q = (mk g) ↑q

theorem AdjoinRoot.nonempty_algEquiv_complex {q : Polynomial ℝ} (hm : q.Monic) (hirr : Irreducible q) (hd : q.natDegree = 2) : Nonempty (AdjoinRoot q ≃ₐ[ℝ] ℂ)

For a monic irreducible quadratic q : ℝ[X], the field ℝ[X]/(q) is ℂ: it is a degree-2 (hence not ℝ) algebraic extension of ℝ, and every such extension is ℝ or ℂ.

theorem AdjoinRoot.norm_mk_eq_det_mulModByMonic {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] (hg : g.Monic) (p : Polynomial R) : (Algebra.norm R) ((mk g) p) = LinearMap.det (Polynomial.mulModByMonic hg p)

The norm of mk g p is the determinant of multiplication by p on R[X]_(g.natDegree), because degreeLTEquiv hg conjugates the latter into multiplication by mk g p.

theorem AdjoinRoot.norm_mk_eq_resultant {R : Type u_1} [CommRing R] {g : Polynomial R} [Nontrivial R] (hg : g.Monic) (p : Polynomial R) : (Algebra.norm R) ((mk g) p) = g.resultant p

The norm of AdjoinRoot.mk g p over the base ring, for g monic, is the resultant of g and p. Equivalently, it is the product of the values of p at the roots of g.

theorem AdjoinRoot.isIntegralElem_root_of_map {R : Type u_1} [CommRing R] {g : Polynomial R} {S : Type u_2} [CommRing S] (φ : R →+* S) {h : Polynomial S} (hg : g.Monic) (hmap : Polynomial.map φ g = h) : ((algebraMap S (AdjoinRoot h)).comp φ).IsIntegralElem (root h)

The root of h = g.map φ in S[X]/(h), for g monic over R, is integral over R (along the composite of φ with the canonical map).

@[simp]

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

Evaluation of AdjoinRoot.map on the class of a polynomial (the companion of Mathlib's AdjoinRoot.map_of and AdjoinRoot.map_root).

theorem AdjoinRoot.map_comp_algebraMap {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {p : Polynomial K} {q : Polynomial (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} (hq : q ∣ Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) p) : (map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) p q hq).comp (algebraMap R (AdjoinRoot p)) = (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (AdjoinRoot q)).comp (algebraMap R ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))

The base-change map K[X]/(p) →+* K_v[X]/(q) of AdjoinRoots at a completion is compatible with the algebra maps from the underlying Dedekind domain R and from the ring of integers of the completion.

The norm on a product algebra

theorem Algebra.norm_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A] [Module.Free R B] [Module.Finite R B] (x : A × B) : (norm R) x = (norm R) x.1 * (norm R) x.2

The R-norm on a product algebra is the product of the norms.

theorem Algebra.norm_pi {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] {S : ι → Type u_3} [(i : ι) → CommRing (S i)] [(i : ι) → Algebra R (S i)] [∀ (i : ι), Module.Free R (S i)] [∀ (i : ι), Module.Finite R (S i)] (g : (i : ι) → S i) : (norm R) g = ∏ i : ι, (norm R) (g i)

The R-norm on a finite product of R-algebras is the product of the norms.

Decomposition of K[X]/(f) into a product of fields

For a nonzero squarefree f over a field K, the étale algebra AdjoinRoot f is the product of the fields AdjoinRoot p, where p runs over the distinct irreducible factors of f. This is what lets one talk about the primes, and hence the Selmer group, of AdjoinRoot f: they are those of the factors.

If moreover f is separable, each factor is separable, so each AdjoinRoot p is a finite separable extension of K and its integral closure over a Dedekind domain is again Dedekind.

@[reducible, inline]

abbrev Polynomial.Factors {K : Type u_1} [Field K] (f : Polynomial K) : Type u_1

The distinct monic irreducible factors of f, as an index type.

Note that this is not defined via normalizedFactors (which would require DecidableEq K); membership in normalizedFactors f is characterized by Factors.mem_normalizedFactors_iff.

Equations

• f.Factors = { p : Polynomial K // p.Monic ∧ Irreducible p ∧ p ∣ f }

theorem Polynomial.Factors.monic {K : Type u_1} [Field K] {f : Polynomial K} (p : f.Factors) : (↑p).Monic

theorem Polynomial.Factors.irreducible {K : Type u_1} [Field K] {f : Polynomial K} (p : f.Factors) : Irreducible ↑p

theorem Polynomial.Factors.dvd {K : Type u_1} [Field K] {f : Polynomial K} (p : f.Factors) : ↑p ∣ f

theorem Polynomial.Factors.coe_eq {K : Type u_1} [Field K] {f : Polynomial K} (hf : Irreducible f) (hmon : f.Monic) (p : f.Factors) : ↑p = f

If f itself is monic and irreducible, then its only factor is f.

@[reducible]

def Polynomial.Factors.unique {K : Type u_1} [Field K] {f : Polynomial K} (hf : Irreducible f) (hmon : f.Monic) : Unique f.Factors

A monic irreducible polynomial has itself as its only monic irreducible factor.

Equations

• Polynomial.Factors.unique hf hmon = { default := ⟨f, ⋯⟩, uniq := ⋯ }

theorem Polynomial.Factors.ne_zero {K : Type u_1} [Field K] {f : Polynomial K} (p : f.Factors) : ↑p ≠ 0

theorem Polynomial.Factors.prime {K : Type u_1} [Field K] {f : Polynomial K} (p : f.Factors) : Prime ↑p

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

theorem Polynomial.Factors.mem_normalizedFactors_iff {K : Type u_1} [Field K] {f : Polynomial K} [DecidableEq K] (hf : f ≠ 0) {p : Polynomial K} : p ∈ UniqueFactorizationMonoid.normalizedFactors f ↔ p.Monic ∧ Irreducible p ∧ p ∣ f

Membership in normalizedFactors (with its normalization from DecidableEq K) is equivalent to being a monic irreducible factor.

theorem Polynomial.Factors.finite {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0) : Finite f.Factors

theorem Polynomial.Factors.nonempty {K : Type u_1} [Field K] {f : Polynomial K} (hu : ¬IsUnit f) : Nonempty f.Factors

noncomputable def Polynomial.Factors.linearEquivRoots {K : Type u_1} [Field K] {f : Polynomial K} : { p : f.Factors // (↑p).natDegree = 1 } ≃ { x : K // eval x f = 0 }

The monic linear factors of f correspond to the roots of f.

Equations

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

theorem Polynomial.Factors.isCoprime {K : Type u_1} [Field K] {f : Polynomial K} {p q : f.Factors} (hne : p ≠ q) : IsCoprime ↑p ↑q

theorem Polynomial.Factors.isCoprime_span {K : Type u_1} [Field K] {f : Polynomial K} {p q : f.Factors} (hne : p ≠ q) : IsCoprime (Ideal.span {↑p}) (Ideal.span {↑q})

theorem Polynomial.Factors.associated_prod {K : Type u_1} [Field K] {f : Polynomial K} [Fintype f.Factors] (hf : f ≠ 0) (hsq : Squarefree f) : Associated (∏ p : f.Factors, ↑p) f

theorem Polynomial.Factors.sum_natDegree_le {K : Type u_1} [Field K] {f : Polynomial K} [Fintype f.Factors] (hf : f ≠ 0) : ∑ p : f.Factors, (↑p).natDegree ≤ f.natDegree

The degrees of the distinct monic irreducible factors of f ≠ 0 sum to at most the degree of f (with equality iff f is squarefree, up to normalization).

theorem Polynomial.Factors.span_eq_iInf_span {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0) (hsq : Squarefree f) : Ideal.span {f} = ⨅ (p : f.Factors), Ideal.span {↑p}

theorem Polynomial.Factors.exists_dvd_map {K : Type u_1} [Field K] {f : Polynomial K} {L : Type u_2} [Field L] (σ : K →+* L) (hf : f ≠ 0) {q : Polynomial L} (hq : Prime q) (hdvd : q ∣ map σ f) : ∃ (p : f.Factors), q ∣ map σ ↑p

An irreducible factor of the image of f under a field embedding divides the image of one of the irreducible factors of 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)

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

theorem AdjoinRoot.finrank_eq_natDegree {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0) : Module.finrank K (AdjoinRoot f) = f.natDegree

The dimension of K[X]/(f) over K is the degree of f.

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

theorem AdjoinRoot.discr_powerBasis_eq_discr {K : Type u_1} [Field K] {f : Polynomial K} [Fact (Irreducible f)] [Algebra.IsSeparable K (AdjoinRoot f)] (hf : f.Monic) (hd : (Polynomial.derivative f).natDegree = f.natDegree - 1) : Algebra.discr K ⇑(powerBasis ⋯).basis = f.discr

The discriminant of the power basis of K[X]/(f), for f monic irreducible with derivative of the generic degree, is the discriminant of the polynomial f.

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 →+* AdjoinRoot ↑p

The projection of K[X]/(f) onto the field factor K[X]/(p).

Equations

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

@[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

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

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

Equations

• AdjoinRoot.modPowEquivPiFactors hf hsq n = (Units.modPow.congr (AdjoinRoot.equivPiFactors hf hsq).toMulEquiv n).trans (Units.modPow.piEquiv (fun (p : f.Factors) => AdjoinRoot ↑p) n)

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.

@[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)) u)

On the class of a unit, modPowEquivPiFactors is componentwise projection to the factors (Units.map version of modPowEquivPiFactors_unit).

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)) u) = 1

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

theorem AdjoinRoot.norm_eq_prod_norm_projFactor {K : Type u_1} [Field K] {f : Polynomial K} [Fintype f.Factors] (hf : f ≠ 0) (hsq : Squarefree f) (a : AdjoinRoot f) : (Algebra.norm K) a = ∏ p : f.Factors, (Algebra.norm K) ((projFactor hf hsq p) a)

The norm of an element of K[X]/(f) is the product of the norms of its components in the field factors.

theorem AdjoinRoot.norm_projFactor_mk_C_sub_X {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0) (hsq : Squarefree f) (p : f.Factors) (x : K) : (Algebra.norm K) ((projFactor hf hsq p) ((mk f) (Polynomial.C x - Polynomial.X))) = Polynomial.eval x ↑p

The norm of the component at the factor p of the class of C x - X is p.eval x.

Rings of integers in finite extensions of number fields

The integral closure of 𝓞 K in a finite extension L of a number field K is (isomorphic to) the ring of integers of L; consequently the class number theorem and (the finite-generation part of) Dirichlet's unit theorem apply to it.

instance Rat.instIsPrincipalIdealRingRingOfIntegers : IsPrincipalIdealRing (NumberField.RingOfIntegers ℚ)

theorem isIntegralClosure_int_integralClosure (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : IsIntegralClosure ↥(integralClosure (NumberField.RingOfIntegers K) L) ℤ L

The integral closure of 𝓞 K in an extension L of K is the integral closure of ℤ in L.

theorem NumberField.finite_classGroup_integralClosure (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] : Finite (ClassGroup ↥(integralClosure (RingOfIntegers K) L))

The class number theorem for the integral closure of 𝓞 K in a finite extension L of the number field K: its class group is finite.

theorem NumberField.fg_units_integralClosure (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] : Group.FG (↥(integralClosure (RingOfIntegers K) L))ˣ

Dirichlet's unit theorem (finite generation) for the integral closure of 𝓞 K in a finite extension L of the number field K: its unit group is finitely generated.

theorem NumberField.subsingleton_classGroup_integralClosure (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] (h : IsPrincipalIdealRing (RingOfIntegers L)) : Subsingleton (ClassGroup ↥(integralClosure (RingOfIntegers K) L))

If the ring of integers of L is a principal ideal domain, then the integral closure of 𝓞 K in L (being isomorphic to 𝓞 L) has trivial class group.

theorem NumberField.finrank_additive_units_integralClosure (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] : Module.finrank ℤ (Additive (↥(integralClosure (RingOfIntegers K) L))ˣ) = Module.finrank ℤ (Additive (RingOfIntegers L)ˣ)

The unit group of the integral closure of 𝓞 K in a finite extension L has the same rank as that of 𝓞 L (they are isomorphic).

Discriminants, class numbers, and unit ranks of cubic fields

The discriminant of a number field is the discriminant of any power basis with integral generator divided by a square; consequently a cubic field whose power-basis discriminant is at most 49 in absolute value has trivial class group (by the Minkowski bound), and the sign of the power-basis discriminant determines the signature and hence, by Dirichlet's unit theorem, the unit rank (1 if negative, 2 if positive).

theorem NumberField.exists_eq_discr_mul_sq {K : Type u_1} [Field K] [NumberField K] (pb : PowerBasis ℚ K) (hpb : IsIntegral ℤ pb.gen) {d : ℤ} (hd : Algebra.discr ℚ ⇑pb.basis = ↑d) : ∃ (q : ℤ), d = discr K * q ^ 2

The discriminant of any power basis of a number field K over ℚ with integral generator (expressed via an integer d mapping to it) is the field discriminant times a square. In particular, discr K divides d and has the same sign.

theorem RingOfIntegers.finrank_additive_units_of_discr_neg {K : Type u_1} [Field K] [NumberField K] (h3 : Module.finrank ℚ K = 3) (hd : NumberField.discr K < 0) : Module.finrank ℤ (Additive (NumberField.RingOfIntegers K)ˣ) = 1

A cubic number field with negative discriminant has unit rank 1: its signature is (1, 1), so Dirichlet's unit theorem gives rank 1 + 1 - 1 = 1.

theorem RingOfIntegers.finrank_additive_units_of_discr_pos {K : Type u_1} [Field K] [NumberField K] (h3 : Module.finrank ℚ K = 3) (hd : 0 < NumberField.discr K) : Module.finrank ℤ (Additive (NumberField.RingOfIntegers K)ˣ) = 2

A cubic number field with positive discriminant has unit rank 2: it is totally real, so Dirichlet's unit theorem gives rank 3 - 1 = 2.

theorem RingOfIntegers.isPrincipalIdealRing_of_finrank_eq_three_of_abs_discr_le {K : Type u_1} [Field K] [NumberField K] (h3 : Module.finrank ℚ K = 3) (hd : |NumberField.discr K| ≤ 49) : IsPrincipalIdealRing (NumberField.RingOfIntegers K)

A cubic number field with |discr K| ≤ 49 has a principal ring of integers: its Minkowski bound is less than 2 for either signature.