Library Algebra.Ring.Ring_charac
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Support for the characteristic of rings.
Let K : Ring.
This module may be used through the import of Algebra.Ring.Ring,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
- ring_charac K is the characteristic of K, ie the smallest nonzero natural number n such that plusn1 n = 0, or 0 if no such number exists;
- is_field_not_charac_2 K states that K is a field of characteristic distinct from 2.
Used logic axioms
- classic, the weak form of excluded middle;
- ex_EX, an alias for constructive_indefinite_description.
Usage
From Requisite Require Import stdlib_wR ssr_wMC.
From Coquelicot Require Import Hierarchy Markov.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid Group Ring_compl Ring_FF_FT.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Section Ring_charac.
Lemma ring_charac_EX :
∀ K : Ring,
{ n | n ≠ 0%nat ∧ plusn1 K n = 0 ∧
∀ p, p ≠ 0%nat → (p < n)%coq_nat → plusn1 K p ≠ 0 } +
{ ∀ n, n ≠ 0%nat → plusn1 K n ≠ 0 }.
Proof.
intros; pose (P n := n ≠ 0%nat ∧ plusn1 K n = 0).
destruct (LPO P (fun⇒ classic _)) as [[N HN] | H]; [left | right].
apply ex_EX; destruct (dec_inh_nat_subset_has_unique_least_element P)
as [n [[Hn1 Hn2] _]]; [intros; apply classic | ∃ N; easy |].
∃ n; repeat split; try apply Hn1.
intros p Hp0; rewrite contra_not_r_equiv Nat.nlt_ge; intros Hp1.
apply Hn2; easy.
intros n; unfold P in H; specialize (H n); rewrite not_and_equiv in H.
destruct H; easy.
Qed.
Definition ring_charac (K : Ring) : nat :=
match ring_charac_EX K with
| inleft H ⇒ proj1_sig H
| inright _ ⇒ 0
end.
Definition is_field_not_charac_2 (K : Ring) : Prop :=
is_field K ∧ ring_charac K ≠ 2%nat.
Context {K : Ring}.
Lemma ring_charac_0 :
ring_charac K = 0%nat ↔ ∀ n, n ≠ 0%nat → plusn1 K n ≠ 0.
Proof.
unfold ring_charac;
destruct ring_charac_EX as [[n [Hn0 [Hn1 Hn2]]] | ]; simpl; try easy.
rewrite iff_not_equiv not_all_ex_not_equiv; split; try easy; intros _.
∃ n; rewrite -contra_equiv not_imp_and_equiv; easy.
Qed.
Lemma ring_charac_S :
∀ n, ring_charac K = n.+1 ↔
plusn n.+1 (1 : K) = 0 ∧
(∀ p, p ≠ 0%nat → (p < n.+1)%coq_nat → plusn1 K p ≠ 0).
Proof.
intros n; unfold ring_charac;
destruct ring_charac_EX as [[m [Hm0 [Hm1 Hm2]]] | H];
simpl; split; try (now intros; subst); intros [Hn1 Hn2].
destruct (nat_lt_eq_gt_dec m n.+1) as [[H | H] | H]; try easy.
contradict Hm1; apply Hn2; easy.
contradict Hn1; apply Hm2; easy.
contradict Hn1; apply H; easy.
Qed.
Lemma ring_charac_equiv :
∀ n, ring_charac K = n ↔
(∀ k, (∀ x : K, plusn k x = 0) ↔ k mod n = 0%nat).
Proof.
intros n; destruct n.
rewrite ring_charac_0; unfold Nat.modulo; split.
intros H k; split; intros Hk.
destruct k; try easy.
specialize (H k.+1); specialize (Hk 1); contradict Hk; auto.
intros; subst; apply plusn_0_l.
intros H n Hn; contradict Hn; apply H.
intros x; rewrite plusn_eq Hn mult_zero_l; easy.
rewrite ring_charac_S; split.
intros [Hn1 Hn2] k; split.
move⇒ /plusn_zero_equiv Hk0.
generalize (Nat.div_mod_eq k n.+1); intros Hk1.
rewrite Hk1 plusn1_eq plusn_distr_l plusn_assoc_r
Hn1 plusn_0_r plus_zero_l in Hk0.
apply NNPP_equiv; contradict Hk0; apply Hn2; try easy.
apply Nat.mod_upper_bound; easy.
move⇒ /Nat.Div0.div_exact Hk; apply plusn_zero_equiv; rewrite Hk; try lia.
unfold plusn1; rewrite plusn_assoc_r Hn1 plusn_0_r; easy.
intros Hn; split.
apply plusn_zero_equiv, Hn, Nat.Div0.mod_same; easy.
intros p Hp0 Hp1; contradict Hp0; rewrite -(Nat.mod_small _ _ Hp1).
apply Hn, plusn_zero_equiv; easy.
Qed.
Lemma ring_charac_1 : ring_charac K = 1%nat ↔ zero_struct K.
Proof.
rewrite -one_is_zero_equiv ring_charac_S plusn_1_l; split; try easy.
intros H; split; try easy.
intros p Hp0 Hp1; contradict Hp0; apply lt_1; easy.
Qed.
Lemma ring_charac_2 :
ring_charac K = 2%nat ↔ nonzero_struct K ∧ (2 : K) = 0.
Proof.
split; [intros HK | intros [HK0 HK1]; rewrite -plusn_2_1 in HK1].
split.
apply nonzero_not_zero_struct_equiv; contradict HK.
apply ring_charac_1 in HK; rewrite HK; easy.
rewrite ring_charac_equiv in HK.
rewrite -plusn1_2; apply plusn_zero_equiv, HK, Nat.Div0.mod_same; easy.
apply ring_charac_equiv; intros k; rewrite -plusn_zero_equiv; split; intros Hk.
assert (Hk1 : k mod 2 = 0%nat ∨ k mod 2 = 1%nat)
by now apply lt_2, Nat.mod_upper_bound.
destruct Hk1 as [Hk1 | Hk1]; try easy; contradict Hk.
generalize (Nat.div_mod_eq k 2); intros Hk2; rewrite Hk2.
rewrite plusn1_eq plusn_distr_l plusn_assoc_r HK1 plusn_0_r plus_zero_l Hk1 plusn_1_l.
apply one_not_zero; easy.
apply Nat.Div0.div_exact in Hk; try easy; rewrite Hk.
rewrite plusn1_eq plusn_assoc_r HK1 plusn_0_r; easy.
Qed.
Lemma invertible_plusn :
∀ n, nonzero_struct K → n ≠ 0%nat →
invertible (plusn1 K n) → ring_charac K ≠ n.
Proof.
intros n HK0 Hn HK1; contradict Hn; destruct n; try easy; contradict HK1.
apply ring_charac_S in Hn; rewrite plusn1_eq (proj1 Hn).
apply noninvertible_zero; easy.
Qed.
End Ring_charac.