Require Import WildCat.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic.
(* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *)
Require Import Classes.interfaces.abstract_algebra.
Require Import Algebra.Groups.Group Algebra.Groups.Subgroup.
Require Export Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct Algebra.AbGroups.FiniteSum.

Require Export Classes.theory.rings.
Require Import Modalities.ReflectiveSubuniverse.

(** We make sure to treat [AbGroup] as if it has a [Plus], [Zero], and [Negate] operation from now on. *)
Export AbelianGroup.AdditiveInstances.

(** * Rings *)

Declare Scope ring_scope.

Local Open Scope ring_scope.
(** We want to print equivalences as [≅]. *)
Local Open Scope wc_iso_scope.

(** A ring consists of the following data: *)
Record Ring := Build_Ring' {
  (** An underlying abelian group. *)
  ring_abgroup :> AbGroup;
  (** A multiplication operation. *)
  ring_mult :: Mult ring_abgroup;
  (** A multiplicative identity called [one]. *)
  ring_one :: One ring_abgroup;
  (** Such that all they all satisfy the axioms of a ring. *)
  ring_isring :: IsRing ring_abgroup;
  (** This field only exists so that opposite rings are definitionally involutive and can safely be ignored. *)
  ring_mult_assoc_opp : forall z y x, (x * y) * z = x * (y * z);
}.

Arguments ring_mult {R} : rename.
Arguments ring_one {R} : rename.
Arguments ring_isring {R} : rename.

Definition issig_Ring : _ <~> Ring := ltac:(issig).

Instance ring_plus {R : Ring} : Plus R := plus_abgroup (ring_abgroup R).
Instance ring_zero {R : Ring} : Zero R := zero_abgroup (ring_abgroup R).
Instance ring_negate {R : Ring} : Negate R := negate_abgroup (ring_abgroup R).

(** A ring homomorphism between rings is a map of the underlying type and a proof that this map is a ring homomorphism. *)
Record RingHomomorphism (A B : Ring) := {
  rng_homo_map :> A -> B;
  rng_homo_ishomo :: IsSemiRingPreserving rng_homo_map;
}.

Arguments Build_RingHomomorphism {_ _} _ _.

Definition issig_RingHomomorphism (A B : Ring)
  : _ <~> RingHomomorphism A B
  := ltac:(issig).

Definition equiv_path_ringhomomorphism `{Funext} {A B : Ring}
  {f g : RingHomomorphism A B} : f == g <~> f = g.
H: Funext
A, B: Ring
f, g: RingHomomorphism A B
f == g <~> f = g
Proof.
H: Funext
A, B: Ring
f, g: RingHomomorphism A B
f == g <~> f = g
  refine ((equiv_ap (issig_RingHomomorphism A B)^-1 _ _)^-1 oE _).
H: Funext
A, B: Ring
f, g: RingHomomorphism A B
f == g <~>
(issig_RingHomomorphism A B)^-1 f =
(issig_RingHomomorphism A B)^-1 g
  refine (equiv_path_sigma_hprop _ _ oE _).
H: Funext
A, B: Ring
f, g: RingHomomorphism A B
f == g <~>
((issig_RingHomomorphism A B)^-1 f).1 =
((issig_RingHomomorphism A B)^-1 g).1
  apply equiv_path_forall.
Defined.

Definition rng_homo_id (A : Ring) : RingHomomorphism A A
  := Build_RingHomomorphism idmap (Build_IsSemiRingPreserving _ _ _).

Definition rng_homo_compose {A B C : Ring}
  (f : RingHomomorphism B C) (g : RingHomomorphism A B)
  : RingHomomorphism A C.
A, B, C: Ring
f: RingHomomorphism B C
g: RingHomomorphism A B
RingHomomorphism A C
Proof.
A, B, C: Ring
f: RingHomomorphism B C
g: RingHomomorphism A B
RingHomomorphism A C
  snapply Build_RingHomomorphism.
A, B, C: Ring
f: RingHomomorphism B C
g: RingHomomorphism A B
A -> C
A, B, C: Ring
f: RingHomomorphism B C
g: RingHomomorphism A B
IsSemiRingPreserving ?rng_homo_map
  1: exact (f o g).
A, B, C: Ring
f: RingHomomorphism B C
g: RingHomomorphism A B
IsSemiRingPreserving (f o g)
  rapply compose_sr_morphism.
Defined.

(** ** Ring laws *)

Section RingLaws.

  (** Many of these ring laws have already been proven. But we give them names here so that they are easy to find and use. *)

  Context {A : Ring} (x y z : A).

  Definition rng_dist_l : x * (y + z) = x * y + x * z := simple_distribute_l _ _ _.
  Definition rng_dist_r : (x + y) * z = x * z + y * z := simple_distribute_r _ _ _.
  Definition rng_plus_zero_l : 0 + x = x := left_identity _.
  Definition rng_plus_zero_r : x + 0 = x := right_identity _.
  Definition rng_plus_negate_l : (- x) + x = 0 := left_inverse _.
  Definition rng_plus_negate_r : x + (- x) = 0 := right_inverse _.

  Definition rng_plus_comm : x + y = y + x := commutativity x y.
  Definition rng_plus_assoc : x + (y + z) = (x + y) + z := simple_associativity x y z.
  Definition rng_mult_assoc : x * (y * z) = (x * y) * z := simple_associativity x y z.

  Definition rng_negate_negate : - (- x) = x := groups.inverse_involutive _.
  Definition rng_negate_zero : - (0 : A) = 0 := groups.inverse_mon_unit.
  Definition rng_negate_plus : - (x + y) = - x - y := negate_plus_distr _ _.

  Definition rng_mult_one_l : 1 * x = x := left_identity _.
  Definition rng_mult_one_r : x * 1 = x := right_identity _.
  Definition rng_mult_zero_l : 0 * x = 0 := left_absorb _.
  Definition rng_mult_zero_r : x * 0 = 0 := right_absorb _.
  Definition rng_mult_negate : -1 * x = - x := (negate_mult_l _)^.
  Definition rng_mult_negate_negate : -x * -y = x * y := negate_mult_negate _ _.
  Definition rng_mult_negate_l : -x * y = -(x * y) := inverse (negate_mult_distr_l _ _).
  Definition rng_mult_negate_r : x * -y = -(x * y) := inverse (negate_mult_distr_r _ _).

End RingLaws.

Definition rng_dist_l_negate {A : Ring} (x y z : A)
  : x * (y - z) = x * y - x * z.
A: Ring
x, y, z: A
x * (y - z) = x * y - x * z
Proof.
A: Ring
x, y, z: A
x * (y - z) = x * y - x * z
  lhs napply rng_dist_l.
A: Ring
x, y, z: A
x * y + x * - z = x * y - x * z
  napply ap.
A: Ring
x, y, z: A
x * - z = - (x * z)
  napply rng_mult_negate_r.
Defined.

Definition rng_dist_r_negate {A : Ring} (x y z : A)
  : (x - y) * z = x * z - y * z.
A: Ring
x, y, z: A
(x - y) * z = x * z - y * z
Proof.
A: Ring
x, y, z: A
(x - y) * z = x * z - y * z
  lhs napply rng_dist_r.
A: Ring
x, y, z: A
x * z + - y * z = x * z - y * z
  napply ap.
A: Ring
x, y, z: A
- y * z = - (y * z)
  napply rng_mult_negate_l.
Defined.

Section RingHomoLaws.

  Context {A B : Ring} (f : RingHomomorphism A B) (x y : A).

  Definition rng_homo_plus : f (x + y) = f x + f y := preserves_plus x y.
  Definition rng_homo_mult : f (x * y) = f x * f y := preserves_mult x y.
  Definition rng_homo_zero : f 0 = 0 := preserves_0.
  Definition rng_homo_one  : f 1 = 1 := preserves_1.
  Definition rng_homo_negate : f (-x) = -(f x) := preserves_negate x.

  Definition rng_homo_minus_one : f (-1) = -1
    := preserves_negate _ @ ap negate preserves_1.

End RingHomoLaws.

(** Isomorphisms of commutative rings *)
Record RingIsomorphism (A B : Ring) := {
  rng_iso_homo : RingHomomorphism A B ;
  isequiv_rng_iso_homo :: IsEquiv rng_iso_homo ;
}.

Arguments rng_iso_homo {_ _ }.
Coercion rng_iso_homo : RingIsomorphism >-> RingHomomorphism.

Definition issig_RingIsomorphism {A B : Ring}
  : _ <~> RingIsomorphism A B := ltac:(issig).

(** We can construct a ring isomorphism from an equivalence that preserves addition and multiplication. *)
Definition Build_RingIsomorphism' (A B : Ring) (e : A <~> B)
  `{!IsSemiRingPreserving e}
  : RingIsomorphism A B
  := Build_RingIsomorphism A B (Build_RingHomomorphism e _) _.

(** The inverse of a Ring isomorphism *)
Definition rng_iso_inverse {A B : Ring}
  : RingIsomorphism A B -> RingIsomorphism B A.
A, B: Ring
RingIsomorphism A B -> RingIsomorphism B A
Proof.
A, B: Ring
RingIsomorphism A B -> RingIsomorphism B A
  intros [f e].
A, B: Ring
f: RingHomomorphism A B
e: IsEquiv f
RingIsomorphism B A
  snapply Build_RingIsomorphism.
A, B: Ring
f: RingHomomorphism A B
e: IsEquiv f
RingHomomorphism B A
A, B: Ring
f: RingHomomorphism A B
e: IsEquiv f
IsEquiv ?rng_iso_homo
  {
A, B: Ring
f: RingHomomorphism A B
e: IsEquiv f
RingHomomorphism B A snapply Build_RingHomomorphism.
A, B: Ring
f: RingHomomorphism A B
e: IsEquiv f
B -> A
A, B: Ring
f: RingHomomorphism A B
e: IsEquiv f
IsSemiRingPreserving ?rng_homo_map
    1: exact f^-1.
A, B: Ring
f: RingHomomorphism A B
e: IsEquiv f
IsSemiRingPreserving f^-1
    exact _. }
A, B: Ring
f: RingHomomorphism A B
e: IsEquiv f
IsEquiv
  {|
    rng_homo_map := f^-1;
    rng_homo_ishomo :=
      invert_sr_morphism f (rng_homo_ishomo A B f)
  |}
  exact _.
Defined.

(** Ring isomorphisms are a reflexive relation *)
Instance reflexive_ringisomorphism : Reflexive RingIsomorphism
  := fun x => Build_RingIsomorphism _ _ (rng_homo_id x) _.

(** Ring isomorphisms are a symmetric relation *)
Instance symmetry_ringisomorphism : Symmetric RingIsomorphism
  := fun x y => rng_iso_inverse.

