Integral domains #

Assorted theorems about integral domains.

Main theorems #

is_cyclic_of_subgroup_is_domain: A finite subgroup of the units of an integral domain is cyclic.
fintype.field_of_domain: 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

source

theorem mul_right_bijective_of_fintype₀ {M : Type u_1} [cancel_monoid_with_zero M] [fintype M] {a : M} (ha : a ≠ 0) :

function.bijective (λ (b : M), a * b)

source

theorem mul_left_bijective_of_fintype₀ {M : Type u_1} [cancel_monoid_with_zero M] [fintype 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

fintype.group_with_zero_of_cancel M = {mul := cancel_monoid_with_zero.mul _inst_3, mul_assoc := _, one := cancel_monoid_with_zero.one _inst_3, one_mul := _, mul_one := _, npow := cancel_monoid_with_zero.npow _inst_3, npow_zero' := _, npow_succ' := _, zero := cancel_monoid_with_zero.zero _inst_3, zero_mul := _, mul_zero := _, inv := λ (a : M), dite (a = 0) (λ (h : a = 0), 0) (λ (h : ¬a = 0), fintype.bij_inv _ 1), div := div_inv_monoid.div._default cancel_monoid_with_zero.mul cancel_monoid_with_zero.mul_assoc cancel_monoid_with_zero.one cancel_monoid_with_zero.one_mul cancel_monoid_with_zero.mul_one cancel_monoid_with_zero.npow cancel_monoid_with_zero.npow_zero' cancel_monoid_with_zero.npow_succ' (λ (a : M), dite (a = 0) (λ (h : a = 0), 0) (λ (h : ¬a = 0), fintype.bij_inv _ 1)), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default cancel_monoid_with_zero.mul cancel_monoid_with_zero.mul_assoc cancel_monoid_with_zero.one cancel_monoid_with_zero.one_mul cancel_monoid_with_zero.mul_one cancel_monoid_with_zero.npow cancel_monoid_with_zero.npow_zero' cancel_monoid_with_zero.npow_succ' (λ (a : M), dite (a = 0) (λ (h : a = 0), 0) (λ (h : ¬a = 0), fintype.bij_inv _ 1)), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

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

fintype.division_ring_of_is_domain R = {add := ring.add _inst_4, add_assoc := _, zero := group_with_zero.zero (show group_with_zero R, from fintype.group_with_zero_of_cancel R), zero_add := _, add_zero := _, nsmul := ring.nsmul _inst_4, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg _inst_4, sub := ring.sub _inst_4, sub_eq_add_neg := _, zsmul := ring.zsmul _inst_4, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := group_with_zero.mul (show group_with_zero R, from fintype.group_with_zero_of_cancel R), mul_assoc := _, one := group_with_zero.one (show group_with_zero R, from fintype.group_with_zero_of_cancel R), one_mul := _, mul_one := _, npow := group_with_zero.npow (show group_with_zero R, from fintype.group_with_zero_of_cancel R), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := group_with_zero.inv (show group_with_zero R, from fintype.group_with_zero_of_cancel R), div := group_with_zero.div (show group_with_zero R, from fintype.group_with_zero_of_cancel R), div_eq_mul_inv := _, zpow := group_with_zero.zpow (show group_with_zero R, from fintype.group_with_zero_of_cancel R), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

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

fintype.field_of_domain R = {add := comm_ring.add _inst_4, add_assoc := _, zero := group_with_zero.zero (fintype.group_with_zero_of_cancel R), zero_add := _, add_zero := _, nsmul := comm_ring.nsmul _inst_4, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg _inst_4, sub := comm_ring.sub _inst_4, sub_eq_add_neg := _, zsmul := comm_ring.zsmul _inst_4, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := group_with_zero.mul (fintype.group_with_zero_of_cancel R), mul_assoc := _, one := group_with_zero.one (fintype.group_with_zero_of_cancel R), one_mul := _, mul_one := _, npow := group_with_zero.npow (fintype.group_with_zero_of_cancel R), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := group_with_zero.inv (fintype.group_with_zero_of_cancel R), div := group_with_zero.div (fintype.group_with_zero_of_cancel R), div_eq_mul_inv := _, zpow := group_with_zero.zpow (fintype.group_with_zero_of_cancel R), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

source

theorem fintype.is_field_of_domain (R : Type u_1) [comm_ring R] [is_domain R] [fintype 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] [fintype 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] [fintype 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 fintype Rˣ rather than deducing it from fintype R.

source

@[protected, instance]

def subgroup_units_cyclic {R : Type u_1} [comm_ring R] [is_domain R] (S : subgroup Rˣ) [fintype ↥S] :

is_cyclic ↥S

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

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) :

∑ (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)] :

∑ (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.