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.field_of_is_domain
: A finite integral domain is a field.
Tags #
integral domain, finite integral domain, finite field
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)
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)
def
group_with_zero_of_fintype
(M : Type u_1)
[cancel_monoid_with_zero M]
[decidable_eq M]
[fintype M]
[nontrivial M] :
Every finite nontrivial cancel_monoid_with_zero is a group_with_zero.
Equations
- group_with_zero_of_fintype 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 := _}
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
- division_ring_of_is_domain R = {add := ring.add _inst_4, add_assoc := _, zero := group_with_zero.zero (show group_with_zero R, from group_with_zero_of_fintype 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 group_with_zero_of_fintype R), mul_assoc := _, one := group_with_zero.one (show group_with_zero R, from group_with_zero_of_fintype R), one_mul := _, mul_one := _, npow := group_with_zero.npow (show group_with_zero R, from group_with_zero_of_fintype R), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := group_with_zero.inv (show group_with_zero R, from group_with_zero_of_fintype R), div := group_with_zero.div (show group_with_zero R, from group_with_zero_of_fintype R), div_eq_mul_inv := _, zpow := group_with_zero.zpow (show group_with_zero R, from group_with_zero_of_fintype R), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
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₀))
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.
def
field_of_is_domain
{R : Type u_1}
[comm_ring R]
[is_domain R]
[decidable_eq R]
[fintype R] :
field R
Every finite integral domain is a field.
Equations
- field_of_is_domain = {add := division_ring.add (division_ring_of_is_domain R), add_assoc := _, zero := division_ring.zero (division_ring_of_is_domain R), zero_add := _, add_zero := _, nsmul := division_ring.nsmul (division_ring_of_is_domain R), nsmul_zero' := _, nsmul_succ' := _, neg := division_ring.neg (division_ring_of_is_domain R), sub := division_ring.sub (division_ring_of_is_domain R), sub_eq_add_neg := _, zsmul := division_ring.zsmul (division_ring_of_is_domain R), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := division_ring.mul (division_ring_of_is_domain R), mul_assoc := _, one := division_ring.one (division_ring_of_is_domain R), one_mul := _, mul_one := _, npow := division_ring.npow (division_ring_of_is_domain R), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := division_ring.inv (division_ring_of_is_domain R), div := division_ring.div (division_ring_of_is_domain R), div_eq_mul_inv := _, zpow := division_ring.zpow (division_ring_of_is_domain R), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
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
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)] :
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.