(** Ring isomorphisms are a transitive relation *)
Instance transitive_ringisomorphism : Transitive RingIsomorphism
  := fun x y z f g => Build_RingIsomorphism _ _ (rng_homo_compose g f) _.

(** Underlying group homomorphism of a ring homomorphism *)
Definition grp_homo_rng_homo {R S : Ring}
  : RingHomomorphism R S -> GroupHomomorphism R S
  := fun f => @Build_GroupHomomorphism R S f _.

Coercion grp_homo_rng_homo : RingHomomorphism >-> GroupHomomorphism.

(** We can construct a ring homomorphism from a group homomorphism that preserves multiplication *)
Definition Build_RingHomomorphism' (A B : Ring) (map : GroupHomomorphism A B)
  {H : IsMonoidPreserving (Aop:=ring_mult) (Bop:=ring_mult)
    (Aunit:=one) (Bunit:=one) map}
  : RingHomomorphism A B
  := Build_RingHomomorphism map
      (Build_IsSemiRingPreserving _ (ismonoidpreserving_grp_homo map) H).

(** We can construct a ring isomorphism from a group isomorphism that preserves multiplication *)
Definition Build_RingIsomorphism'' (A B : Ring) (e : GroupIsomorphism A B)
  {H : IsMonoidPreserving (Aop:=ring_mult) (Bop:=ring_mult) (Aunit:=one) (Bunit:=one) e}
  : RingIsomorphism A B
  := @Build_RingIsomorphism' A B e (Build_IsSemiRingPreserving e _ H).

(** Here is an alternative way to build a ring using the underlying abelian group. *)
Definition Build_Ring (R : AbGroup)
  `(Mult R, One R, !Associative (.*.),
    !LeftDistribute (.*.) (+), !RightDistribute (.*.) (+),
    !LeftIdentity (.*.) 1, !RightIdentity (.*.) 1)
  : Ring.
R: AbGroup
H: Mult R
H0: One R
Associative0: Associative mult
LeftDistribute0: LeftDistribute mult plus
RightDistribute0: RightDistribute mult plus
LeftIdentity0: LeftIdentity mult 1
RightIdentity0: RightIdentity mult 1
Ring
Proof.
R: AbGroup
H: Mult R
H0: One R
Associative0: Associative mult
LeftDistribute0: LeftDistribute mult plus
RightDistribute0: RightDistribute mult plus
LeftIdentity0: LeftIdentity mult 1
RightIdentity0: RightIdentity mult 1
Ring
  rapply (Build_Ring' R).
R: AbGroup
H: Mult R
H0: One R
Associative0: Associative mult
LeftDistribute0: LeftDistribute mult plus
RightDistribute0: RightDistribute mult plus
LeftIdentity0: LeftIdentity mult 1
RightIdentity0: RightIdentity mult 1
IsRing R
R: AbGroup
H: Mult R
H0: One R
Associative0: Associative mult
LeftDistribute0: LeftDistribute mult plus
RightDistribute0: RightDistribute mult plus
LeftIdentity0: LeftIdentity mult 1
RightIdentity0: RightIdentity mult 1
forall z y x : R, x * y * z = x * (y * z)
  2: exact (fun z y x => (associativity x y z)^).
R: AbGroup
H: Mult R
H0: One R
Associative0: Associative mult
LeftDistribute0: LeftDistribute mult plus
RightDistribute0: RightDistribute mult plus
LeftIdentity0: LeftIdentity mult 1
RightIdentity0: RightIdentity mult 1
IsRing R
  split; only 1,3,4: exact _.
R: AbGroup
H: Mult R
H0: One R
Associative0: Associative mult
LeftDistribute0: LeftDistribute mult plus
RightDistribute0: RightDistribute mult plus
LeftIdentity0: LeftIdentity mult 1
RightIdentity0: RightIdentity mult 1
IsMonoid R
  repeat split; exact _.
Defined.

(** Scalar multiplication on the left is a group homomorphism. *)
Definition grp_homo_rng_left_mult {R : Ring} (r : R)
  : GroupHomomorphism R R
  := @Build_GroupHomomorphism R R (fun s => r * s) (rng_dist_l r).

(** Scalar multiplication on the right is a group homomorphism. *)
Definition grp_homo_rng_right_mult {R : Ring} (r : R)
  : GroupHomomorphism R R
  := @Build_GroupHomomorphism R R (fun s => s * r) (fun x y => rng_dist_r x y r).

(** ** Ring movement lemmas *)

Section RingMovement.

  (** We adopt a similar naming convention to the [moveR_equiv] style lemmas that can be found in Types.Paths. *)

  Context {R : Ring} {x y z : R}.

  Definition rng_moveL_Mr : - y + x = z <~> x = y + z := @grp_moveL_Mg R x y z.
  Definition rng_moveL_rM : x + - z = y <~> x = y + z := @grp_moveL_gM R x y z.
  Definition rng_moveR_Mr : y = - x + z <~> x + y = z := @grp_moveR_Mg R x y z.
  Definition rng_moveR_rM : x = z + - y <~> x + y = z := @grp_moveR_gM R x y z.

  Definition rng_moveL_Vr : x + y = z <~> y = - x + z := @grp_moveL_Vg R x y z.
  Definition rng_moveL_rV : x + y = z <~> x = z + - y := @grp_moveL_gV R x y z.
  Definition rng_moveR_Vr : x = y + z <~> - y + x = z := @grp_moveR_Vg R x y z.
  Definition rng_moveR_rV : x = y + z <~> x + - z = y := @grp_moveR_gV R x y z.

  Definition rng_moveL_M0 : - y + x = 0 <~> x = y := @grp_moveL_M1 R x y.
  Definition rng_moveL_0M :	x + - y = 0 <~> x = y := @grp_moveL_1M R x y.
  Definition rng_moveR_M0 : 0 = - x + y <~> x = y := @grp_moveR_M1 R x y.
  Definition rng_moveR_0M : 0 = y + - x <~> x = y := @grp_moveR_1M R x y.

  (** TODO: Movement laws about [mult] *)

End RingMovement.

(** ** Wild category of rings *)

Instance isgraph_ring : IsGraph Ring
  := Build_IsGraph _ RingHomomorphism.

Instance is01cat_ring : Is01Cat Ring
  := Build_Is01Cat _ _ rng_homo_id (@rng_homo_compose).

Instance is2graph_ring : Is2Graph Ring
  := fun A B => isgraph_induced (@rng_homo_map A B : _ -> (group_type _ $-> _)).

Instance is01cat_ringhomomorphism {A B : Ring} : Is01Cat (A $-> B)
  := is01cat_induced (@rng_homo_map A B).

Instance is0gpd_ringhomomorphism {A B : Ring} : Is0Gpd (A $-> B)
  := is0gpd_induced (@rng_homo_map A B).

Instance is0functor_postcomp_ringhomomorphism {A B C : Ring} (h : B $-> C)
  : Is0Functor (@cat_postcomp Ring _ _ A B C h).
A, B, C: Ring
h: B $-> C
Is0Functor (cat_postcomp A h)
Proof.
A, B, C: Ring
h: B $-> C
Is0Functor (cat_postcomp A h)
  apply Build_Is0Functor.
A, B, C: Ring
h: B $-> C
forall a b : A $-> B,
(a $-> b) -> cat_postcomp A h a $-> cat_postcomp A h b
  intros [f ?] [g ?] p a ; exact (ap h (p a)).
Defined.

Instance is0functor_precomp_ringhomomorphism
       {A B C : Ring} (h : A $-> B)
  : Is0Functor (@cat_precomp Ring _ _ A B C h).
A, B, C: Ring
h: A $-> B
Is0Functor (cat_precomp C h)
Proof.
A, B, C: Ring
h: A $-> B
Is0Functor (cat_precomp C h)
  apply Build_Is0Functor.
A, B, C: Ring
h: A $-> B
forall a b : B $-> C,
(a $-> b) -> cat_precomp C h a $-> cat_precomp C h b
  intros [f ?] [g ?] p a ; exact (p (h a)).
Defined.

(** Ring forms a 1-category. *)
Instance is1cat_ring : Is1Cat Ring.
Is1Cat Ring
Proof.
Is1Cat Ring
  by rapply Build_Is1Cat.
Defined.

Instance hasmorext_ring `{Funext} : HasMorExt Ring.
H: Funext
HasMorExt Ring
Proof.
H: Funext
HasMorExt Ring
  intros A B f g; cbn in *.
H: Funext
A, B: Ring
f, g: RingHomomorphism A B
IsEquiv GpdHom_path
  snapply @isequiv_homotopic.
H: Funext
A, B: Ring
f, g: RingHomomorphism A B
f = g -> f == g
H: Funext
A, B: Ring
f, g: RingHomomorphism A B
IsEquiv ?f
H: Funext
A, B: Ring
f, g: RingHomomorphism A B
?f == GpdHom_path
  1: exact (equiv_path_ringhomomorphism^-1%equiv).
H: Funext
A, B: Ring
f, g: RingHomomorphism A B
IsEquiv equiv_path_ringhomomorphism^-1%equiv
H: Funext
A, B: Ring
f, g: RingHomomorphism A B
equiv_path_ringhomomorphism^-1%equiv == GpdHom_path
  1: exact _.
H: Funext
A, B: Ring
f, g: RingHomomorphism A B
equiv_path_ringhomomorphism^-1%equiv == GpdHom_path
  intros []; reflexivity. 
Defined.

Instance hasequivs_ring : HasEquivs Ring.
HasEquivs Ring
Proof.
HasEquivs Ring
  unshelve econstructor.
