mathlib3 documentation

ring_theory.integral_domain

Integral domains #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Assorted theorems about integral domains.

Main theorems #

TODO #

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

Tags #

integral domain, finite integral domain, finite field

source
theorem mul_right_bijective_of_finite₀ {M : Type u_1} [cancel_monoid_with_zero M] [finite M] {a : M} (ha : a ≠ 0) :
function.bijective (λ (b : M), a * b)
source
theorem mul_left_bijective_of_finite₀ {M : Type u_1} [cancel_monoid_with_zero M] [finite M] {a : M} (ha : a ≠ 0) :
function.bijective (λ (b : M), b * a)
source
def fintype.group_with_zero_of_cancel (M : Type u_1) [cancel_monoid_with_zero M] [decidable_eq M] [fintype M] [nontrivial M] :
group_with_zero M

Every finite nontrivial cancel_monoid_with_zero is a group_with_zero.

Equations
source
theorem exists_eq_pow_of_mul_eq_pow_of_coprime {R : Type u_1} [comm_semiring R] [is_domain R] [gcd_monoid R] [unique Rˣ] {a b c : R} {n : ℕ} (cp : is_coprime a b) (h : a * b = c ^ n) :
∃ (d : R), a = d ^ n
source
theorem finset.exists_eq_pow_of_mul_eq_pow_of_coprime {ι : Type u_1} {R : Type u_2} [comm_semiring R] [is_domain R] [gcd_monoid R] [unique Rˣ] {n : ℕ} {c : R} {s : finset ι} {f : ι → R} (h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → is_coprime (f i) (f j)) (hprod : s.prod (λ (i : ι), f i) = c ^ n) (i : ι) (H : i ∈ s) :
∃ (d : R), f i = d ^ n
source
def fintype.division_ring_of_is_domain (R : Type u_1) [ring R] [is_domain R] [decidable_eq R] [fintype R] :
division_ring 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
source
def fintype.field_of_domain (R : Type u_1) [comm_ring R] [is_domain R] [decidable_eq 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
source
theorem finite.is_field_of_domain (R : Type u_1) [comm_ring R] [is_domain R] [finite R] :
is_field R
source
theorem card_nth_roots_subgroup_units {R : Type u_1} {G : Type u_2} [comm_ring R] [is_domain R] [group G] [fintype G] (f : G →* R) (hf : function.injective ⇑f) {n : ℕ} (hn : 0 < n) (g₀ : G) :
{g ∈ finset.univ | g ^ n = g₀}.card ≤ ⇑multiset.card (polynomial.nth_roots n (⇑f g₀))
source
theorem is_cyclic_of_subgroup_is_domain {R : Type u_1} {G : Type u_2} [comm_ring R] [is_domain R] [group G] [finite G] (f : G →* R) (hf : function.injective ⇑f) :
is_cyclic G

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

source
@[protected, instance]
def units.is_cyclic {R : Type u_1} [comm_ring R] [is_domain R] [finite Rˣ] :
is_cyclic 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.

source
@[protected, instance]
def subgroup_units_cyclic {R : Type u_1} [comm_ring R] [is_domain R] (S : subgroup Rˣ) [finite ↥S] :
is_cyclic ↥S

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

source
theorem polynomial.div_eq_quo_add_rem_div {R : Type u_1} [comm_ring R] [is_domain R] (K : Type) [field K] [algebra (polynomial R) K] [is_fraction_ring (polynomial R) K] (f : polynomial R) {g : polynomial R} (hg : g.monic) :
∃ (q r : polynomial R), r.degree < g.degree ∧ ↑f / ↑g = ↑q + ↑r / ↑g
source
theorem card_fiber_eq_of_mem_range {G : Type u_2} [group G] [fintype G] {H : Type u_1} [group H] [decidable_eq H] (f : G →* H) {x y : H} (hx : x ∈ set.range ⇑f) (hy : y ∈ set.range ⇑f) :
(finset.filter (λ (g : G), ⇑f g = x) finset.univ).card = (finset.filter (λ (g : G), ⇑f g = y) finset.univ).card
source
theorem sum_hom_units_eq_zero {R : Type u_1} {G : Type u_2} [comm_ring R] [is_domain R] [group G] [fintype G] (f : G →* R) (hf : f ≠ 1) :
finset.univ.sum (λ (g : G), ⇑f g) = 0

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

source
theorem sum_hom_units {R : Type u_1} {G : Type u_2} [comm_ring R] [is_domain R] [group G] [fintype G] (f : G →* R) [decidable (f = 1)] :
finset.univ.sum (λ (g : G), ⇑f g) = ite (f = 1) ↑(fintype.card G) 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.