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.

Brief description

Support for the characteristic of rings.

Description

Let K : Ring.
  • 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

Usage

This module may be used through the import of Algebra.Ring.Ring, Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.

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 Hproj1_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.