Ring -> Ring -> Type
forall a b : Ring, (a $-> b) -> Type
forall a b : Ring, ?CatEquiv' a b -> a $-> b
forall (a b : Ring) (f : a $-> b),
?CatIsEquiv' a b f -> ?CatEquiv' a b
forall a b : Ring, ?CatEquiv' a b -> b $-> a
forall (a b : Ring) (f : ?CatEquiv' a b),
?CatIsEquiv' a b (?cate_fun' a b f)
forall (a b : Ring) (f : a $-> b)
(fe : ?CatIsEquiv' a b f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
forall (a b : Ring) (f : ?CatEquiv' a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
forall (a b : Ring) (f : ?CatEquiv' a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
forall (a b : Ring) (f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> ?CatIsEquiv' a b f
  +
Ring -> Ring -> Type exact RingIsomorphism.
  +
forall a b : Ring, (a $-> b) -> Type exact (fun G H f => IsEquiv f).
  +
forall a b : Ring, RingIsomorphism a b -> a $-> b intros G H f; exact f.
  +
forall (a b : Ring) (f : a $-> b),
(fun (G H : Ring) (f0 : G $-> H) => IsEquiv f0) a b f ->
RingIsomorphism a b exact Build_RingIsomorphism.
  +
forall a b : Ring, RingIsomorphism a b -> b $-> a intros G H; exact rng_iso_inverse.
  +
forall (a b : Ring) (f : RingIsomorphism a b),
(fun (G H : Ring) (f0 : G $-> H) => IsEquiv f0) a b
  ((fun (G H : Ring) (f0 : RingIsomorphism G H) =>
    rng_iso_homo f0) a b f) cbn; exact _.
  +
forall (a b : Ring) (f : a $-> b)
(fe : (fun (G H : Ring) (f0 : G $-> H) => IsEquiv f0)
        a b f),
(fun (G H : Ring) (f0 : RingIsomorphism G H) =>
 rng_iso_homo f0) a b
  {| rng_iso_homo := f; isequiv_rng_iso_homo := fe |} $==
f reflexivity.
  +
forall (a b : Ring) (f : RingIsomorphism a b),
(fun (G H : Ring) (x : RingIsomorphism G H) =>
 rng_iso_homo (rng_iso_inverse x)) a b f $o
(fun (G H : Ring) (f0 : RingIsomorphism G H) =>
 rng_iso_homo f0) a b f $== Id a intros ????; apply eissect.
  +
forall (a b : Ring) (f : RingIsomorphism a b),
(fun (G H : Ring) (f0 : RingIsomorphism G H) =>
 rng_iso_homo f0) a b f $o
(fun (G H : Ring) (x : RingIsomorphism G H) =>
 rng_iso_homo (rng_iso_inverse x)) a b f $== Id b intros ????; apply eisretr.
  +
forall (a b : Ring) (f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a ->
(fun (G H : Ring) (f0 : G $-> H) => IsEquiv f0) a b f intros G H f g p q.
G, H: Ring
f: G $-> H
g: H $-> G
p: f $o g $== Id H
q: g $o f $== Id G
(fun (G H : Ring) (f : G $-> H) => IsEquiv f) G H f
    exact (isequiv_adjointify f g p q).
Defined.

(** ** Subrings *)

(** TODO: factor out this definition as a submonoid *)
(** A subring is a subgroup of the underlying abelian group of a ring that is closed under multiplication and contains [1]. *)
Class IsSubring {R : Ring} (S : R -> Type) := {
  issubring_issubgroup :: IsSubgroup S;
  issubring_mult {x y} : S x -> S y -> S (x * y);
  issubring_one : S 1;
}.

Definition issig_IsSubring {R : Ring} (S : R -> Type)
  : _ <~> IsSubring S
  := ltac:(issig).

Instance ishprop_issubring `{Funext} {R : Ring} (S : R -> Type)
  : IsHProp (IsSubring S).
H: Funext
R: Ring
S: R -> Type
IsHProp (IsSubring S)
Proof.
H: Funext
R: Ring
S: R -> Type
IsHProp (IsSubring S)
  exact (istrunc_equiv_istrunc _ (issig_IsSubring S)).
Defined.

(** Subring criterion. *)
Definition Build_IsSubring' {R : Ring} (S : R -> Type)
  (H : forall x, IsHProp (S x))
  (H1 : forall x y, S x -> S y -> S (x - y))
  (H2 : forall x y, S x -> S y -> S (x * y))
  (H3 : S 1)
  : IsSubring S.
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
IsSubring S
Proof.
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
IsSubring S
  snapply Build_IsSubring.
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
IsSubgroup S
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
forall x y : R, S x -> S y -> S (x * y)
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
S 1
  -
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
IsSubgroup S snapply Build_IsSubgroup'.
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
forall x : R, IsHProp (S x)
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
S mon_unit
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
forall x y : R, S x -> S y -> S (sg_op x (inv y))
    +
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
forall x : R, IsHProp (S x) exact _.
    +
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
S mon_unit pose (p := H1 1 1 H3 H3).
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
p:= H1 1 1 H3 H3: S (1 - 1)
S mon_unit
      rewrite rng_plus_negate_r in p.
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
p: S 0
S mon_unit
      exact p.
    +
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
forall x y : R, S x -> S y -> S (sg_op x (inv y)) exact H1.
  -
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
forall x y : R, S x -> S y -> S (x * y) exact H2.
  -
R: Ring
S: R -> Type
H: forall x : R, IsHProp (S x)
H1: forall x y : R, S x -> S y -> S (x - y)
H2: forall x y : R, S x -> S y -> S (x * y)
H3: S 1
S 1 exact H3.
Defined.

Record Subring (R : Ring) := {
  #[reversible=no]
  subring_pred :> R -> Type;
  subring_issubring :: IsSubring subring_pred;
}.

Definition Build_Subring'' {R : Ring} (S : Subgroup R)
  (H1 : forall x y, S x -> S y -> S (x * y))
  (H2 : S 1)
  : Subring R.
R: Ring
S: Subgroup R
H1: forall x y : R, S x -> S y -> S (x * y)
H2: S 1
Subring R
Proof.
R: Ring
S: Subgroup R
H1: forall x y : R, S x -> S y -> S (x * y)
H2: S 1
Subring R
  snapply (Build_Subring _ S).
R: Ring
S: Subgroup R
H1: forall x y : R, S x -> S y -> S (x * y)
H2: S 1
IsSubring S
  snapply Build_IsSubring.
R: Ring
S: Subgroup R
H1: forall x y : R, S x -> S y -> S (x * y)
H2: S 1
IsSubgroup S
R: Ring
S: Subgroup R
H1: forall x y : R, S x -> S y -> S (x * y)
H2: S 1
forall x y : R, S x -> S y -> S (x * y)
R: Ring
S: Subgroup R
H1: forall x y : R, S x -> S y -> S (x * y)
H2: S 1
S 1
  -
R: Ring
S: Subgroup R
H1: forall x y : R, S x -> S y -> S (x * y)
H2: S 1
IsSubgroup S exact _.
  -
R: Ring
S: Subgroup R
H1: forall x y : R, S x -> S y -> S (x * y)
H2: S 1
forall x y : R, S x -> S y -> S (x * y) exact H1.
  -
R: Ring
S: Subgroup R
H1: forall x y : R, S x -> S y -> S (x * y)
H2: S 1
S 1 exact H2.
Defined.

Definition Build_Subring' {R : Ring} (S : R -> Type)
  (H : forall x, IsHProp (S x))
  (H1 : forall x y, S x -> S y -> S (x - y))
  (H2 : forall x y, S x -> S y -> S (x * y))
  (H3 : S 1)
  : Subring R
  := Build_Subring R S (Build_IsSubring' S H H1 H2 H3).

(** The underlying subgroup of a subring. *)
Coercion subgroup_subring {R} : Subring R -> Subgroup R
  := fun S => Build_Subgroup R S _.

(** The ring given by a subring. *)
Coercion ring_subring {R : Ring} (S : Subring R) : Ring.
R: Ring
S: Subring R
Ring
Proof.
R: Ring
S: Subring R
Ring
  snapply (Build_Ring (subgroup_subring S)).
R: Ring
S: Subring R
Mult S
R: Ring
S: Subring R
One S
R: Ring
S: Subring R
Associative mult
R: Ring
S: Subring R
LeftDistribute mult plus
R: Ring
S: Subring R
RightDistribute mult plus
R: Ring
S: Subring R
LeftIdentity mult 1
R: Ring
S: Subring R
RightIdentity mult 1
  3-7: hnf; intros; srapply path_sigma_hprop.
R: Ring
S: Subring R
Mult S
R: Ring
S: Subring R
One S
R: Ring
S: Subring R
x, y, z: S
(x * (y * z)).1 = (x * y * z).1
R: Ring
S: Subring R
a, b, c: S
(a * (b + c)).1 = (a * b + a * c).1
R: Ring
S: Subring R
a, b, c: S
((a + b) * c).1 = (a * c + b * c).1
R: Ring
S: Subring R
y: S
(1 * y).1 = y.1
R: Ring
S: Subring R
x: S
(x * 1).1 = x.1
  -
R: Ring
S: Subring R
Mult S intros [r ?] [s ?]; exists (r * s).
R: Ring
S: Subring R
r: R
proj2: S r
s: R
proj0: S s
S (r * s)
    by apply issubring_mult.
  -
R: Ring
S: Subring R
One S exists 1.
R: Ring
S: Subring R
S 1
    exact issubring_one.
  -
R: Ring
S: Subring R
x, y, z: S
(x * (y * z)).1 = (x * y * z).1 napply rng_mult_assoc.
  -
R: Ring
S: Subring R
a, b, c: S
(a * (b + c)).1 = (a * b + a * c).1 napply rng_dist_l.
  -
R: Ring
S: Subring R
a, b, c: S
((a + b) * c).1 = (a * c + b * c).1 napply rng_dist_r.
  -
R: Ring
S: Subring R
y: S
(1 * y).1 = y.1 napply rng_mult_one_l.
  -
R: Ring
S: Subring R
x: S
(x * 1).1 = x.1 napply rng_mult_one_r.
Defined.

(** ** Product ring *)

Definition ring_product : Ring -> Ring -> Ring.
Ring -> Ring -> Ring
Proof.
Ring -> Ring -> Ring
  intros R S.
R, S: Ring
Ring
  snapply Build_Ring.
R, S: Ring
AbGroup
R, S: Ring
Mult ?R
R, S: Ring
One ?R
R, S: Ring
Associative mult
R, S: Ring
LeftDistribute mult plus
R, S: Ring
RightDistribute mult plus
R, S: Ring
LeftIdentity mult 1
R, S: Ring
RightIdentity mult 1
  -
R, S: Ring
AbGroup exact (ab_biprod R S).
  -
R, S: Ring
Mult (ab_biprod R S) exact (fun '(r1 , s1) '(r2 , s2) => (r1 * r2 , s1 * s2)).
  -
R, S: Ring
One (ab_biprod R S) exact (ring_one , ring_one).
  -
R, S: Ring
Associative mult intros [r1 s1] [r2 s2] [r3 s3].
R, S: Ring
r1: R
s1: S
r2: R
s2: S
r3: R
s3: S
(r1, s1) * ((r2, s2) * (r3, s3)) =
(r1, s1) * (r2, s2) * (r3, s3)
    apply path_prod; cbn; apply rng_mult_assoc.
  -
R, S: Ring
LeftDistribute mult plus intros [r1 s1] [r2 s2] [r3 s3].
R, S: Ring
r1: R
s1: S
r2: R
s2: S
r3: R
s3: S
(r1, s1) * ((r2, s2) + (r3, s3)) =
(r1, s1) * (r2, s2) + (r1, s1) * (r3, s3)
    apply path_prod; cbn; apply rng_dist_l.
  -
R, S: Ring
RightDistribute mult plus intros [r1 s1] [r2 s2] [r3 s3].
R, S: Ring
r1: R
s1: S
r2: R
s2: S
r3: R
s3: S
((r1, s1) + (r2, s2)) * (r3, s3) =
(r1, s1) * (r3, s3) + (r2, s2) * (r3, s3)
    apply path_prod; cbn; apply rng_dist_r.
  -
R, S: Ring
LeftIdentity mult 1 intros [r1 s1]; apply path_prod; cbn; apply rng_mult_one_l.
  -
R, S: Ring
RightIdentity mult 1 intros [r1 s1]; apply path_prod; cbn; apply rng_mult_one_r.
Defined.

Infix "×" := ring_product : ring_scope.

Definition ring_product_fst {R S : Ring} : R × S $-> R.
R, S: Ring
R × S $-> R
Proof.
R, S: Ring
R × S $-> R
  snapply Build_RingHomomorphism.
R, S: Ring
R × S -> R
R, S: Ring
IsSemiRingPreserving ?rng_homo_map
  1: exact fst.
R, S: Ring
IsSemiRingPreserving fst
  repeat split.
Defined.

Definition ring_product_snd {R S : Ring} : R × S $-> S.
R, S: Ring
R × S $-> S
Proof.
R, S: Ring
R × S $-> S
  snapply Build_RingHomomorphism.
R, S: Ring
R × S -> S
R, S: Ring
IsSemiRingPreserving ?rng_homo_map
  1: exact snd.
R, S: Ring
IsSemiRingPreserving snd
  repeat split.
Defined.

Definition ring_product_corec (R S T : Ring)
  : (R $-> S) -> (R $-> T) -> (R $-> S × T).
R, S, T: Ring
(R $-> S) -> (R $-> T) -> R $-> S × T
Proof.
R, S, T: Ring
(R $-> S) -> (R $-> T) -> R $-> S × T
  intros f g.
R, S, T: Ring
f: R $-> S
g: R $-> T
R $-> S × T
  srapply Build_RingHomomorphism'.
R, S, T: Ring
f: R $-> S
g: R $-> T
GroupHomomorphism R (S × T)
R, S, T: Ring
f: R $-> S
g: R $-> T
IsMonoidPreserving ?map
  1: exact (ab_biprod_corec f g).
R, S, T: Ring
f: R $-> S
g: R $-> T
IsMonoidPreserving (ab_biprod_corec f g)
  repeat split.
R, S, T: Ring
f: R $-> S
g: R $-> T
IsSemiGroupPreserving (ab_biprod_corec f g)
R, S, T: Ring
f: R $-> S
g: R $-> T
IsUnitPreserving (ab_biprod_corec f g)
  1: cbn; intros x y; apply path_prod; apply rng_homo_mult.
R, S, T: Ring
f: R $-> S
g: R $-> T
IsUnitPreserving (ab_biprod_corec f g)
  cbn; apply path_prod; apply rng_homo_one.
Defined.

Definition equiv_ring_product_corec `{Funext} (R S T : Ring)
  : (R $-> S) * (R $-> T) <~> (R $-> S × T).
H: Funext
R, S, T: Ring
(R $-> S) * (R $-> T) <~> (R $-> S × T)
Proof.
H: Funext
R, S, T: Ring
(R $-> S) * (R $-> T) <~> (R $-> S × T)
  snapply equiv_adjointify.
H: Funext
R, S, T: Ring
(R $-> S) * (R $-> T) -> R $-> S × T
H: Funext
R, S, T: Ring
(R $-> S × T) -> (R $-> S) * (R $-> T)
H: Funext
R, S, T: Ring
?f o ?g == idmap
H: Funext
R, S, T: Ring
?g o ?f == idmap
  1: exact (uncurry (ring_product_corec _ _ _)).
H: Funext
R, S, T: Ring
(R $-> S × T) -> (R $-> S) * (R $-> T)
H: Funext
R, S, T: Ring
uncurry (ring_product_corec R S T) o ?g == idmap
H: Funext
R, S, T: Ring
?g o uncurry (ring_product_corec R S T) == idmap
  {
H: Funext
R, S, T: Ring
(R $-> S × T) -> (R $-> S) * (R $-> T) intros f.
H: Funext
R, S, T: Ring
f: R $-> S × T
((R $-> S) * (R $-> T))%type
    exact (ring_product_fst $o f, ring_product_snd $o f). }
H: Funext
R, S, T: Ring
uncurry (ring_product_corec R S T)
o (fun f : R $-> S × T =>
   (ring_product_fst $o f, ring_product_snd $o f)) ==
idmap
H: Funext
R, S, T: Ring
(fun f : R $-> S × T =>
 (ring_product_fst $o f, ring_product_snd $o f))
o uncurry (ring_product_corec R S T) == idmap
  {
H: Funext
R, S, T: Ring
uncurry (ring_product_corec R S T)
o (fun f : R $-> S × T =>
   (ring_product_fst $o f, ring_product_snd $o f)) ==
idmap hnf; intros f.
H: Funext
R, S, T: Ring
f: R $-> S × T
uncurry (ring_product_corec R S T)
  (ring_product_fst $o f, ring_product_snd $o f) = f
    by apply path_hom. }
H: Funext
R, S, T: Ring
(fun f : R $-> S × T =>
 (ring_product_fst $o f, ring_product_snd $o f))
o uncurry (ring_product_corec R S T) == idmap
  intros [f g].
H: Funext
R, S, T: Ring
f: R $-> S
g: R $-> T
(ring_product_fst $o
 uncurry (ring_product_corec R S T) (f, g),
ring_product_snd $o
uncurry (ring_product_corec R S T) (f, g)) = (f, g)
  apply path_prod.
H: Funext
R, S, T: Ring
f: R $-> S
g: R $-> T
fst
  (ring_product_fst $o
   uncurry (ring_product_corec R S T) (f, g),
  ring_product_snd $o
  uncurry (ring_product_corec R S T) (f, g)) =
fst (f, g)
H: Funext
R, S, T: Ring
f: R $-> S
g: R $-> T
snd
  (ring_product_fst $o
   uncurry (ring_product_corec R S T) (f, g),
  ring_product_snd $o
  uncurry (ring_product_corec R S T) (f, g)) =
snd (f, g)
  1,2: by apply path_hom.
Defined.

Instance hasbinaryproducts_ring : HasBinaryProducts Ring.
HasBinaryProducts Ring
Proof.
HasBinaryProducts Ring
  intros R S.
R, S: Ring
BinaryProduct R S
  snapply Build_BinaryProduct.
R, S: Ring
Ring
R, S: Ring
?cat_binprod' $-> R
R, S: Ring
?cat_binprod' $-> S
R, S: Ring
forall z : Ring,
(z $-> R) -> (z $-> S) -> z $-> ?cat_binprod'
R, S: Ring
forall (z : Ring) (f : z $-> R) (g : z $-> S),
?cat_pr1 $o ?cat_binprod_corec z f g $== f
R, S: Ring
forall (z : Ring) (f : z $-> R) (g : z $-> S),
?cat_pr2 $o ?cat_binprod_corec z f g $== g
R, S: Ring
forall (z : Ring) (f g : z $-> ?cat_binprod'),
?cat_pr1 $o f $== ?cat_pr1 $o g ->
?cat_pr2 $o f $== ?cat_pr2 $o g -> f $== g
  -
R, S: Ring
Ring exact (R × S).
  -
R, S: Ring
R × S $-> R exact ring_product_fst.
  -
R, S: Ring
R × S $-> S exact ring_product_snd.
  -
R, S: Ring
forall z : Ring, (z $-> R) -> (z $-> S) -> z $-> R × S exact (fun T => ring_product_corec T R S).
  -
R, S: Ring
forall (z : Ring) (f : z $-> R) (g : z $-> S),
ring_product_fst $o
(fun T : Ring => ring_product_corec T R S) z f g $== f cbn; reflexivity.
  -
R, S: Ring
forall (z : Ring) (f : z $-> R) (g : z $-> S),
ring_product_snd $o
(fun T : Ring => ring_product_corec T R S) z f g $== g cbn; reflexivity.
  -
R, S: Ring
forall (z : Ring) (f g : z $-> R × S),
ring_product_fst $o f $== ring_product_fst $o g ->
ring_product_snd $o f $== ring_product_snd $o g ->
f $== g intros T f g p q x.
R, S, T: Ring
f, g: T $-> R × S
p: ring_product_fst $o f $== ring_product_fst $o g
q: ring_product_snd $o f $== ring_product_snd $o g
x: T
f x = g x
    exact (path_prod' (p x) (q x)).
Defined.

(** ** Image ring *)

(** The image of a ring homomorphism *)
Definition rng_image {R S : Ring} (f : R $-> S) : Subring S.
R, S: Ring
f: R $-> S
Subring S
Proof.
R, S: Ring
f: R $-> S
Subring S
  snapply (Build_Subring'' (grp_image f)).
R, S: Ring
f: R $-> S
forall x y : S,
grp_image f x -> grp_image f y -> grp_image f (x * y)
R, S: Ring
f: R $-> S
grp_image f 1
  -
R, S: Ring
f: R $-> S
forall x y : S,
grp_image f x -> grp_image f y -> grp_image f (x * y) simpl.
R, S: Ring
f: R $-> S
forall x y : S,
Tr (-1) {x0 : R & f x0 = x} ->
Tr (-1) {x0 : R & f x0 = y} ->
Tr (-1) {x0 : R & f x0 = x * y}
    intros x y p q.
R, S: Ring
f: R $-> S
x, y: S
p: Tr (-1) {x0 : R & f x0 = x}
q: Tr (-1) {x : R & f x = y}
Tr (-1) {x0 : R & f x0 = x * y}
    strip_truncations; apply tr.
R, S: Ring
f: R $-> S
x, y: S
q: {x : R & f x = y}
p: {x0 : R & f x0 = x}
{x0 : R & f x0 = x * y}
    destruct p as [a p'], q as [b q'].
R, S: Ring
f: R $-> S
x, y: S
b: R
q': f b = y
a: R
p': f a = x
{x0 : R & f x0 = x * y}
    exists (a * b).
R, S: Ring
f: R $-> S
x, y: S
b: R
q': f b = y
a: R
p': f a = x
f (a * b) = x * y
    refine (rng_homo_mult _ _ _ @ _).
R, S: Ring
f: R $-> S
x, y: S
b: R
q': f b = y
a: R
p': f a = x
f a * f b = x * y
    f_ap.
  -
R, S: Ring
f: R $-> S
grp_image f 1 apply tr.
R, S: Ring
f: R $-> S
{x : R & f x = 1}
    exists 1.
R, S: Ring
f: R $-> S
f 1 = 1
    exact (rng_homo_one f).
Defined.

Lemma rng_homo_image_incl {R S} (f : RingHomomorphism R S)
  : (rng_image f : Ring) $-> S.
R, S: Ring
f: RingHomomorphism R S
(rng_image f : Ring) $-> S
Proof.
R, S: Ring
f: RingHomomorphism R S
(rng_image f : Ring) $-> S
  snapply Build_RingHomomorphism.
R, S: Ring
f: RingHomomorphism R S
rng_image f -> S
R, S: Ring
f: RingHomomorphism R S
IsSemiRingPreserving ?rng_homo_map
  1: exact pr1.
R, S: Ring
f: RingHomomorphism R S
IsSemiRingPreserving pr1
  repeat split.
Defined.

(** Image of a surjective ring homomorphism *)
Lemma rng_image_issurj {R S} (f : RingHomomorphism R S) {issurj : IsSurjection f}
  : (rng_image f : Ring) ≅ S.
R, S: Ring
f: RingHomomorphism R S
issurj: IsConnMap (Tr (-1)) f
(rng_image f : Ring) ≅ S
Proof.
R, S: Ring
f: RingHomomorphism R S
issurj: IsConnMap (Tr (-1)) f
(rng_image f : Ring) ≅ S
  snapply Build_RingIsomorphism.
R, S: Ring
f: RingHomomorphism R S
issurj: IsConnMap (Tr (-1)) f
RingHomomorphism (rng_image f) S
R, S: Ring
f: RingHomomorphism R S
issurj: IsConnMap (Tr (-1)) f
IsEquiv ?rng_iso_homo
  1: exact (rng_homo_image_incl f).
R, S: Ring
f: RingHomomorphism R S
issurj: IsConnMap (Tr (-1)) f
IsEquiv (rng_homo_image_incl f)
  exact _.
Defined. 

(** ** Opposite Ring *)

(** Given a ring [R] we can reverse the order of the multiplication to get another ring [R^op]. *)
Definition rng_op : Ring -> Ring.
Ring -> Ring
Proof.
Ring -> Ring
  (** Let's carefully pull apart the ring structure and put it back together. Unfortunately, our definition of ring has some redundant data such as multiple hset assumptions, due to the mixing of algebraic structures. This isn't a problem in practice, but it does mean using typeclass inference here will pick up the wrong instance, therefore we carefully put it back together. See test/Algebra/Rings/Ring.v for a test checking this operation is definitionally involutive. *)
  intros [R mult one
    [is_abgroup [[monoid_ishset mult_assoc] li ri] ld rd]
    mult_assoc_opp].
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
Ring
  snapply Build_Ring'.
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
AbGroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
Mult ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
One ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
IsRing ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
forall z y x : ?ring_abgroup, x * y * z = x * (y * z)
  4: split.
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
AbGroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
Mult ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
One ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
IsAbGroup ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
IsMonoid ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
LeftDistribute canonical_names.mult plus
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
RightDistribute canonical_names.mult plus
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
forall z y x : ?ring_abgroup, x * y * z = x * (y * z)
  5: split.
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
AbGroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
Mult ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
One ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
IsAbGroup ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
IsSemiGroup ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
LeftIdentity sg_op mon_unit
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
RightIdentity sg_op mon_unit
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
LeftDistribute canonical_names.mult plus
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
RightDistribute canonical_names.mult plus
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
forall z y x : ?ring_abgroup, x * y * z = x * (y * z)
  5: split.
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
AbGroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
Mult ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
One ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
IsAbGroup ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
IsHSet ?ring_abgroup
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
Associative sg_op
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
LeftIdentity sg_op mon_unit
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
RightIdentity sg_op mon_unit
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
LeftDistribute canonical_names.mult plus
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
RightDistribute canonical_names.mult plus
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
forall z y x : ?ring_abgroup, x * y * z = x * (y * z)
  -
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
AbGroup exact R.
  -
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
Mult R exact (fun x y => mult y x).
  -
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
One R exact one.
  -
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
IsAbGroup R exact is_abgroup.
  -
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
IsHSet R exact monoid_ishset.
  -
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
Associative sg_op exact mult_assoc_opp.
  -
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
LeftIdentity sg_op mon_unit exact ri.
  -
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
RightIdentity sg_op mon_unit exact li.
  -
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
LeftDistribute canonical_names.mult plus exact (fun x y z => rd y z x).
  -
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
RightDistribute canonical_names.mult plus exact (fun x y z => ld z x y).
  -
R: AbGroup
mult: Mult R
one: One R
is_abgroup: IsAbGroup R
monoid_ishset: IsHSet R
mult_assoc: Associative sg_op
li: LeftIdentity sg_op mon_unit
ri: RightIdentity sg_op mon_unit
ld: LeftDistribute canonical_names.mult plus
rd: RightDistribute canonical_names.mult plus
mult_assoc_opp: forall z y x : R,
x * y * z = x * (y * z)
forall z y x : R, x * y * z = x * (y * z) exact mult_assoc.
Defined.

(** The opposite ring is a functor. *)
Instance is0functor_rng_op : Is0Functor rng_op.
Is0Functor rng_op
Proof.
Is0Functor rng_op
  snapply Build_Is0Functor.
forall a b : Ring, (a $-> b) -> rng_op a $-> rng_op b
  intros R S f.
R, S: Ring
f: R $-> S
rng_op R $-> rng_op S
  snapply Build_RingHomomorphism'.
R, S: Ring
f: R $-> S
GroupHomomorphism (rng_op R) (rng_op S)
R, S: Ring
f: R $-> S
IsMonoidPreserving ?map
  -
R, S: Ring
f: R $-> S
GroupHomomorphism (rng_op R) (rng_op S) exact f.
  -
R, S: Ring
f: R $-> S
IsMonoidPreserving f split.
R, S: Ring
f: R $-> S
IsSemiGroupPreserving f
R, S: Ring
f: R $-> S
IsUnitPreserving f
    +
R, S: Ring
f: R $-> S
IsSemiGroupPreserving f exact (fun x y => rng_homo_mult f y x).
    +
R, S: Ring
f: R $-> S
IsUnitPreserving f exact (rng_homo_one f).
Defined.

Instance is1functor_rng_op : Is1Functor rng_op.
Is1Functor rng_op
Proof.
Is1Functor rng_op
  snapply Build_Is1Functor.
forall (a b : Ring) (f g : a $-> b),
f $== g -> fmap rng_op f $== fmap rng_op g
forall a : Ring, fmap rng_op (Id a) $== Id (rng_op a)
forall (a b c : Ring) (f : a $-> b) (g : b $-> c),
fmap rng_op (g $o f) $==
fmap rng_op g $o fmap rng_op f
  -
forall (a b : Ring) (f g : a $-> b),
f $== g -> fmap rng_op f $== fmap rng_op g intros R S f g p.
R, S: Ring
f, g: R $-> S
p: f $== g
fmap rng_op f $== fmap rng_op g
    exact p.
  -
forall a : Ring, fmap rng_op (Id a) $== Id (rng_op a) intros R; cbn; reflexivity.
  -
forall (a b c : Ring) (f : a $-> b) (g : b $-> c),
fmap rng_op (g $o f) $==
fmap rng_op g $o fmap rng_op f intros R S T f g; cbn; reflexivity.
Defined.

(** ** Powers *)

(** Powers of ring elements *)
Definition rng_power {R : Ring} (x : R) (n : nat) : R := nat_iter n (x *.) ring_one.

(** Power laws *)
Lemma rng_power_mult_law {R : Ring} (x : R) (n m : nat)
  : (rng_power x n) * (rng_power x m) = rng_power x (n + m).
R: Ring
x: R
n, m: nat
rng_power x n * rng_power x m = rng_power x (n + m)
Proof.
R: Ring
x: R
n, m: nat
rng_power x n * rng_power x m = rng_power x (n + m)
  induction n as [|n IHn].
R: Ring
x: R
m: nat
rng_power x 0 * rng_power x m = rng_power x (0 + m)
R: Ring
x: R
n, m: nat
IHn: rng_power x n * rng_power x m = rng_power x (n + m)
rng_power x n.+1 * rng_power x m =
rng_power x (n.+1 + m)
  1: apply rng_mult_one_l.
R: Ring
x: R
n, m: nat
IHn: rng_power x n * rng_power x m = rng_power x (n + m)
rng_power x n.+1 * rng_power x m =
rng_power x (n.+1 + m)
  refine ((rng_mult_assoc _ _ _)^ @ _).
R: Ring
x: R
n, m: nat
IHn: rng_power x n * rng_power x m = rng_power x (n + m)
x * (nat_iter n (mult x) ring_one * rng_power x m) =
rng_power x (n.+1 + m)
  exact (ap (x *.) IHn).
Defined.

(** ** Finite Sums *)

(** Ring multiplication distributes over finite sums on the left. *)
Definition rng_sum_dist_l {R : Ring} (n : nat) (f : forall k, (k < n)%nat -> R) (r : R)
  : r * ab_sum n f = ab_sum n (fun k Hk => r * f k Hk).
R: Ring
n: nat
f: forall k : nat, (k < n)%nat -> R
r: R
r * ab_sum n f =
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) => r * f k Hk)
Proof.
R: Ring
n: nat
f: forall k : nat, (k < n)%nat -> R
r: R
r * ab_sum n f =
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) => r * f k Hk)
  induction n as [|n IHn].
R: Ring
f: forall k : nat, (k < 0)%nat -> R
r: R
r * ab_sum 0 f =
ab_sum 0
  (fun (k : nat) (Hk : (k < 0)%nat) => r * f k Hk)
R: Ring
n: nat
f: forall k : nat, (k < n.+1)%nat -> R
r: R
IHn: forall f : forall k : nat, (k < n)%nat -> R,
r * ab_sum n f = ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => r * f k Hk)
r * ab_sum n.+1 f =
ab_sum n.+1
  (fun (k : nat) (Hk : (k < n.+1)%nat) => r * f k Hk)
  1: apply rng_mult_zero_r.
R: Ring
n: nat
f: forall k : nat, (k < n.+1)%nat -> R
r: R
IHn: forall f : forall k : nat, (k < n)%nat -> R,
r * ab_sum n f = ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => r * f k Hk)
r * ab_sum n.+1 f =
ab_sum n.+1
  (fun (k : nat) (Hk : (k < n.+1)%nat) => r * f k Hk)
  lhs napply rng_dist_l; simpl; f_ap.
Defined.

(** Ring multiplication distributes over finite sums on the right. *)
Definition rng_sum_dist_r {R : Ring} (n : nat) (f : forall k, (k < n)%nat -> R) (r : R)
  : ab_sum n f * r = ab_sum n (fun k Hk => f k Hk * r).
R: Ring
n: nat
f: forall k : nat, (k < n)%nat -> R
r: R
ab_sum n f * r =
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) => f k Hk * r)
Proof.
R: Ring
n: nat
f: forall k : nat, (k < n)%nat -> R
r: R
ab_sum n f * r =
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) => f k Hk * r)
  induction n as [|n IHn].
