Require Import WildCat.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Spaces.Nat.Core.
(* 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.AbGroups.
Require Export Classes.theory.rings.
Require Import Modalities.ReflectiveSubuniverse.

(** * 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 {_}.
Arguments ring_one {_}.
Arguments ring_isring {_}.

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

Global Instance ring_plus {R : Ring} : Plus R := plus_abgroup (ring_abgroup R).
Global Instance ring_zero {R : Ring} : Zero R := zero_abgroup (ring_abgroup R).
Global 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
  snrapply 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 B : Ring} (f : RingHomomorphism A B) (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.negate_involutive _.

  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 _ _).

  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 1%mc @ ap negate preserves_1.

End RingLaws.

(** 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.
Global Existing Instance isequiv_rng_iso_homo.

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
  snrapply 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 snrapply 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 *)
Global Instance reflexive_ringisomorphism : Reflexive RingIsomorphism
  := fun x => Build_RingIsomorphism _ _ (rng_homo_id x) _.

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

(** Ring isomorphisms are a transitive relation *)
Global 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 _ (grp_homo_ishomo _ _ 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 commutative ring using the underlying abelian group. *)
Definition Build_Ring (R : AbGroup)
  `(Mult R, One R, LeftDistribute R mult (@group_sgop R), RightDistribute R mult (@group_sgop R))
  (iscomm : @IsMonoid R mult one)
  : Ring
  := Build_Ring' R _ _ (Build_IsRing _ _ _  _ _) (fun z y x => (associativity x y z)^).

(** 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 *)

Global Instance isgraph_ring : IsGraph Ring
  := Build_IsGraph _ RingHomomorphism.

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

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

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

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

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

Global 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. *)
Global Instance is1cat_ring : Is1Cat Ring.
Is1Cat Ring
Proof.
Is1Cat Ring
  by rapply Build_Is1Cat.
Defined.

Global Instance hasmorext_ring `{Funext} : HasMorExt Ring.
H: Funext
HasMorExt Ring
Proof.
H: Funext
HasMorExt Ring
  srapply Build_HasMorExt.
H: Funext
forall (a b : Ring) (f g : a $-> b),
IsEquiv GpdHom_path
  intros A B f g; cbn in *.
H: Funext
A, B: Ring
f, g: RingHomomorphism A B
IsEquiv GpdHom_path
  snrapply @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.

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

(** ** Product ring *)

Definition ring_product : Ring -> Ring -> Ring.
Ring -> Ring -> Ring
Proof.
Ring -> Ring -> Ring
  intros R S.
R, S: Ring
Ring
  snrapply Build_Ring.
R, S: Ring
AbGroup
R, S: Ring
Mult ?R
R, S: Ring
One ?R
R, S: Ring
LeftDistribute mult group_sgop
R, S: Ring
RightDistribute mult group_sgop
R, S: Ring
IsMonoid ?R
  1: exact (ab_biprod R S).
R, S: Ring
Mult (ab_biprod R S)
R, S: Ring
One (ab_biprod R S)
R, S: Ring
LeftDistribute mult group_sgop
R, S: Ring
RightDistribute mult group_sgop
R, S: Ring
IsMonoid (ab_biprod R S)
  1: exact (fun '(r1 , s1) '(r2 , s2) => (r1 * r2 , s1 * s2)).
R, S: Ring
One (ab_biprod R S)
R, S: Ring
LeftDistribute mult group_sgop
R, S: Ring
RightDistribute mult group_sgop
R, S: Ring
IsMonoid (ab_biprod R S)
  1: exact (ring_one , ring_one).
R, S: Ring
LeftDistribute mult group_sgop
R, S: Ring
RightDistribute mult group_sgop
R, S: Ring
IsMonoid (ab_biprod R S)
  {
R, S: Ring
LeftDistribute mult group_sgop intros [r1 s1] [r2 s2] [r3 s3].
R, S: Ring
r1: R
s1: S
r2: R
s2: S
r3: R
s3: S
(r1, s1) * group_sgop (r2, s2) (r3, s3) =
group_sgop ((r1, s1) * (r2, s2)) ((r1, s1) * (r3, s3))
    apply path_prod; cbn; apply rng_dist_l. }
R, S: Ring
RightDistribute mult group_sgop
R, S: Ring
IsMonoid (ab_biprod R S)
  {
R, S: Ring
RightDistribute mult group_sgop intros [r1 s1] [r2 s2] [r3 s3].
R, S: Ring
r1: R
s1: S
r2: R
s2: S
r3: R
s3: S
group_sgop (r1, s1) (r2, s2) * (r3, s3) =
group_sgop ((r1, s1) * (r3, s3)) ((r2, s2) * (r3, s3))
    apply path_prod; cbn; apply rng_dist_r. }
R, S: Ring
IsMonoid (ab_biprod R S)
  repeat split.
R, S: Ring
IsHSet (ab_biprod R S)
R, S: Ring
Associative sg_op
R, S: Ring
LeftIdentity sg_op mon_unit
R, S: Ring
RightIdentity sg_op mon_unit
  1: exact _.
R, S: Ring
Associative sg_op
R, S: Ring
LeftIdentity sg_op mon_unit
R, S: Ring
RightIdentity sg_op mon_unit
  {
R, S: Ring
Associative sg_op intros [r1 s1] [r2 s2] [r3 s3].
R, S: Ring
r1: R
s1: S
r2: R
s2: S
r3: R
s3: S
sg_op (r1, s1) (sg_op (r2, s2) (r3, s3)) =
sg_op (sg_op (r1, s1) (r2, s2)) (r3, s3)
    apply path_prod; cbn; apply rng_mult_assoc. }
R, S: Ring
LeftIdentity sg_op mon_unit
R, S: Ring
RightIdentity sg_op mon_unit
  1: intros [r1 s1]; apply path_prod; cbn; apply rng_mult_one_l.
R, S: Ring
RightIdentity sg_op mon_unit
  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
  snrapply 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
  snrapply 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: apply (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)
  snrapply 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))%type
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))%type
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))%type 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.

