Integral domains

Assorted theorems about integral domains.

Main theorems

• isCyclic_of_subgroup_isDomain: A finite subgroup of the units of an integral domain is cyclic.
• Fintype.fieldOfDomain: A finite integral domain is a field.

TODO

Prove Wedderburn's little theorem, which shows that all finite division rings are actually fields.

Tags

integral domain, finite integral domain, finite field

theorem mul_right_bijective_of_finite₀ {M : Type u_1} [CancelMonoidWithZero M] [Finite M] {a : M} (ha : a ≠ 0) : Function.Bijective fun b => a * b

theorem mul_left_bijective_of_finite₀ {M : Type u_1} [CancelMonoidWithZero M] [Finite M] {a : M} (ha : a ≠ 0) : Function.Bijective fun b => b * a

def Fintype.groupWithZeroOfCancel (M : Type u_2) [CancelMonoidWithZero M] [DecidableEq M] [Fintype M] [Nontrivial M] : GroupWithZero M

Every finite nontrivial cancel_monoid_with_zero is a group_with_zero.

Equations

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

theorem exists_eq_pow_of_mul_eq_pow_of_coprime {R : Type u_2} [CommSemiring R] [IsDomain R] [GCDMonoid R] [Unique Rˣ] {a : R} {b : R} {c : R} {n : ℕ} (cp : IsCoprime a b) (h : a * b = c ^ n) : ∃ d, a = d ^ n

theorem Finset.exists_eq_pow_of_mul_eq_pow_of_coprime {ι : Type u_2} {R : Type u_3} [CommSemiring R] [IsDomain R] [GCDMonoid R] [Unique Rˣ] {n : ℕ} {c : R} {s : Finset ι} {f : ι → R} (h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)) (hprod : (Finset.prod s fun i => f i) = c ^ n) (i : ι) : i ∈ s → ∃ d, f i = d ^ n

def Fintype.divisionRingOfIsDomain (R : Type u_3) [Ring R] [IsDomain R] [DecidableEq R] [Fintype R] : DivisionRing R

Every finite domain is a division ring.

TODO: Prove Wedderburn's little theorem, which shows a finite domain is in fact commutative, hence a field.

Equations

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

def Fintype.fieldOfDomain (R : Type u_3) [CommRing R] [IsDomain R] [DecidableEq R] [Fintype R] : Field R

Every finite commutative domain is a field.

TODO: Prove Wedderburn's little theorem, which shows a finite domain is automatically commutative, dropping one assumption from this theorem.

Equations

• Fintype.fieldOfDomain R = let src := Fintype.groupWithZeroOfCancel R; let src_1 := inst✝²; Field.mk GroupWithZero.zpow (_ : ∀ (a : R), a ≠ 0 → a * a⁻¹ = 1) (_ : 0⁻¹ = 0) (qsmulRec Rat.cast)

theorem Finite.isField_of_domain (R : Type u_3) [CommRing R] [IsDomain R] [Finite R] : IsField R

theorem card_nthRoots_subgroup_units {R : Type u_1} {G : Type u_2} [CommRing R] [IsDomain R] [Group G] [Fintype G] [DecidableEq G] (f : G →* R) (hf : Function.Injective ↑f) {n : ℕ} (hn : 0 < n) (g₀ : G) : Finset.card (Finset.filter (fun g => g ^ n = g₀) Finset.univ) ≤ ↑Multiset.card (Polynomial.nthRoots n (↑f g₀))

theorem isCyclic_of_subgroup_isDomain {R : Type u_1} {G : Type u_2} [CommRing R] [IsDomain R] [Group G] [Finite G] (f : G →* R) (hf : Function.Injective ↑f) : IsCyclic G

A finite subgroup of the unit group of an integral domain is cyclic.

instance instIsCyclicUnitsToMonoidToMonoidWithZeroToSemiringToCommSemiringInstGroupUnits {R : Type u_1} [CommRing R] [IsDomain R] [Finite Rˣ] : IsCyclic Rˣ

The unit group of a finite integral domain is cyclic.

To support ℤˣ and other infinite monoids with finite groups of units, this requires only Finite Rˣ rather than deducing it from Finite R.

Equations

• @instIsCyclicUnitsToMonoidToMonoidWithZeroToSemiringToCommSemiringInstGroupUnits = @instIsCyclicUnitsToMonoidToMonoidWithZeroToSemiringToCommSemiringInstGroupUnits.proof_1

instance subgroup_units_cyclic {R : Type u_1} [CommRing R] [IsDomain R] (S : Subgroup Rˣ) [Finite { x // x ∈ S }] : IsCyclic { x // x ∈ S }

A finite subgroup of the units of an integral domain is cyclic.

Equations

• @subgroup_units_cyclic = @subgroup_units_cyclic.proof_1

theorem Polynomial.div_eq_quo_add_rem_div {R : Type u_1} [CommRing R] [IsDomain R] (K : Type) [Field K] [Algebra (Polynomial R) K] [IsFractionRing (Polynomial R) K] (f : Polynomial R) {g : Polynomial R} (hg : Polynomial.Monic g) : ∃ q r, Polynomial.degree r < Polynomial.degree g ∧ ↑(algebraMap (Polynomial R) K) f / ↑(algebraMap (Polynomial R) K) g = ↑(algebraMap (Polynomial R) K) q + ↑(algebraMap (Polynomial R) K) r / ↑(algebraMap (Polynomial R) K) g

theorem card_fiber_eq_of_mem_range {G : Type u_2} [Group G] [Fintype G] {H : Type u_3} [Group H] [DecidableEq H] (f : G →* H) {x : H} {y : H} (hx : x ∈ Set.range ↑f) (hy : y ∈ Set.range ↑f) : Finset.card (Finset.filter (fun g => ↑f g = x) Finset.univ) = Finset.card (Finset.filter (fun g => ↑f g = y) Finset.univ)

theorem sum_hom_units_eq_zero {R : Type u_1} {G : Type u_2} [CommRing R] [IsDomain R] [Group G] [Fintype G] (f : G →* R) (hf : f ≠ 1) : (Finset.sum Finset.univ fun g => ↑f g) = 0

In an integral domain, a sum indexed by a nontrivial homomorphism from a finite group is zero.

theorem sum_hom_units {R : Type u_1} {G : Type u_2} [CommRing R] [IsDomain R] [Group G] [Fintype G] (f : G →* R) [Decidable (f = 1)] : (Finset.sum Finset.univ fun g => ↑f g) = ↑(if f = 1 then Fintype.card G else 0)

In an integral domain, a sum indexed by a homomorphism from a finite group is zero, unless the homomorphism is trivial, in which case the sum is equal to the cardinality of the group.