R: Ring
f: forall k : nat, (k < 0)%nat -> R
r: R
ab_sum 0 f * r =
ab_sum 0
  (fun (k : nat) (Hk : (k < 0)%nat) => f k Hk * r)
R: Ring
n: nat
f: forall k : nat, (k < n.+1)%nat -> R
r: R
IHn: forall f : forall k : nat, (k < n)%nat -> R,
ab_sum n f * r = ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f k Hk * r)
ab_sum n.+1 f * r =
ab_sum n.+1
  (fun (k : nat) (Hk : (k < n.+1)%nat) => f k Hk * r)
  1: apply rng_mult_zero_l.
R: Ring
n: nat
f: forall k : nat, (k < n.+1)%nat -> R
r: R
IHn: forall f : forall k : nat, (k < n)%nat -> R,
ab_sum n f * r = ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => f k Hk * r)
ab_sum n.+1 f * r =
ab_sum n.+1
  (fun (k : nat) (Hk : (k < n.+1)%nat) => f k Hk * r)
  lhs napply rng_dist_r; simpl; f_ap.
Defined.

(** ** Invertible elements *)

(** An element [x] of a ring [R] is left invertible if there exists an element [y] such that [y * x = 1]. *)
Class IsLeftInvertible (R : Ring) (x : R) := {
  left_inverse_elem : R;
  left_inverse_eq : left_inverse_elem * x = 1;
}.