Global Instance hasbinaryproducts_ring : HasBinaryProducts Ring.
HasBinaryProducts Ring
Proof.
HasBinaryProducts Ring
  intros R S.
R, S: Ring
BinaryProduct R S
  snrapply 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) : Ring.
R, S: Ring
f: R $-> S
Ring
Proof.
R, S: Ring
f: R $-> S
Ring
  snrapply (Build_Ring (abgroup_image f)).
R, S: Ring
f: R $-> S
Mult (abgroup_image f)
R, S: Ring
f: R $-> S
One (abgroup_image f)
R, S: Ring
f: R $-> S
LeftDistribute mult group_sgop
R, S: Ring
f: R $-> S
RightDistribute mult group_sgop
R, S: Ring
f: R $-> S
IsMonoid (abgroup_image f)
  {
R, S: Ring
f: R $-> S
Mult (abgroup_image f) simpl.
R, S: Ring
f: R $-> S
Mult {b : S & Tr (-1) {a : R & f a = b}}
    intros [x p] [y q].
R, S: Ring
f: R $-> S
x: S
p: Tr (-1) {a : R & f a = x}
y: S
q: Tr (-1) {a : R & f a = y}
{b : S & Tr (-1) {a : R & f a = b}}
    exists (x * y).
R, S: Ring
f: R $-> S
x: S
p: Tr (-1) {a : R & f a = x}
y: S
q: Tr (-1) {a : R & f a = y}
Tr (-1) {a : R & f a = x * y}
    strip_truncations; apply tr.
R, S: Ring
f: R $-> S
x, y: S
q: {a : R & f a = y}
p: {a : R & f a = x}
{a : R & f a = x * y}
    destruct p as [p p'], q as [q q'].
R, S: Ring
f: R $-> S
x, y: S
q: R
q': f q = y
p: R
p': f p = x
{a : R & f a = x * y}
    exists (p * q).
R, S: Ring
f: R $-> S
x, y: S
q: R
q': f q = y
p: R
p': f p = x
f (p * q) = x * y
    refine (rng_homo_mult _ _ _ @ _).
R, S: Ring
f: R $-> S
x, y: S
q: R
q': f q = y
p: R
p': f p = x
f p * f q = x * y
    f_ap. }
R, S: Ring
f: R $-> S
One (abgroup_image f)
R, S: Ring
f: R $-> S
LeftDistribute mult group_sgop
R, S: Ring
f: R $-> S
RightDistribute mult group_sgop
R, S: Ring
f: R $-> S
IsMonoid (abgroup_image f)
  {
R, S: Ring
f: R $-> S
One (abgroup_image f) exists 1.
R, S: Ring
f: R $-> S
grp_image f 1
    apply tr.
R, S: Ring
f: R $-> S
{a : R & f a = 1}
    exists 1.
R, S: Ring
f: R $-> S
f 1 = 1
    exact (rng_homo_one f). }
R, S: Ring
f: R $-> S
LeftDistribute mult group_sgop
R, S: Ring
f: R $-> S
RightDistribute mult group_sgop
R, S: Ring
f: R $-> S
IsMonoid (abgroup_image f)
  (** Much of this proof is doing the same thing over, so we use some compact tactics. *)
  all: repeat split.
