mathlibdocumentation

ring_theory.integral_domain

Integral domains #

Main theorems #

• is_cyclic_of_subgroup_is_domain : A finite subgroup of the units of an integral domain is cyclic.
• field_of_is_domain : A finite integral domain is a field.

Tags #

integral domain, finite integral domain, finite field

theorem mul_right_bijective₀ {R : Type u_1} [ring R] [is_domain R] [fintype R] (a : R) (ha : a 0) :
function.bijective (λ (b : R), a * b)
theorem mul_left_bijective₀ {R : Type u_1} [ring R] [is_domain R] [fintype R] (a : R) (ha : a 0) :
function.bijective (λ (b : R), b * a)
def division_ring_of_is_domain (R : Type u_1) [ring R] [is_domain R] [decidable_eq R] [fintype 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
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 (f g₀))
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) :

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

@[instance]
def units.is_cyclic {R : Type u_1} [comm_ring R] [is_domain R] [fintype (units R)] :

The unit group of a finite integral domain is cyclic.

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

def field_of_is_domain {R : Type u_1} [comm_ring R] [is_domain R] [decidable_eq R] [fintype R] :

Every finite integral domain is a field.

Equations
@[instance]
def subgroup_units_cyclic {R : Type u_1} [comm_ring R] [is_domain R] (S : subgroup (units R)) [fintype S] :

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

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 ) (hy : y ) :
(finset.filter (λ (g : G), f g = x) finset.univ).card = (finset.filter (λ (g : G), f g = y) finset.univ).card
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.

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.