Arguments left_inverse_elem {R} x {_}.
Arguments left_inverse_eq {R} x {_}.

Definition issig_IsLeftInvertible {R : Ring} (x : R)
  : _ <~> IsLeftInvertible R x
  := ltac:(issig).

(** An element [x] of a ring [R] is right invertible if there exists an element [y] such that [x * y = 1]. We state this as a left invertible element of the opposite ring. *)
Class IsRightInvertible (R : Ring) (x : R)
  := isleftinvertible_rng_op :: IsLeftInvertible (rng_op R) x.

Definition right_inverse_elem {R} x `{!IsRightInvertible R x} : R
  := left_inverse_elem (R:=rng_op R) x.

Definition right_inverse_eq {R} x `{!IsRightInvertible R x}
  : x * right_inverse_elem x = 1
  := left_inverse_eq (R:=rng_op R) x.

(** An element [x] of a ring [R] is invertible if it is both left and right invertible. *)
Class IsInvertible (R : Ring) (x : R) := Build_IsInvertible' {
  isleftinvertible_isinvertible :: IsLeftInvertible R x;
  isrightinvertible_isinvertible :: IsRightInvertible R x;
}.

(** We can show an element is invertible by providing an inverse element which is a left and right inverse simultaneously. We will later show that the two inverses of an invertible element must be equal anyway. *)
Definition Build_IsInvertible {R : Ring} (x : R)
  (inv : R) (inv_l : inv * x = 1) (inv_r : x * inv = 1)
  : IsInvertible R x.