R, S: Ring
f: R $-> S
LeftDistribute mult group_sgop
R, S: Ring
f: R $-> S
RightDistribute mult group_sgop
R, S: Ring
f: R $-> S
IsHSet (abgroup_image f)
R, S: Ring
f: R $-> S
Associative sg_op
R, S: Ring
f: R $-> S
LeftIdentity sg_op mon_unit
R, S: Ring
f: R $-> S
RightIdentity sg_op mon_unit
  3: exact _.
R, S: Ring
f: R $-> S
LeftDistribute mult group_sgop
R, S: Ring
f: R $-> S
RightDistribute mult group_sgop
R, S: Ring
f: R $-> S
Associative sg_op
R, S: Ring
f: R $-> S
LeftIdentity sg_op mon_unit
R, S: Ring
f: R $-> S
RightIdentity sg_op mon_unit
  all: repeat intros [].
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
proj0: S
proj3: grp_image f proj0
proj4: S
proj5: grp_image f proj4
(proj1; proj2) *
group_sgop (proj0; proj3) (proj4; proj5) =
group_sgop ((proj1; proj2) * (proj0; proj3))
  ((proj1; proj2) * (proj4; proj5))
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
proj0: S
proj3: grp_image f proj0
proj4: S
proj5: grp_image f proj4
group_sgop (proj1; proj2) (proj0; proj3) *
(proj4; proj5) =
group_sgop ((proj1; proj2) * (proj4; proj5))
  ((proj0; proj3) * (proj4; proj5))
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
proj0: S
proj3: grp_image f proj0
proj4: S
proj5: grp_image f proj4
sg_op (proj1; proj2)
  (sg_op (proj0; proj3) (proj4; proj5)) =
sg_op (sg_op (proj1; proj2) (proj0; proj3))
  (proj4; proj5)
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
sg_op mon_unit (proj1; proj2) = (proj1; proj2)
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
sg_op (proj1; proj2) mon_unit = (proj1; proj2)
  all: apply path_sigma_hprop; cbn.
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
proj0: S
proj3: grp_image f proj0
proj4: S
proj5: grp_image f proj4
proj1 * sg_op proj0 proj4 =
sg_op (proj1 * proj0) (proj1 * proj4)
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
proj0: S
proj3: grp_image f proj0
proj4: S
proj5: grp_image f proj4
sg_op proj1 proj0 * proj4 =
sg_op (proj1 * proj4) (proj0 * proj4)
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
proj0: S
proj3: grp_image f proj0
proj4: S
proj5: grp_image f proj4
proj1 * (proj0 * proj4) = proj1 * proj0 * proj4
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
1 * proj1 = proj1
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
proj1 * 1 = proj1
  1: apply distribute_l.
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
proj0: S
proj3: grp_image f proj0
proj4: S
proj5: grp_image f proj4
sg_op proj1 proj0 * proj4 =
sg_op (proj1 * proj4) (proj0 * proj4)
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
proj0: S
proj3: grp_image f proj0
proj4: S
proj5: grp_image f proj4
proj1 * (proj0 * proj4) = proj1 * proj0 * proj4
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
1 * proj1 = proj1
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
proj1 * 1 = proj1
  1: apply distribute_r.
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
proj0: S
proj3: grp_image f proj0
proj4: S
proj5: grp_image f proj4
proj1 * (proj0 * proj4) = proj1 * proj0 * proj4
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
1 * proj1 = proj1
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
proj1 * 1 = proj1
  1: apply associativity.
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
1 * proj1 = proj1
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
proj1 * 1 = proj1
  1: apply left_identity.
R, S: Ring
f: R $-> S
proj1: S
proj2: grp_image f proj1
proj1 * 1 = proj1
  apply right_identity.
Defined.

Lemma rng_homo_image_incl {R S} (f : RingHomomorphism R S)
  : rng_image f $-> S.
R, S: Ring
f: RingHomomorphism R S
rng_image f $-> S
Proof.
R, S: Ring
f: RingHomomorphism R S
rng_image f $-> S
  snrapply 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 ≅ S.
R, S: Ring
f: RingHomomorphism R S
issurj: IsConnMap (Tr (-1)) f
rng_image f ≅ S
Proof.
R, S: Ring
f: RingHomomorphism R S
issurj: IsConnMap (Tr (-1)) f
rng_image f ≅ S
  snrapply 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 strucutres. 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
  snrapply 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. *)
Global Instance is0functor_rng_op : Is0Functor rng_op.
Is0Functor rng_op
Proof.
Is0Functor rng_op
  snrapply 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
  snrapply 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.

Global Instance is1functor_rng_op : Is1Functor rng_op.
Is1Functor rng_op
Proof.
Is1Functor rng_op
  snrapply 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.

(** ** More Ring laws *)

(** 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.