Integral domains

Assorted theorems about integral domains.

Main theorems

is_cyclic_of_subgroup_integral_domain : A finite subgroup of the units of an integral domain is cyclic.
field_of_integral_domain : A finite integral domain is a field.

Tags

integral domain, finite integral domain, finite field

theorem card_nth_roots_subgroup_units {R : Type u_1} {G : Type u_2} [integral_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 ≤ (polynomial.nth_roots n (⇑f g₀)).card

source

theorem is_cyclic_of_subgroup_integral_domain {R : Type u_1} {G : Type u_2} [integral_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

@[instance]

def units.is_cyclic {R : Type u_1} [integral_domain R] [fintype R] :

is_cyclic (units R)

The unit group of a finite integral domain is cyclic.

source

def field_of_integral_domain {R : Type u_1} [integral_domain R] [decidable_eq R] [fintype R] :

field R

Every finite integral domain is a field.

Equations

field_of_integral_domain = {add := integral_domain.add (show integral_domain R, from _inst_1), add_assoc := _, zero := integral_domain.zero (show integral_domain R, from _inst_1), zero_add := _, add_zero := _, neg := integral_domain.neg (show integral_domain R, from _inst_1), add_left_neg := _, add_comm := _, mul := integral_domain.mul (show integral_domain R, from _inst_1), mul_assoc := _, one := integral_domain.one (show integral_domain R, from _inst_1), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := λ (a : R), dite (a = 0) (λ (h : a = 0), 0) (λ (h : ¬a = 0), fintype.bij_inv _ 1), exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

source

@[instance]

def subgroup_units_cyclic {R : Type u_1} [integral_domain R] (S : set (units R)) [is_subgroup S] [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} [integral_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} [integral_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.