R: Ring
x, inv: R
inv_l: inv * x = 1
inv_r: x * inv = 1
IsInvertible R x
Proof.
R: Ring
x, inv: R
inv_l: inv * x = 1
inv_r: x * inv = 1
IsInvertible R x
  split.
R: Ring
x, inv: R
inv_l: inv * x = 1
inv_r: x * inv = 1
IsLeftInvertible R x
R: Ring
x, inv: R
inv_l: inv * x = 1
inv_r: x * inv = 1
IsRightInvertible R x
  -
R: Ring
x, inv: R
inv_l: inv * x = 1
inv_r: x * inv = 1
IsLeftInvertible R x by exists inv.
  -
R: Ring
x, inv: R
inv_l: inv * x = 1
inv_r: x * inv = 1
IsRightInvertible R x unfold IsRightInvertible.
R: Ring
x, inv: R
inv_l: inv * x = 1
inv_r: x * inv = 1
IsLeftInvertible (rng_op R) x
    by exists (inv : rng_op R).
Defined.

(** The invertible elements in [R] and [rng_op R] agree, by swapping the proofs of left and right invertibility. *)
Definition isinvertible_rng_op (R : Ring) (x : R) `{!IsInvertible R x}
  : IsInvertible (rng_op R) x.
R: Ring
x: R
IsInvertible0: IsInvertible R x
IsInvertible (rng_op R) x
Proof.
R: Ring
x: R
IsInvertible0: IsInvertible R x
IsInvertible (rng_op R) x
  split.
R: Ring
x: R
IsInvertible0: IsInvertible R x
IsLeftInvertible (rng_op R) x
R: Ring
x: R
IsInvertible0: IsInvertible R x
IsRightInvertible (rng_op R) x
  -
R: Ring
x: R
IsInvertible0: IsInvertible R x
IsLeftInvertible (rng_op R) x exact (isrightinvertible_isinvertible).
  -
R: Ring
x: R
IsInvertible0: IsInvertible R x
IsRightInvertible (rng_op R) x exact (isleftinvertible_isinvertible).
Defined.

(** *** Uniqueness of inverses *)

(** This general lemma will be used for uniqueness results. *)
Definition path_left_right_inverse {R : Ring} (x x' x'' : R)
  (p : x' * x = 1) (q : x * x'' = 1)
  : x' = x''.
R: Ring
x, x', x'': R
p: x' * x = 1
q: x * x'' = 1
x' = x''
Proof.
R: Ring
x, x', x'': R
p: x' * x = 1
q: x * x'' = 1
x' = x''
  rhs_V napply rng_mult_one_l.
R: Ring
x, x', x'': R
p: x' * x = 1
q: x * x'' = 1
x' = 1 * x''
  rewrite <- p.
R: Ring
x, x', x'': R
p: x' * x = 1
q: x * x'' = 1
x' = x' * x * x'' 
  rewrite <- simple_associativity.
R: Ring
x, x', x'': R
p: x' * x = 1
q: x * x'' = 1
x' = x' * (x * x'')
  rewrite q.
R: Ring
x, x', x'': R
p: x' * x = 1
q: x * x'' = 1
x' = x' * 1
  symmetry.
R: Ring
x, x', x'': R
p: x' * x = 1
q: x * x'' = 1
x' * 1 = x'
  apply rng_mult_one_r.
Defined.

(** The left and right inverse of an invertible element are necessarily equal. *)
Definition path_left_inverse_elem_right_inverse_elem
  {R : Ring} x `{!IsInvertible R x}
  : left_inverse_elem x = right_inverse_elem x.
R: Ring
x: R
IsInvertible0: IsInvertible R x
left_inverse_elem x = right_inverse_elem x
Proof.
R: Ring
x: R
IsInvertible0: IsInvertible R x
left_inverse_elem x = right_inverse_elem x
  napply (path_left_right_inverse x).
R: Ring
x: R
IsInvertible0: IsInvertible R x
left_inverse_elem x * x = 1
R: Ring
x: R
IsInvertible0: IsInvertible R x
x * right_inverse_elem x = 1
  -
R: Ring
x: R
IsInvertible0: IsInvertible R x
left_inverse_elem x * x = 1 apply left_inverse_eq.
  -
R: Ring
x: R
IsInvertible0: IsInvertible R x
x * right_inverse_elem x = 1 apply right_inverse_eq.
Defined.

(** It is therefore well-defined to talk about the inverse of an invertible element. *)
Definition inverse_elem {R : Ring} (x : R) `{IsInvertible R x} : R
  := left_inverse_elem x.

(** Left cancellation for an invertible element. *)
Definition rng_inv_l {R : Ring} (x : R) `{IsInvertible R x}
  : inverse_elem x * x = 1.
R: Ring
x: R
H: IsInvertible R x
inverse_elem x * x = 1
Proof.
R: Ring
x: R
H: IsInvertible R x
inverse_elem x * x = 1
  apply left_inverse_eq.
Defined.

(** Right cancellation for an invertible element. *)
Definition rng_inv_r {R : Ring} (x : R) `{IsInvertible R x}
  : x * inverse_elem x = 1.
R: Ring
x: R
H: IsInvertible R x
x * inverse_elem x = 1
Proof.
R: Ring
x: R
H: IsInvertible R x
x * inverse_elem x = 1
  rhs_V exact (right_inverse_eq x).
R: Ring
x: R
H: IsInvertible R x
x * inverse_elem x = x * right_inverse_elem x
  f_ap.
R: Ring
x: R
H: IsInvertible R x
inverse_elem x = right_inverse_elem x
  apply path_left_inverse_elem_right_inverse_elem.
Defined.

(** Equal elements have equal inverses.  Note that we don't require that the proofs of invertibility are equal (over [p]).  It follows that the inverse of an invertible element [x] depends only on [x]. *)
Definition isinvertible_unique {R : Ring} (x y : R) `{IsInvertible R x} `{IsInvertible R y} (p : x = y)
  : inverse_elem x = inverse_elem y.
R: Ring
x, y: R
H: IsInvertible R x
H0: IsInvertible R y
p: x = y
inverse_elem x = inverse_elem y
Proof.
R: Ring
x, y: R
H: IsInvertible R x
H0: IsInvertible R y
p: x = y
inverse_elem x = inverse_elem y
  destruct p.
R: Ring
x: R
H, H0: IsInvertible R x
inverse_elem x = inverse_elem x
  snapply (path_left_right_inverse x).
R: Ring
x: R
H, H0: IsInvertible R x
inverse_elem x * x = 1
R: Ring
x: R
H, H0: IsInvertible R x
x * inverse_elem x = 1
  -
R: Ring
x: R
H, H0: IsInvertible R x
inverse_elem x * x = 1 apply rng_inv_l.
  -
R: Ring
x: R
H, H0: IsInvertible R x
x * inverse_elem x = 1 apply rng_inv_r.
Defined.

(** We can show that being invertible is equivalent to having an inverse element that is simultaneously a left and right inverse. *)
Definition equiv_isinvertible_left_right_inverse {R : Ring} (x : R)
  : {inv : R & prod (inv * x = 1) (x * inv = 1)} <~> IsInvertible R x.
R: Ring
x: R
{inv : R & ((mult inv x = 1) * (mult x inv = 1))%type} <~>
IsInvertible R x
Proof.
R: Ring
x: R
{inv : R & ((mult inv x = 1) * (mult x inv = 1))%type} <~>
IsInvertible R x
  equiv_via { i : IsInvertible R x & right_inverse_elem x = left_inverse_elem x }.
R: Ring
x: R
{inv : R & ((mult inv x = 1) * (mult x inv = 1))%type} <~>
{i : IsInvertible R x &
right_inverse_elem x = left_inverse_elem x}
R: Ring
x: R
{i : IsInvertible R x &
right_inverse_elem x = left_inverse_elem x} <~>
IsInvertible R x
  1: make_equiv_contr_basedpaths.
R: Ring
x: R
{i : IsInvertible R x &
right_inverse_elem x = left_inverse_elem x} <~>
IsInvertible R x
  apply equiv_sigma_contr; intro i.
R: Ring
x: R
i: IsInvertible R x
Contr (right_inverse_elem x = left_inverse_elem x)
  rapply contr_inhabited_hprop.
R: Ring
x: R
i: IsInvertible R x
right_inverse_elem x = left_inverse_elem x
  symmetry; apply path_left_inverse_elem_right_inverse_elem.
Defined.

(** Being invertible is a proposition. *)
Instance ishprop_isinvertible {R x} : IsHProp (IsInvertible R x).
R: Ring
x: R
IsHProp (IsInvertible R x)
Proof.
R: Ring
x: R
IsHProp (IsInvertible R x)
  napply (istrunc_equiv_istrunc _ (equiv_isinvertible_left_right_inverse x)).
R: Ring
x: R
IsHProp
  {inv : R &
  ((mult inv x = 1) * (mult x inv = 1))%type}
  snapply hprop_allpath; intros [y [p1 p2]] [z [q1 q2]].
R: Ring
x, y: R
p1: y * x = 1
p2: x * y = 1
z: R
q1: z * x = 1
q2: x * z = 1
(y; (p1, p2)) = (z; (q1, q2))
  rapply path_sigma_hprop; cbn.
R: Ring
x, y: R
p1: y * x = 1
p2: x * y = 1
z: R
q1: z * x = 1
q2: x * z = 1
y = z
  exact (path_left_right_inverse x y z p1 q2).
Defined.

(** *** Closure of invertible elements under multiplication *)

(** Left invertible elements are closed under multiplication. *)
Instance isleftinvertible_mult {R : Ring} (x y : R)
  : IsLeftInvertible R x -> IsLeftInvertible R y -> IsLeftInvertible R (x * y).
R: Ring
x, y: R
IsLeftInvertible R x ->
IsLeftInvertible R y -> IsLeftInvertible R (x * y)
Proof.
R: Ring
x, y: R
IsLeftInvertible R x ->
IsLeftInvertible R y -> IsLeftInvertible R (x * y)
  intros [x' p] [y' q].
R: Ring
x, y, x': R
p: x' * x = 1
y': R
q: y' * y = 1
IsLeftInvertible R (x * y)
  exists (y' * x').
R: Ring
x, y, x': R
p: x' * x = 1
y': R
q: y' * y = 1
y' * x' * (x * y) = 1
  rhs_V exact q.
R: Ring
x, y, x': R
p: x' * x = 1
y': R
q: y' * y = 1
y' * x' * (x * y) = y' * y
  lhs napply rng_mult_assoc.
R: Ring
x, y, x': R
p: x' * x = 1
y': R
q: y' * y = 1
y' * x' * x * y = y' * y
  f_ap.
R: Ring
x, y, x': R
p: x' * x = 1
y': R
q: y' * y = 1
y' * x' * x = y'
  rhs_V napply rng_mult_one_r.
R: Ring
x, y, x': R
p: x' * x = 1
y': R
q: y' * y = 1
y' * x' * x = y' * 1
  lhs_V napply rng_mult_assoc.
R: Ring
x, y, x': R
p: x' * x = 1
y': R
q: y' * y = 1
y' * (x' * x) = y' * 1
  f_ap.
Defined.

(** Right invertible elements are closed under multiplication. *)
Instance isrightinvertible_mult {R : Ring} (x y : R)
  : IsRightInvertible R x -> IsRightInvertible R y -> IsRightInvertible R (x * y).
R: Ring
x, y: R
IsRightInvertible R x ->
IsRightInvertible R y -> IsRightInvertible R (x * y)
Proof.
R: Ring
x, y: R
IsRightInvertible R x ->
IsRightInvertible R y -> IsRightInvertible R (x * y)
  change (x * y) with (ring_mult (R:=rng_op R) y x).
R: Ring
x, y: R
IsRightInvertible R x ->
IsRightInvertible R y ->
IsRightInvertible R (ring_mult y x)
  unfold IsRightInvertible.
R: Ring
x, y: R
IsLeftInvertible (rng_op R) x ->
IsLeftInvertible (rng_op R) y ->
IsLeftInvertible (rng_op R) (ring_mult y x)
  exact _.
Defined.

(** Invertible elements are closed under multiplication. *)
Instance isinvertible_mult {R : Ring} (x y : R)
  : IsInvertible R x -> IsInvertible R y -> IsInvertible R (x * y)
  := {}.

(** Left invertible elements are closed under negation. *)
Instance isleftinvertible_neg {R : Ring} (x : R)
  : IsLeftInvertible R x -> IsLeftInvertible R (-x).
R: Ring
x: R
IsLeftInvertible R x -> IsLeftInvertible R (- x)
Proof.
R: Ring
x: R
IsLeftInvertible R x -> IsLeftInvertible R (- x)
  intros H.
R: Ring
x: R
H: IsLeftInvertible R x
IsLeftInvertible R (- x)
  exists (- left_inverse_elem x).
R: Ring
x: R
H: IsLeftInvertible R x
- left_inverse_elem x * - x = 1
  lhs napply rng_mult_negate_negate.
R: Ring
x: R
H: IsLeftInvertible R x
left_inverse_elem x * x = 1
  apply left_inverse_eq.
Defined.

(** Right invertible elements are closed under negation. *)
Instance isrightinvertible_neg {R : Ring} (x : R)
  : IsRightInvertible R x -> IsRightInvertible R (-x).
R: Ring
x: R
IsRightInvertible R x -> IsRightInvertible R (- x)
Proof.
R: Ring
x: R
IsRightInvertible R x -> IsRightInvertible R (- x)
  intros H.
R: Ring
x: R
H: IsRightInvertible R x
IsRightInvertible R (- x)
  rapply isleftinvertible_neg.
Defined.

(** Invertible elements are closed under negation. *)
Instance isinvertible_neg {R : Ring} (x : R)
  : IsInvertible R x -> IsInvertible R (-x)
  := {}.

(** Inverses of left invertible elements are themselves right invertible. *)
Instance isrightinvertible_left_inverse_elem {R : Ring} (x : R)
  `{IsLeftInvertible R x}
  : IsRightInvertible R (left_inverse_elem x).
R: Ring
x: R
H: IsLeftInvertible R x
IsRightInvertible R (left_inverse_elem x)
Proof.
R: Ring
x: R
H: IsLeftInvertible R x
IsRightInvertible R (left_inverse_elem x)
  exists (x : rng_op R).
R: Ring
x: R
H: IsLeftInvertible R x
x * left_inverse_elem x = 1
  exact (left_inverse_eq x).
Defined.

(** Inverses of right invertible elements are themselves left invertible. *)
Instance isleftinvertible_right_inverse_elem {R : Ring} (x : R)
  `{IsRightInvertible R x}
  : IsLeftInvertible R (right_inverse_elem x).
R: Ring
x: R
H: IsRightInvertible R x
IsLeftInvertible R (right_inverse_elem x)
Proof.
R: Ring
x: R
H: IsRightInvertible R x
IsLeftInvertible R (right_inverse_elem x)
  exists x.
R: Ring
x: R
H: IsRightInvertible R x
x * right_inverse_elem x = 1
  exact (right_inverse_eq x).
Defined.

(** Inverses of invertible elements are themselves invertible.  We take both inverses of [inverse_elem x] to be [x]. *)
Instance isinvertible_inverse_elem {R : Ring} (x : R)
  `{IsInvertible R x}
  : IsInvertible R (inverse_elem x).
R: Ring
x: R
H: IsInvertible R x
IsInvertible R (inverse_elem x)
Proof.
R: Ring
x: R
H: IsInvertible R x
IsInvertible R (inverse_elem x)
  split.
R: Ring
x: R
H: IsInvertible R x
IsLeftInvertible R (inverse_elem x)
R: Ring
x: R
H: IsInvertible R x
IsRightInvertible R (inverse_elem x)
  -
R: Ring
x: R
H: IsInvertible R x
IsLeftInvertible R (inverse_elem x) exists x; apply rng_inv_r.
  -
R: Ring
x: R
H: IsInvertible R x
IsRightInvertible R (inverse_elem x) apply isrightinvertible_left_inverse_elem.
Defined.

(** Since [inverse_elem (inverse_elem x) = x], we get the following equivalence. *)
Definition equiv_path_inverse_elem {R : Ring} {x y : R}
  `{IsInvertible R x, IsInvertible R y}
  : x = y <~> inverse_elem x = inverse_elem y.
R: Ring
x, y: R
H: IsInvertible R x
H0: IsInvertible R y
x = y <~> inverse_elem x = inverse_elem y
Proof.
R: Ring
x, y: R
H: IsInvertible R x
H0: IsInvertible R y
x = y <~> inverse_elem x = inverse_elem y
  srapply equiv_iff_hprop.
R: Ring
x, y: R
H: IsInvertible R x
H0: IsInvertible R y
x = y -> inverse_elem x = inverse_elem y
R: Ring
x, y: R
H: IsInvertible R x
H0: IsInvertible R y
inverse_elem x = inverse_elem y -> x = y
  -
R: Ring
x, y: R
H: IsInvertible R x
H0: IsInvertible R y
x = y -> inverse_elem x = inverse_elem y exact (isinvertible_unique x y).
  -
R: Ring
x, y: R
H: IsInvertible R x
H0: IsInvertible R y
inverse_elem x = inverse_elem y -> x = y exact (isinvertible_unique (inverse_elem x) (inverse_elem y)).
Defined.

(** [1] is always invertible, and by the above [-1]. *)
Instance isinvertible_one {R} : IsInvertible R 1.
R: Ring
IsInvertible R 1
Proof.
R: Ring
IsInvertible R 1
  snapply Build_IsInvertible.
R: Ring
R
R: Ring
?inv * 1 = 1
R: Ring
1 * ?inv = 1
  -
R: Ring
R exact one.
  -
R: Ring
1 * 1 = 1 apply rng_mult_one_l.
  -
R: Ring
1 * 1 = 1 apply rng_mult_one_l.
Defined.

(** Ring homomorphisms preserve invertible elements. *)
Instance isinvertible_rng_homo {R S} (f : R $-> S)
  : forall x, IsInvertible R x -> IsInvertible S (f x).
R, S: Ring
f: R $-> S
forall x : R, IsInvertible R x -> IsInvertible S (f x)
Proof.
R, S: Ring
f: R $-> S
forall x : R, IsInvertible R x -> IsInvertible S (f x)
  intros x H.
R, S: Ring
f: R $-> S
x: R
H: IsInvertible R x
IsInvertible S (f x)
  snapply Build_IsInvertible.
R, S: Ring
f: R $-> S
x: R
H: IsInvertible R x
S
R, S: Ring
f: R $-> S
x: R
H: IsInvertible R x
?inv * f x = 1
R, S: Ring
f: R $-> S
x: R
H: IsInvertible R x
f x * ?inv = 1
  1: exact (f (inverse_elem x)).
R, S: Ring
f: R $-> S
x: R
H: IsInvertible R x
f (inverse_elem x) * f x = 1
R, S: Ring
f: R $-> S
x: R
H: IsInvertible R x
f x * f (inverse_elem x) = 1
  1,2: lhs_V napply rng_homo_mult.
R, S: Ring
f: R $-> S
x: R
H: IsInvertible R x
f (inverse_elem x * x) = 1
R, S: Ring
f: R $-> S
x: R
H: IsInvertible R x
f (x * inverse_elem x) = 1
  1,2: rhs_V napply (rng_homo_one f).
R, S: Ring
f: R $-> S
x: R
H: IsInvertible R x
f (inverse_elem x * x) = f 1
R, S: Ring
f: R $-> S
x: R
H: IsInvertible R x
f (x * inverse_elem x) = f 1
  1,2: napply (ap f).
R, S: Ring
f: R $-> S
x: R
H: IsInvertible R x
inverse_elem x * x = 1
R, S: Ring
f: R $-> S
x: R
H: IsInvertible R x
x * inverse_elem x = 1
  -
R, S: Ring
f: R $-> S
x: R
H: IsInvertible R x
inverse_elem x * x = 1 exact (rng_inv_l x).
  -
R, S: Ring
f: R $-> S
x: R
H: IsInvertible R x
x * inverse_elem x = 1 exact (rng_inv_r x).
Defined.

(** *** Group of units *)

(** Invertible elements are typically called "units" in ring theory and the collection of units forms a group under the ring multiplication. *)
Definition rng_unit_group (R : Ring) : Group.
R: Ring
Group
Proof.
R: Ring
Group
  (** TODO: Use a generalised version of [Build_Subgroup] that works for subgroups of monoids. *)
  snapply Build_Group.
R: Ring
Type
R: Ring
SgOp ?G
R: Ring
MonUnit ?G
R: Ring
Inverse ?G
R: Ring
IsGroup ?G
  -
R: Ring
Type exact {x : R & IsInvertible R x}.
  -
R: Ring
SgOp {x : R & IsInvertible R x} intros [x p] [y q].
R: Ring
x: R
p: IsInvertible R x
y: R
q: IsInvertible R y
{x : R & IsInvertible R x}
    exists (x * y).
R: Ring
x: R
p: IsInvertible R x
y: R
q: IsInvertible R y
IsInvertible R (x * y)
    exact _.
  -
R: Ring
MonUnit {x : R & IsInvertible R x} exists 1.
R: Ring
IsInvertible R 1
    exact _.
  -
R: Ring
Inverse {x : R & IsInvertible R x} intros [x p].
R: Ring
x: R
p: IsInvertible R x
{x : R & IsInvertible R x}
    exists (inverse_elem x).
R: Ring
x: R
p: IsInvertible R x
IsInvertible R (inverse_elem x)
    exact _.
  -
R: Ring
IsGroup {x : R & IsInvertible R x} repeat split.
R: Ring
IsHSet {x : R & IsInvertible R x}
R: Ring
Associative sg_op
R: Ring
LeftIdentity sg_op mon_unit
R: Ring
RightIdentity sg_op mon_unit
R: Ring
LeftInverse sg_op inv mon_unit
R: Ring
RightInverse sg_op inv mon_unit
    1: exact _.
R: Ring
Associative sg_op
R: Ring
LeftIdentity sg_op mon_unit
R: Ring
RightIdentity sg_op mon_unit
R: Ring
LeftInverse sg_op inv mon_unit
R: Ring
RightInverse sg_op inv mon_unit
    1-5: hnf; intros; apply path_sigma_hprop.
R: Ring
x, y, z: {x : R & IsInvertible R x}
(sg_op x (sg_op y z)).1 = (sg_op (sg_op x y) z).1
R: Ring
y: {x : R & IsInvertible R x}
(sg_op mon_unit y).1 = y.1
R: Ring
x: {x : R & IsInvertible R x}
(sg_op x mon_unit).1 = x.1
R: Ring
x: {x : R & IsInvertible R x}
(sg_op (inv x) x).1 = mon_unit.1
R: Ring
x: {x : R & IsInvertible R x}
(sg_op x (inv x)).1 = mon_unit.1
    +
R: Ring
x, y, z: {x : R & IsInvertible R x}
(sg_op x (sg_op y z)).1 = (sg_op (sg_op x y) z).1 rapply simple_associativity.
    +
R: Ring
y: {x : R & IsInvertible R x}
(sg_op mon_unit y).1 = y.1 rapply left_identity.
    +
R: Ring
x: {x : R & IsInvertible R x}
(sg_op x mon_unit).1 = x.1 rapply right_identity.
    +
R: Ring
x: {x : R & IsInvertible R x}
(sg_op (inv x) x).1 = mon_unit.1 apply rng_inv_l.
    +
R: Ring
x: {x : R & IsInvertible R x}
(sg_op x (inv x)).1 = mon_unit.1 apply rng_inv_r.
Defined.

(** *** Multiplication by an invertible element is an equivalence *)

Instance isequiv_rng_inv_mult_l {R : Ring} {x : R}
  `{IsInvertible R x}
  : IsEquiv (x *.).
R: Ring
x: R
H: IsInvertible R x
IsEquiv (mult x)
Proof.
R: Ring
x: R
H: IsInvertible R x
IsEquiv (mult x)
  snapply isequiv_adjointify.
R: Ring
x: R
H: IsInvertible R x
R -> R
R: Ring
x: R
H: IsInvertible R x
mult x o ?g == idmap
R: Ring
x: R
H: IsInvertible R x
?g o mult x == idmap
  1: exact (inverse_elem x *.).
R: Ring
x: R
H: IsInvertible R x
mult x o mult (inverse_elem x) == idmap
R: Ring
x: R
H: IsInvertible R x
mult (inverse_elem x) o mult x == idmap
  1,2: intros y.
R: Ring
x: R
H: IsInvertible R x
y: R
x * (inverse_elem x * y) = y
R: Ring
x: R
H: IsInvertible R x
y: R
inverse_elem x * (x * y) = y
  1,2: lhs napply rng_mult_assoc.
R: Ring
x: R
H: IsInvertible R x
y: R
x * inverse_elem x * y = y
R: Ring
x: R
H: IsInvertible R x
y: R
inverse_elem x * x * y = y
  1,2: rhs_V napply rng_mult_one_l.
R: Ring
x: R
H: IsInvertible R x
y: R
x * inverse_elem x * y = 1 * y
R: Ring
x: R
H: IsInvertible R x
y: R
inverse_elem x * x * y = 1 * y
  1,2: snapply (ap (.* y)).
R: Ring
x: R
H: IsInvertible R x
y: R
x * inverse_elem x = 1
R: Ring
x: R
H: IsInvertible R x
y: R
inverse_elem x * x = 1
  -
R: Ring
x: R
H: IsInvertible R x
y: R
x * inverse_elem x = 1 napply rng_inv_r.
  -
R: Ring
x: R
H: IsInvertible R x
y: R
inverse_elem x * x = 1 napply rng_inv_l.
Defined.

(** This can be proved by combining [isequiv_rng_inv_mult_l (R:=rng_op R)] with [isinvertible_rng_op], but then the inverse map is given by multiplying by [right_inverse_elem x] not [inverse_elem x], which complicates calculations. *)
Instance isequiv_rng_inv_mult_r {R : Ring} {x : R}
  `{IsInvertible R x}
  : IsEquiv (.* x).
R: Ring
x: R
H: IsInvertible R x
IsEquiv (fun y : R => y * x)
Proof.
R: Ring
x: R
H: IsInvertible R x
IsEquiv (fun y : R => y * x)
  snapply isequiv_adjointify.
R: Ring
x: R
H: IsInvertible R x
R -> R
R: Ring
x: R
H: IsInvertible R x
(fun y : R => y * x) o ?g == idmap
R: Ring
x: R
H: IsInvertible R x
?g o (fun y : R => y * x) == idmap
  1: exact (.* inverse_elem x).
R: Ring
x: R
H: IsInvertible R x
(fun y : R => y * x)
o (fun y : R => y * inverse_elem x) == idmap
R: Ring
x: R
H: IsInvertible R x
(fun y : R => y * inverse_elem x)
o (fun y : R => y * x) == idmap
  1,2: intros y.
R: Ring
x: R
H: IsInvertible R x
y: R
y * inverse_elem x * x = y
R: Ring
x: R
H: IsInvertible R x
y: R
y * x * inverse_elem x = y
  1,2: lhs_V napply rng_mult_assoc.
R: Ring
x: R
H: IsInvertible R x
y: R
y * (inverse_elem x * x) = y
R: Ring
x: R
H: IsInvertible R x
y: R
y * (x * inverse_elem x) = y
  1,2: rhs_V napply rng_mult_one_r.
R: Ring
x: R
H: IsInvertible R x
y: R
y * (inverse_elem x * x) = y * 1
R: Ring
x: R
H: IsInvertible R x
y: R
y * (x * inverse_elem x) = y * 1
  1,2: snapply (ap (y *.)).
R: Ring
x: R
H: IsInvertible R x
y: R
inverse_elem x * x = 1
R: Ring
x: R
H: IsInvertible R x
y: R
x * inverse_elem x = 1
  -
R: Ring
x: R
H: IsInvertible R x
y: R
inverse_elem x * x = 1 napply rng_inv_l.
  -
R: Ring
x: R
H: IsInvertible R x
y: R
x * inverse_elem x = 1 napply rng_inv_r.
Defined.

(** *** Invertible element movement lemmas *)

(** These cannot be proven using the corresponding group laws in the group of units since not all elements involved are invertible. *)

Definition rng_inv_moveL_Vr {R : Ring} {x y z : R} `{IsInvertible R y}
  : y * x = z <~> x = inverse_elem y * z
  := equiv_moveL_equiv_V (f := (y *.)) z x.

Definition rng_inv_moveL_rV {R : Ring} {x y z : R} `{IsInvertible R y}
  : x * y = z <~> x = z * inverse_elem y
  := equiv_moveL_equiv_V (f := (.* y)) z x.

Definition rng_inv_moveR_Vr {R : Ring} {x y z : R} `{IsInvertible R y}
  : x = y * z <~> inverse_elem y * x = z
  := equiv_moveR_equiv_V (f := (y *.)) x z.

Definition rng_inv_moveR_rV {R : Ring} {x y z : R} `{IsInvertible R y}
  : x = z * y <~> x * inverse_elem y = z
  := equiv_moveR_equiv_V (f := (.* y)) x z.

(** TODO: The group of units construction is a functor from [Ring -> Group] and is right adjoint to the group ring construction. *)