Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Spaces.Finite.Fin.
Require Import Classes.interfaces.canonical_names.
Require Import Algebra.Rings.Ring.
Require Import Algebra.Groups.Subgroup.
Require Import Algebra.AbGroups.AbelianGroup.
Require Import WildCat.Core.

Declare Scope ideal_scope.
Delimit Scope ideal_scope with ideal.
Local Open Scope ideal_scope.

(** * Left, Right and Two-sided Ideals *)

(** ** Definition of Ideals *)

(** An additive subgroup [I] of a ring [R] is a left ideal when it is closed under multiplication on the left. *)
Class IsLeftIdeal {R : Ring} (I : Subgroup R) :=
  isleftideal (r x : R) : I x -> I (r * x).

(** An additive subgroup [I] of a ring [R] is a right ideal when it is closed under multiplication on the right. We define this using the opposite ring allowing us to reduce redundancy between left and right ideals. *)
Class IsRightIdeal {R : Ring} (I : Subgroup R) :=
  isrightideal_isleftideal_op :: IsLeftIdeal (R := rng_op R) I.

Definition isrightideal {R : Ring} (I : Subgroup R) (x r : R)
  : IsRightIdeal I -> I x -> I (x * r)
  := fun _ => isleftideal (R := rng_op R) r x.

(** An additive subgroup [I] of a ring [R] is a two-sided ideal when it is both a left and right ideal. In this case we just call it an ideal. *)
Class IsIdeal {R : Ring} (I : Subgroup R) := {
  ideal_isleftideal :: IsLeftIdeal I;
  ideal_isrightideal :: IsRightIdeal I;
}.
Definition issig_IsIdeal {R : Ring} (I : Subgroup R) : _ <~> IsIdeal I := ltac:(issig).
Hint Immediate Build_IsIdeal : typeclass_instances.

(** Any two-sided ideal is also a two-sided ideal of the opposite ring. *)
Instance isideal_op {R : Ring} (I : Subgroup R)
  : IsIdeal I -> IsIdeal (R := rng_op R) I.
R: Ring
I: Subgroup R
IsIdeal I -> IsIdeal I
Proof.
R: Ring
I: Subgroup R
IsIdeal I -> IsIdeal I
  intros [? ?]; exact _.
Defined.

(** A left ideal of a ring [R] is a subgroup [I] of [R] which is closed under left multiplication. *)
Record LeftIdeal (R : Ring) := {
  leftideal_subgroup :> Subgroup R;
  leftideal_isleftideal :: IsLeftIdeal leftideal_subgroup;
}.
Definition issig_LeftIdeal (R : Ring) : _ <~> LeftIdeal R := ltac:(issig).

(** A right ideal of a ring [R] is a subgroup [I] of [R] which is closed under right multiplication. *)
Definition RightIdeal (R : Ring) := LeftIdeal (rng_op R).

Instance isrightdeal_rightideal {R} (I : RightIdeal R)
  : IsRightIdeal (R:=R) I
  := leftideal_isleftideal _ I.

Definition Build_RightIdeal (R : Ring) (I : Subgroup R) (H : IsRightIdeal I)
  : RightIdeal R
  := Build_LeftIdeal (rng_op R) I H.

Definition issig_RightIdeal (R : Ring)
  : {I : Subgroup R& IsRightIdeal (R:=R) I} <~> RightIdeal R
  := ltac:(issig).

(** A two-sided ideal of a ring [R], or just an ideal, is a subgroup [I] of [R] which is closed under both left and right multiplication. *)
Record Ideal (R : Ring) := {
  ideal_subgroup :> Subgroup R;
  ideal_isideal :: IsIdeal ideal_subgroup;
}.
Definition issig_Ideal (R : Ring) : _ <~> Ideal R := ltac:(issig).

Definition ideal_op (R : Ring) : Ideal R -> Ideal (rng_op R)
  := fun I => Build_Ideal (rng_op R) I _.
Coercion ideal_op : Ideal >-> Ideal.

(** *** Truncatedness properties *)

Section IdealTrunc.
  (** Assuming [Funext] we can show that the ideal predicates are propositions. *) 
  Context `{Funext}.

  (** Being a left ideal is a proposition. *)
  #[export] Instance ishprop_isleftideal {R : Ring} (I : Subgroup R)
    : IsHProp (IsLeftIdeal I) := ltac:(unfold IsLeftIdeal; exact _).

  (** Being a right ideal is a proposition. *)
  #[export] Instance ishprop_isrightideal `{Funext} {R : Ring} (I : Subgroup R)
    : IsHProp (IsRightIdeal I) :=  ishprop_isleftideal _.

  (** Being a two-sided ideal is a proposition. *)
  #[export] Instance ishprop_isideal {R : Ring} (I : Subgroup R)
    : IsHProp (IsIdeal I)
    := istrunc_equiv_istrunc _ (issig_IsIdeal I).

  (** Assuming [Univalence] we can show that the ideal types are sets. Note that univalence is only used to prove that the type of [Subgroup]s is a set. *)
  Context `{Univalence}.

  (** The type of left ideals is a set. *)
  #[export] Instance ishset_leftideal {R : Ring} : IsHSet (LeftIdeal R)
    := istrunc_equiv_istrunc _ (issig_LeftIdeal R).

  (** The type of right ideals is a set. *)
  #[export] Instance ishset_rightideal {R : Ring} : IsHSet (RightIdeal R)
    := _.

  (** The type of ideals is a set. *)
  #[export] Instance ishset_ideal {R : Ring} : IsHSet (Ideal R)
    := istrunc_equiv_istrunc _ (issig_Ideal R).

End IdealTrunc.

(** *** Conversion between Ideals *)

(** Every ideal is a left ideal. *)
Definition leftideal_of_ideal {R : Ring} : Ideal R -> LeftIdeal R
  := fun I => Build_LeftIdeal R I _.
Coercion leftideal_of_ideal : Ideal >-> LeftIdeal.

(** Every ideal is a right ideal. *)
Definition rightideal_of_ideal {R : Ring} : Ideal R -> RightIdeal R
  := fun I => Build_RightIdeal R I _.
Coercion rightideal_of_ideal : Ideal >-> RightIdeal.

(** *** Easy properties of ideals *)

(** Here are some lemmas for proving certain elements are in an ideal. They are just special cases of the underlying subgroup lemmas. We write them out for clarity. Note that [I] isn't actually assumed to be an ideal but only a subgroup. *)
Section IdealElements.
  Context {R : Ring} (I : Subgroup R) (a b : R).
  Definition ideal_in_zero : I ring_zero := subgroup_in_unit I.
  Definition ideal_in_plus : I a -> I b -> I (a + b) := subgroup_in_op I a b.
  Definition ideal_in_negate  : I a -> I (- a) := subgroup_in_inv  I a.
  Definition ideal_in_negate' : I (- a) -> I a := subgroup_in_inv' I a.
  Definition ideal_in_plus_negate : I a -> I b -> I (a - b) := subgroup_in_op_inv I a b.
  Definition ideal_in_negate_plus : I a -> I b -> I (-a + b) := subgroup_in_inv_op I a b.
  Definition ideal_in_plus_l : I (a + b) -> I b -> I a := subgroup_in_op_l I a b.
  Definition ideal_in_plus_r : I (a + b) -> I a -> I b := subgroup_in_op_r I a b.
End IdealElements.

(** ** Constructions of ideals *)

(** *** Zero Ideal *)

(** The trivial subgroup is a left ideal. *)
Instance isleftideal_trivial_subgroup (R : Ring)
  : IsLeftIdeal (trivial_subgroup R).
R: Ring
IsLeftIdeal (trivial_subgroup R)
Proof.
R: Ring
IsLeftIdeal (trivial_subgroup R)
  intros r x p.
R: Ring
r, x: R
p: trivial_subgroup R x
trivial_subgroup R (r * x)
  rhs_V napply (rng_mult_zero_r).
R: Ring
r, x: R
p: trivial_subgroup R x
r * x = ?Goal0 * 0
  f_ap.
Defined.

(** The trivial subgroup is a right ideal. *)
Instance isrightideal_trivial_subgroup (R : Ring)
  : IsRightIdeal (trivial_subgroup R)
  := isleftideal_trivial_subgroup _.

(** The trivial subgroup is an ideal. *)
Instance isideal_trivial_subgroup (R : Ring)
  : IsIdeal (trivial_subgroup R)
  := {}.

(** We call the trivial subgroup the "zero ideal". *)
Definition ideal_zero (R : Ring) : Ideal R := Build_Ideal R _ _. 

(** *** The unit ideal *)

(** The maximal subgroup is a left ideal. *)
Instance isleftideal_maximal_subgroup (R : Ring)
  : IsLeftIdeal (maximal_subgroup R)
  := ltac:(done).

(** The maximal subgroup is a right ideal. *)
Instance isrightideal_maximal_subgroup (R : Ring)
  : IsRightIdeal (maximal_subgroup R)
  := isleftideal_maximal_subgroup _.

(** The maximal subgroup is an ideal.  *)
Instance isideal_maximal_subgroup (R : Ring)
  : IsIdeal (maximal_subgroup R)
  := {}.

(** We call the maximal subgroup the "unit ideal". *)
Definition ideal_unit (R : Ring) : Ideal R
  := Build_Ideal R _ (isideal_maximal_subgroup R).

(** *** Intersection of ideals *)

(** Intersections of underlying subgroups of left ideals are again left ideals. *)
Instance isleftideal_subgroup_intersection (R : Ring) (I J : Subgroup R)
  `{IsLeftIdeal R I, IsLeftIdeal R J}
  : IsLeftIdeal (subgroup_intersection I J).
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
IsLeftIdeal (subgroup_intersection I J)
Proof.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
IsLeftIdeal (subgroup_intersection I J)
  intros r x [a b]; split; by apply isleftideal.
Defined.

(** Intersections of underlying subgroups of right ideals are again right ideals. *)
Instance isrightideal_subgroup_intersection (R : Ring) (I J : Subgroup R)
  `{IsRightIdeal R I, IsRightIdeal R J}
  : IsRightIdeal (subgroup_intersection I J)
  := isleftideal_subgroup_intersection _ _ _.

(** Intersections of underlying subgroups of ideals are again ideals. *)
Instance isideal_subgroup_intersection (R : Ring) (I J : Subgroup R)
  `{IsIdeal R I, IsIdeal R J}
  : IsIdeal (subgroup_intersection I J)
  := {}.

(** Intersection of left ideals. *)
Definition leftideal_intersection {R : Ring}
  : LeftIdeal R -> LeftIdeal R -> LeftIdeal R
  := fun I J => Build_LeftIdeal R (subgroup_intersection I J) _.

(** Intersection of right ideals. *)
Definition rightideal_intersection {R : Ring}
  : RightIdeal R -> RightIdeal R -> RightIdeal R
  := leftideal_intersection.

(** Intersection of ideals. *)
Definition ideal_intersection {R : Ring}
  : Ideal R -> Ideal R -> Ideal R
  := fun I J => Build_Ideal R (subgroup_intersection I J) _.

(** *** Sum of ideals *)

(** The subgroup product of left ideals is again an ideal. *)
Instance isleftideal_subgroup_product (R : Ring) (I J : Subgroup R)
  `{IsLeftIdeal R I, IsLeftIdeal R J}
  : IsLeftIdeal (subgroup_product I J).
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
IsLeftIdeal (subgroup_product I J)
Proof.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
IsLeftIdeal (subgroup_product I J)
  intros r.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
forall x : R,
subgroup_product I J x -> subgroup_product I J (r * x)
  napply subgroup_product_ind.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
forall x : R, I x -> subgroup_product I J (r * x)
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
forall x : R, J x -> subgroup_product I J (r * x)
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
subgroup_product I J (r * mon_unit)
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
forall x y : R,
subgroup_generated_type
  (fun x0 : R => (I x0 + J x0)%type) x ->
subgroup_generated_type
  (fun x0 : R => (I x0 + J x0)%type) y ->
subgroup_product I J (r * x) ->
subgroup_product I J (r * y) ->
subgroup_product I J (r * sg_op x (- y))
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
forall x : R,
subgroup_product I J x ->
IsHProp (subgroup_product I J (r * x))
  -
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
forall x : R, I x -> subgroup_product I J (r * x) intros x p.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r, x: R
p: I x
subgroup_product I J (r * x)
    apply tr, sgt_in.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r, x: R
p: I x
(I (mult r x) + J (mult r x))%type
    left; by apply isleftideal.
  -
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
forall x : R, J x -> subgroup_product I J (r * x) intros x p.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r, x: R
p: J x
subgroup_product I J (r * x)
    apply tr, sgt_in.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r, x: R
p: J x
(I (mult r x) + J (mult r x))%type
    right; by apply isleftideal.
  -
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
subgroup_product I J (r * mon_unit) apply tr, sgt_in.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
(I (mult r mon_unit) + J (mult r mon_unit))%type
    left; apply isleftideal.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
I mon_unit
    apply ideal_in_zero.
  -
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
forall x y : R,
subgroup_generated_type
  (fun x0 : R => (I x0 + J x0)%type) x ->
subgroup_generated_type
  (fun x0 : R => (I x0 + J x0)%type) y ->
subgroup_product I J (r * x) ->
subgroup_product I J (r * y) ->
subgroup_product I J (r * sg_op x (- y)) intros x y p q IHp IHq; cbn beta.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r, x, y: R
p: subgroup_generated_type
  (fun x : R => (I x + J x)%type) x
q: subgroup_generated_type
  (fun x : R => (I x + J x)%type) y
IHp: subgroup_product I J (r * x)
IHq: subgroup_product I J (r * y)
subgroup_product I J (r * sg_op x (- y))
    rewrite rng_dist_l.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r, x, y: R
p: subgroup_generated_type
  (fun x : R => (I x + J x)%type) x
q: subgroup_generated_type
  (fun x : R => (I x + J x)%type) y
IHp: subgroup_product I J (r * x)
IHq: subgroup_product I J (r * y)
subgroup_product I J (r * x + r * - y)
    rewrite rng_mult_negate_r.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r, x, y: R
p: subgroup_generated_type
  (fun x : R => (I x + J x)%type) x
q: subgroup_generated_type
  (fun x : R => (I x + J x)%type) y
IHp: subgroup_product I J (r * x)
IHq: subgroup_product I J (r * y)
subgroup_product I J (r * x - r * y)
    by apply subgroup_in_op_inv.
  -
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
forall x : R,
subgroup_product I J x ->
IsHProp (subgroup_product I J (r * x)) exact _.
Defined.

(** The subgroup product of right ideals is again an ideal. *)
Instance isrightideal_subgroup_product (R : Ring) (I J : Subgroup R)
  `{IsRightIdeal R I, IsRightIdeal R J}
  : IsRightIdeal (subgroup_product I J)
  := isleftideal_subgroup_product _ _ _.

(** The subgroup product of ideals is again an ideal. *)
Instance isideal_subgroup_product (R : Ring) (I J : Subgroup R)
  `{IsIdeal R I, IsIdeal R J}
  : IsIdeal (subgroup_product I J)
  := {}.

(** Sum of left ideals. *)
Definition leftideal_sum {R : Ring}
  : LeftIdeal R -> LeftIdeal R -> LeftIdeal R
  := fun I J => Build_LeftIdeal R (subgroup_product I J) _.

(** Sum of right ideals. *)
Definition rightideal_sum {R : Ring}
  : RightIdeal R -> RightIdeal R -> RightIdeal R
  := leftideal_sum.

(** Sum of ideals. *)
Definition ideal_sum {R : Ring}
  : Ideal R -> Ideal R -> Ideal R
  := fun I J => Build_Ideal R (subgroup_product I J) _.

Definition ideal_sum_ind {R : Ring} (I J : Ideal R)
  (P : forall x, ideal_sum I J x -> Type)
  (P_I_in : forall x y, P x (tr (sgt_in (inl y))))
  (P_J_in : forall x y, P x (tr (sgt_in (inr y))))
  (P_unit : P mon_unit (tr sgt_unit))
  (P_op : forall x y h k, P x (tr h) -> P y (tr k) -> P (x - y) (tr (sgt_op h k)))
  `{forall x y, IsHProp (P x y)}
  : forall x (p : ideal_sum I J x), P x p
  := subgroup_product_ind I J P P_I_in P_J_in P_unit P_op.

(** *** Product of ideals *)

(** First we form the "naive" product of ideals { a * b | a ∈ I /\ b ∈ J }. Note that this is not an ideal, but we can fix this. *)
Inductive ideal_product_naive_type {R : Ring} (I J : Subgroup R) : R -> Type :=
| ipn_in : forall x y, I x -> J y -> ideal_product_naive_type I J (x * y).

(** We instead consider the subgroup generated by this naive product and later prove it happens to be an ideal. Note that the subgroup generated by a set and the ideal generated by a set are not the same in general. *)
Definition ideal_product_type {R : Ring} (I J : Subgroup R) : Subgroup R
  := subgroup_generated (G := R) (ideal_product_naive_type I J). 

(** The product of left ideals is a left ideal. *)
Instance isleftideal_ideal_product_type {R : Ring} (I J : Subgroup R)
  `{IsLeftIdeal R I, IsLeftIdeal R J}
  : IsLeftIdeal (ideal_product_type I J).
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
IsLeftIdeal (ideal_product_type I J)
Proof.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
IsLeftIdeal (ideal_product_type I J)
  intro r.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
forall x : R,
ideal_product_type I J x ->
ideal_product_type I J (r * x)
  napply (functor_subgroup_generated _ _ (grp_homo_rng_left_mult r)).
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r: R
forall g : R,
ideal_product_naive_type I J g ->
ideal_product_naive_type I J
  (grp_homo_rng_left_mult r g)
  intros s [s1 s2 p1 p2]; cbn.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r, s, s1, s2: R
p1: I s1
p2: J s2
ideal_product_naive_type I J (r * (s1 * s2))
  rewrite simple_associativity.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r, s, s1, s2: R
p1: I s1
p2: J s2
ideal_product_naive_type I J (r * s1 * s2)
  nrefine (ipn_in I J (r * s1) s2 _ p2).
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsLeftIdeal J
r, s, s1, s2: R
p1: I s1
p2: J s2
I (r * s1)
  by apply isleftideal.
Defined.

(** The product of right ideals is a right ideal. *)
Instance isrightideal_ideal_product_type {R : Ring} (I J : Subgroup R)
  `{IsRightIdeal R I, IsRightIdeal R J}
  : IsRightIdeal (ideal_product_type I J).
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsRightIdeal J
IsRightIdeal (ideal_product_type I J)
Proof.
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsRightIdeal J
IsRightIdeal (ideal_product_type I J)
  intro r.
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsRightIdeal J
r: rng_op R
forall x : rng_op R,
ideal_product_type I J x ->
ideal_product_type I J (r * x)
  napply (functor_subgroup_generated _ _ (grp_homo_rng_right_mult (R:=R) r)).
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsRightIdeal J
r: rng_op R
forall g : R,
ideal_product_naive_type I J g ->
ideal_product_naive_type I J
  (grp_homo_rng_right_mult r g)
  intros s [s1 s2 p1 p2]; cbn.
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsRightIdeal J
r: rng_op R
s, s1, s2: R
p1: I s1
p2: J s2
ideal_product_naive_type I J (s1 * s2 * r)
  rewrite <- simple_associativity.
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsRightIdeal J
r: rng_op R
s, s1, s2: R
p1: I s1
p2: J s2
ideal_product_naive_type I J (s1 * (s2 * r))
  nrefine (ipn_in I J s1 (s2 * r) p1 _).
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsRightIdeal J
r: rng_op R
s, s1, s2: R
p1: I s1
p2: J s2
J (s2 * r)
  by apply isrightideal.
Defined.

(** The product of ideals is an ideal. *)
Instance isideal_ideal_product_type {R : Ring} (I J : Subgroup R)
  `{IsIdeal R I, IsIdeal R J}
  : IsIdeal (ideal_product_type I J)
  := {}. 

(** Product of left ideals. *)
Definition leftideal_product {R : Ring}
  : LeftIdeal R -> LeftIdeal R -> LeftIdeal R
  := fun I J => Build_LeftIdeal R (ideal_product_type I J) _.

(** Product of right ideals. *)
Definition rightideal_product {R : Ring}
  : RightIdeal R -> RightIdeal R -> RightIdeal R
  := leftideal_product.

(** Product of ideals. *)
Definition ideal_product {R : Ring}
  : Ideal R -> Ideal R -> Ideal R
  := fun I J => Build_Ideal R (ideal_product_type I J) _.

(** *** The kernel of a ring homomorphism *)

(** The kernel of the underlying group homomorphism of a ring homomorphism is a left ideal. *)
Instance isleftideal_grp_kernel {R S : Ring} (f : RingHomomorphism R S)
  : IsLeftIdeal (grp_kernel f).
R, S: Ring
f: RingHomomorphism R S
IsLeftIdeal (grp_kernel f)
Proof.
R, S: Ring
f: RingHomomorphism R S
IsLeftIdeal (grp_kernel f)
  intros r x p.
R, S: Ring
f: RingHomomorphism R S
r, x: R
p: grp_kernel f x
grp_kernel f (r * x)
  lhs napply rng_homo_mult.
R, S: Ring
f: RingHomomorphism R S
r, x: R
p: grp_kernel f x
f r * f x = mon_unit
  rhs_V napply (rng_mult_zero_r (f r)).
R, S: Ring
f: RingHomomorphism R S
r, x: R
p: grp_kernel f x
f r * f x = f r * 0
  by apply ap.
Defined.

(** The kernel of the underlying group homomorphism of a ring homomorphism is a right ideal. *)
Instance isrightideal_grp_kernel {R S : Ring} (f : RingHomomorphism R S)
  : IsRightIdeal (grp_kernel f)
  := isleftideal_grp_kernel (fmap rng_op f).

(** The kernel of the underlying group homomorphism of a ring homomorphism is an ideal. *)
Instance isideal_grp_kernel {R S : Ring} (f : RingHomomorphism R S)
  : IsIdeal (grp_kernel f)
  := {}.

(** The kernel of a ring homomorphism is an ideal. *)
Definition ideal_kernel {R S : Ring} (f : RingHomomorphism R S) : Ideal R
  := Build_Ideal R (grp_kernel f) _.

(** *** Ideal generated by a subset *)

(** It seems tempting to define ideals generated by a subset in terms of subgroups generated by a subset but this does not work. Left ideals also have to be closed under left multiplication by ring elements, and similarly for right and two sided ideals. Therefore we will do an analagous construction to the one done in Subgroup.v. *)

(** Underlying type family of a left ideal generated by subset. *)
Inductive leftideal_generated_type (R : Ring) (X : R -> Type) : R -> Type :=
(** It should contain all elements of the original family. *)
| ligt_in (r : R) : X r -> leftideal_generated_type R X r
(** It should contain zero. *)
| ligt_zero : leftideal_generated_type R X ring_zero
(** It should be closed under negation and addition. *)
| ligt_add_neg (r s : R)
  : leftideal_generated_type R X r
  -> leftideal_generated_type R X s
  -> leftideal_generated_type R X (r - s)
(** And finally, it should be closed under left multiplication. *)
| ligt_mul (r s : R)
  : leftideal_generated_type R X s
  -> leftideal_generated_type R X (r * s)
.

Arguments leftideal_generated_type {R} X r.
Arguments ligt_in {R X r}.
Arguments ligt_zero {R X}.
Arguments ligt_add_neg {R X r s}.
Arguments ligt_mul {R X r s}.

(** Left ideal generated by a subset. *)
Definition leftideal_generated@{u v} {R : Ring@{u}} (X : R -> Type@{v}) : LeftIdeal@{u v} R.
R: Ring
X: R -> Type
LeftIdeal R
Proof.
R: Ring
X: R -> Type
LeftIdeal R
  snapply Build_LeftIdeal.
R: Ring
X: R -> Type
Subgroup R
R: Ring
X: R -> Type
IsLeftIdeal ?leftideal_subgroup
  -
R: Ring
X: R -> Type
Subgroup R snapply Build_Subgroup'.
R: Ring
X: R -> Type
R -> Type
R: Ring
X: R -> Type
forall x : R, IsHProp (?H x)
R: Ring
X: R -> Type
?H mon_unit
R: Ring
X: R -> Type
forall x y : R, ?H x -> ?H y -> ?H (sg_op x (inv y))
    +
R: Ring
X: R -> Type
R -> Type exact (fun x => merely (leftideal_generated_type X x)).
    +
R: Ring
X: R -> Type
forall x : R,
IsHProp
  ((fun x0 : R =>
    trunctype_type
      (merely (leftideal_generated_type X x0))) x) exact _.
    +
R: Ring
X: R -> Type
(fun x : R =>
 trunctype_type
   (merely (leftideal_generated_type X x))) mon_unit apply tr, ligt_zero.
    +
R: Ring
X: R -> Type
forall x y : R,
(fun x0 : R =>
 trunctype_type
   (merely (leftideal_generated_type X x0))) x ->
(fun x0 : R =>
 trunctype_type
   (merely (leftideal_generated_type X x0))) y ->
(fun x0 : R =>
 trunctype_type
   (merely (leftideal_generated_type X x0)))
  (sg_op x (inv y)) intros x y p q; strip_truncations.
R: Ring
X: R -> Type
x, y: R
q: leftideal_generated_type X y
p: leftideal_generated_type X x
merely (leftideal_generated_type X (sg_op x (inv y)))
      by apply tr, ligt_add_neg.
  -
R: Ring
X: R -> Type
IsLeftIdeal
  (Build_Subgroup'
     (fun x : R =>
      merely (leftideal_generated_type X x))
     (tr ligt_zero)
     (fun (x y : R)
        (p : (fun x0 : R =>
              trunctype_type
                (merely
                   (leftideal_generated_type X x0))) x)
        (q : (fun x0 : R =>
              trunctype_type
                (merely
                   (leftideal_generated_type X x0))) y)
      =>
      Trunc_ind
        (fun
           _ : Trunc (-1)
                 (leftideal_generated_type X y) =>
         (fun x0 : R =>
          trunctype_type
            (merely (leftideal_generated_type X x0)))
           (sg_op x (inv y)))
        (fun q0 : leftideal_generated_type X y =>
         Trunc_ind
           (fun
              _ : Trunc (-1)
                    (leftideal_generated_type X x) =>
            merely
              (leftideal_generated_type X
                 (sg_op x (inv y))))
           (fun p0 : leftideal_generated_type X x =>
            tr (ligt_add_neg p0 q0)) p) q)) intros r x; apply Trunc_functor.
R: Ring
X: R -> Type
r, x: R
leftideal_generated_type X x ->
leftideal_generated_type X (r * x)
    exact ligt_mul.
Defined.

(** Right ideal generated by a subset. *)
Definition rightideal_generated@{u v} {R : Ring@{u}} (X : R -> Type@{v}) : RightIdeal@{u v} R
  := Build_RightIdeal R (leftideal_generated (R:=rng_op R) X) _.

(** Underlying type family of a two-sided ideal generated by subset. *)
Inductive ideal_generated_type (R : Ring) (X : R -> Type) : R -> Type :=
(** It should contain all elements of the original family. *)
| igt_in (r : R) : X r -> ideal_generated_type R X r
(** It should contain zero. *)
| igt_zero : ideal_generated_type R X ring_zero
(** It should be closed under negation and addition. *)
| igt_add_neg (r s : R)
  : ideal_generated_type R X r
  -> ideal_generated_type R X s
  -> ideal_generated_type R X (r - s)
(** And finally, it should be closed under left and right multiplication. *)
| igt_mul_l (r s : R)
  : ideal_generated_type R X s
  -> ideal_generated_type R X (r * s)
| igt_mul_r (r s : R)
  : ideal_generated_type R X r
  -> ideal_generated_type R X (r * s)
.

Arguments ideal_generated_type {R} X r.
Arguments igt_in {R X r}.
Arguments igt_zero {R X}.
Arguments igt_add_neg {R X r s}.
Arguments igt_mul_l {R X r s}.
Arguments igt_mul_r {R X r s}.

(** Two-sided ideal generated by a subset. *)
Definition ideal_generated {R : Ring} (X : R -> Type) : Ideal R.
R: Ring
X: R -> Type
Ideal R
Proof.
R: Ring
X: R -> Type
Ideal R
  snapply Build_Ideal; [|split].
R: Ring
X: R -> Type
Subgroup R
R: Ring
X: R -> Type
IsLeftIdeal ?ideal_subgroup
R: Ring
X: R -> Type
IsRightIdeal ?ideal_subgroup
  -
R: Ring
X: R -> Type
Subgroup R snapply Build_Subgroup'.
R: Ring
X: R -> Type
R -> Type
R: Ring
X: R -> Type
forall x : R, IsHProp (?H x)
R: Ring
X: R -> Type
?H mon_unit
R: Ring
X: R -> Type
forall x y : R, ?H x -> ?H y -> ?H (sg_op x (inv y))
    +
R: Ring
X: R -> Type
R -> Type exact (fun x => merely (ideal_generated_type X x)).
    +
R: Ring
X: R -> Type
forall x : R,
IsHProp
  ((fun x0 : R =>
    trunctype_type
      (merely (ideal_generated_type X x0))) x) exact _.
    +
R: Ring
X: R -> Type
(fun x : R =>
 trunctype_type (merely (ideal_generated_type X x)))
  mon_unit apply tr, igt_zero.
    +
R: Ring
X: R -> Type
forall x y : R,
(fun x0 : R =>
 trunctype_type (merely (ideal_generated_type X x0)))
  x ->
(fun x0 : R =>
 trunctype_type (merely (ideal_generated_type X x0)))
  y ->
(fun x0 : R =>
 trunctype_type (merely (ideal_generated_type X x0)))
  (sg_op x (inv y)) intros x y p q; strip_truncations.
R: Ring
X: R -> Type
x, y: R
q: ideal_generated_type X y
p: ideal_generated_type X x
merely (ideal_generated_type X (sg_op x (inv y)))
      by apply tr, igt_add_neg.
  -
R: Ring
X: R -> Type
IsLeftIdeal
  (Build_Subgroup'
     (fun x : R => merely (ideal_generated_type X x))
     (tr igt_zero)
     (fun (x y : R)
        (p : (fun x0 : R =>
              trunctype_type
                (merely (ideal_generated_type X x0)))
               x)
        (q : (fun x0 : R =>
              trunctype_type
                (merely (ideal_generated_type X x0)))
               y) =>
      Trunc_ind
        (fun _ : Trunc (-1) (ideal_generated_type X y)
         =>
         (fun x0 : R =>
          trunctype_type
            (merely (ideal_generated_type X x0)))
           (sg_op x (inv y)))
        (fun q0 : ideal_generated_type X y =>
         Trunc_ind
           (fun
              _ : Trunc (-1)
                    (ideal_generated_type X x) =>
            merely
              (ideal_generated_type X
                 (sg_op x (inv y))))
           (fun p0 : ideal_generated_type X x =>
            tr (igt_add_neg p0 q0)) p) q)) intros r x; apply Trunc_functor.
R: Ring
X: R -> Type
r, x: R
ideal_generated_type X x ->
ideal_generated_type X (r * x)
    exact igt_mul_l.
  -
R: Ring
X: R -> Type
IsRightIdeal
  (Build_Subgroup'
     (fun x : R => merely (ideal_generated_type X x))
     (tr igt_zero)
     (fun (x y : R)
        (p : (fun x0 : R =>
              trunctype_type
                (merely (ideal_generated_type X x0)))
               x)
        (q : (fun x0 : R =>
              trunctype_type
                (merely (ideal_generated_type X x0)))
               y) =>
      Trunc_ind
        (fun _ : Trunc (-1) (ideal_generated_type X y)
         =>
         (fun x0 : R =>
          trunctype_type
            (merely (ideal_generated_type X x0)))
           (sg_op x (inv y)))
        (fun q0 : ideal_generated_type X y =>
         Trunc_ind
           (fun
              _ : Trunc (-1)
                    (ideal_generated_type X x) =>
            merely
              (ideal_generated_type X
                 (sg_op x (inv y))))
           (fun p0 : ideal_generated_type X x =>
            tr (igt_add_neg p0 q0)) p) q)) intros x r; apply Trunc_functor.
R: Ring
X: R -> Type
x, r: rng_op R
ideal_generated_type X r ->
ideal_generated_type X (x * r)
    exact igt_mul_r.
Defined. 

(** *** Finitely generated ideal *)

(** Finitely generated ideals *)
Definition ideal_generated_finite {R : Ring} {n : nat} (X : Fin n -> R) : Ideal R.
R: Ring
n: nat
X: Fin n -> R
Ideal R
Proof.
R: Ring
n: nat
X: Fin n -> R
Ideal R
  apply ideal_generated.
R: Ring
n: nat
X: Fin n -> R
R -> Type
  exact (hfiber X).
Defined.

(** *** Principal ideals *)

(** A principal ideal is an ideal generated by a single element. *)
Definition ideal_principal {R : Ring} (x : R) : Ideal R
  := ideal_generated (fun r => x = r).

(** *** Ideal equality *)

(** Classically, set based equality suffices for ideals. Since we are talking about predicates, we use pointwise iffs. This can of course be shown to be equivalent to the identity type. *)
Definition ideal_eq {R : Ring} (I J : Subgroup R) := forall x, I x <-> J x.

(** With univalence we can characterize equality of ideals. *)
Lemma equiv_path_ideal `{Univalence} {R : Ring} {I J : Ideal R} : ideal_eq I J <~> I = J.
H: Univalence
R: Ring
I, J: Ideal R
ideal_eq I J <~> I = J
Proof.
H: Univalence
R: Ring
I, J: Ideal R
ideal_eq I J <~> I = J
  refine ((equiv_ap' (issig_Ideal R)^-1 _ _)^-1 oE _).
H: Univalence
R: Ring
I, J: Ideal R
ideal_eq I J <~>
(issig_Ideal R)^-1%equiv I =
(issig_Ideal R)^-1%equiv J
  refine (equiv_path_sigma_hprop _ _ oE _).
H: Univalence
R: Ring
I, J: Ideal R
ideal_eq I J <~>
((issig_Ideal R)^-1%equiv I).1 =
((issig_Ideal R)^-1%equiv J).1
  rapply equiv_path_subgroup'.
Defined.

(** Under funext, ideal equality is a proposition. *)
Instance ishprop_ideal_eq `{Funext} {R : Ring} (I J : Ideal R)
  : IsHProp (ideal_eq I J) := _.

(** Ideal equality is reflexive. *)
Instance reflexive_ideal_eq {R : Ring} : Reflexive (@ideal_eq R).
R: Ring
Reflexive ideal_eq
Proof.
R: Ring
Reflexive ideal_eq
  intros I x; by split.
Defined.

(** Ideal equality is symmetric. *)
Instance symmetric_ideal_eq {R : Ring} : Symmetric (@ideal_eq R).
R: Ring
Symmetric ideal_eq
Proof.
R: Ring
Symmetric ideal_eq
  intros I J p x; specialize (p x); by symmetry.
Defined.

(** Ideal equality is transitive. *)
Instance transitive_ideal_eq {R : Ring} : Transitive (@ideal_eq R).
R: Ring
Transitive ideal_eq
Proof.
R: Ring
Transitive ideal_eq
  intros I J K p q x; specialize (p x); specialize (q x); by transitivity (J x).
Defined.

(** *** Subset relation on ideals *)

(** We define the subset relation on ideals in the usual way: *)
Definition ideal_subset {R : Ring} (I J : Subgroup R) := (forall x, I x -> J x).

(** The subset relation is reflexive. *)
Instance reflexive_ideal_subset {R : Ring} : Reflexive (@ideal_subset R)
  := fun _ _ => idmap.

(** The subset relation is transitive. *)
Instance transitive_ideal_subset {R : Ring} : Transitive (@ideal_subset R).
R: Ring
Transitive ideal_subset
Proof.
R: Ring
Transitive ideal_subset
  intros x y z p q a.
R: Ring
x, y, z: Subgroup R
p: ideal_subset x y
q: ideal_subset y z
a: R
x a -> z a
  exact (q a o p a).
Defined.

(** We can coerce equality to the subset relation, since equality is defined to be the subset relation in each direction. *)
Coercion ideal_eq_subset {R : Ring} {I J : Subgroup R} : ideal_eq I J -> ideal_subset I J.
R: Ring
I, J: Subgroup R
ideal_eq I J -> ideal_subset I J
Proof.
R: Ring
I, J: Subgroup R
ideal_eq I J -> ideal_subset I J
  intros f x; apply f.
Defined.

(** *** Quotient (a.k.a colon) ideals *)

(** The definitions here are not entirely standard, but will become so when considering only commutative rings. For the non-commutative case there isn't a lot written about ideal quotients. *)

(** The subgroup corresponding to the left ideal quotient. *)
Definition subgroup_leftideal_quotient {R : Ring} (I J : Subgroup R)
  : Subgroup R.
R: Ring
I, J: Subgroup R
Subgroup R
Proof.
R: Ring
I, J: Subgroup R
Subgroup R
  snapply Build_Subgroup'.
R: Ring
I, J: Subgroup R
R -> Type
R: Ring
I, J: Subgroup R
forall x : R, IsHProp (?H x)
R: Ring
I, J: Subgroup R
?H mon_unit
R: Ring
I, J: Subgroup R
forall x y : R, ?H x -> ?H y -> ?H (sg_op x (inv y))
  -
R: Ring
I, J: Subgroup R
R -> Type exact (fun r => merely (forall x, J x -> I (r * x))).
  -
R: Ring
I, J: Subgroup R
forall x : R,
IsHProp
  ((fun r : R =>
    trunctype_type
      (merely (forall x0 : R, J x0 -> I (r * x0)))) x) exact _.
  -
R: Ring
I, J: Subgroup R
(fun r : R =>
 trunctype_type
   (merely (forall x : R, J x -> I (r * x)))) mon_unit apply tr.
R: Ring
I, J: Subgroup R
forall x : R, J x -> I (mon_unit * x)
    intros r p.
R: Ring
I, J: Subgroup R
r: R
p: J r
I (mon_unit * r)
    rewrite rng_mult_zero_l.
R: Ring
I, J: Subgroup R
r: R
p: J r
I 0
    apply ideal_in_zero.
  -
R: Ring
I, J: Subgroup R
forall x y : R,
(fun r : R =>
 trunctype_type
   (merely (forall x0 : R, J x0 -> I (r * x0)))) x ->
(fun r : R =>
 trunctype_type
   (merely (forall x0 : R, J x0 -> I (r * x0)))) y ->
(fun r : R =>
 trunctype_type
   (merely (forall x0 : R, J x0 -> I (r * x0))))
  (sg_op x (inv y)) intros x y p q.
R: Ring
I, J: Subgroup R
x, y: R
p: (fun r : R =>
 trunctype_type
   (merely (forall x : R, J x -> I (r * x)))) x
q: (fun r : R =>
 trunctype_type
   (merely (forall x : R, J x -> I (r * x)))) y
(fun r : R =>
 trunctype_type
   (merely (forall x : R, J x -> I (r * x))))
  (sg_op x (inv y))
    strip_truncations; apply tr.
R: Ring
I, J: Subgroup R
x, y: R
q: forall x : R, J x -> I (y * x)
p: forall x0 : R, J x0 -> I (x * x0)
forall x0 : R, J x0 -> I (sg_op x (inv y) * x0)
    hnf; intros s j.
R: Ring
I, J: Subgroup R
x, y: R
q: forall x : R, J x -> I (y * x)
p: forall x0 : R, J x0 -> I (x * x0)
s: R
j: J s
I (sg_op x (inv y) * s)
    rewrite rng_dist_r.
R: Ring
I, J: Subgroup R
x, y: R
q: forall x : R, J x -> I (y * x)
p: forall x0 : R, J x0 -> I (x * x0)
s: R
j: J s
I (x * s + inv y * s)
    rewrite rng_mult_negate_l.
R: Ring
I, J: Subgroup R
x, y: R
q: forall x : R, J x -> I (y * x)
p: forall x0 : R, J x0 -> I (x * x0)
s: R
j: J s
I (x * s - y * s)
    apply ideal_in_plus_negate.
R: Ring
I, J: Subgroup R
x, y: R
q: forall x : R, J x -> I (y * x)
p: forall x0 : R, J x0 -> I (x * x0)
s: R
j: J s
I (x * s)
R: Ring
I, J: Subgroup R
x, y: R
q: forall x : R, J x -> I (y * x)
p: forall x0 : R, J x0 -> I (x * x0)
s: R
j: J s
I (y * s)
    +
R: Ring
I, J: Subgroup R
x, y: R
q: forall x : R, J x -> I (y * x)
p: forall x0 : R, J x0 -> I (x * x0)
s: R
j: J s
I (x * s) by apply p.
    +
R: Ring
I, J: Subgroup R
x, y: R
q: forall x : R, J x -> I (y * x)
p: forall x0 : R, J x0 -> I (x * x0)
s: R
j: J s
I (y * s) by apply q.
Defined.

(** The left ideal quotient of a left ideal is a left ideal. *)
Instance isleftideal_subgroup_leftideal_quotient {R : Ring}
  (I J : Subgroup R) `{IsLeftIdeal R I}
  : IsLeftIdeal (subgroup_leftideal_quotient I J).
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
IsLeftIdeal (subgroup_leftideal_quotient I J)
Proof.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
IsLeftIdeal (subgroup_leftideal_quotient I J)
  intros r x p.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
r, x: R
p: subgroup_leftideal_quotient I J x
subgroup_leftideal_quotient I J (r * x)
  strip_truncations; apply tr.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
r, x: R
p: forall x0 : R, J x0 -> I (x * x0)
forall x0 : R, J x0 -> I (r * x * x0)
  intros s j.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
r, x: R
p: forall x0 : R, J x0 -> I (x * x0)
s: R
j: J s
I (r * x * s)
  rewrite <- rng_mult_assoc.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
r, x: R
p: forall x0 : R, J x0 -> I (x * x0)
s: R
j: J s
I (r * (x * s))
  apply isleftideal.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
r, x: R
p: forall x0 : R, J x0 -> I (x * x0)
s: R
j: J s
I (x * s)
  by napply p.
Defined.

(** The left ideal quotient of a right ideal by a left ideal is a right ideal. *)
Instance isrightideal_subgroup_leftideal_quotient {R : Ring}
  (I J : Subgroup R) `{IsRightIdeal R I, IsLeftIdeal R J}
  : IsRightIdeal (subgroup_leftideal_quotient (R:=R) I J).
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsLeftIdeal J
IsRightIdeal (subgroup_leftideal_quotient I J)
Proof.
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsLeftIdeal J
IsRightIdeal (subgroup_leftideal_quotient I J)
  intros r x p.
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsLeftIdeal J
r, x: rng_op R
p: subgroup_leftideal_quotient I J x
subgroup_leftideal_quotient I J (r * x)
  strip_truncations; apply tr.
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsLeftIdeal J
r, x: rng_op R
p: forall x0 : R, J x0 -> I (x * x0)
forall x0 : R, J x0 -> I (r * x * x0)
  intros s j.
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsLeftIdeal J
r, x: rng_op R
p: forall x0 : R, J x0 -> I (x * x0)
s: R
j: J s
I (r * x * s)
  cbn in *.
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsLeftIdeal J
r, x: R
p: forall x0 : R, J x0 -> I (x * x0)
s: R
j: J s
I (ring_mult x r * s)
  rewrite <- rng_mult_assoc.
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsLeftIdeal J
r, x: R
p: forall x0 : R, J x0 -> I (x * x0)
s: R
j: J s
I (x * (r * s))
  apply p.
R: Ring
I, J: Subgroup R
H: IsRightIdeal I
H0: IsLeftIdeal J
r, x: R
p: forall x0 : R, J x0 -> I (x * x0)
s: R
j: J s
J (r * s)
  by rapply isleftideal.
Defined.

(** We define the left ideal quotient as a left ideal. *)
Definition leftideal_quotient {R : Ring}
  : LeftIdeal R -> Subgroup R -> LeftIdeal R
  := fun I J => Build_LeftIdeal R (subgroup_leftideal_quotient I J) _.

Definition subgroup_rightideal_quotient {R : Ring} (I J : Subgroup R) : Subgroup R
  := subgroup_leftideal_quotient (R:=rng_op R) I J. 

Instance isrightideal_subgroup_rightideal_quotient {R : Ring}
  (I J : Subgroup R) `{IsRightIdeal R I}
  : IsRightIdeal (subgroup_rightideal_quotient I J)
  := isleftideal_subgroup_leftideal_quotient (R:=rng_op R) I J.

Instance isleftideal_subgroup_rightideal_quotient {R : Ring}
  (I J : Subgroup R) `{H : IsLeftIdeal R I, IsRightIdeal R J}
  : IsLeftIdeal (subgroup_rightideal_quotient I J).
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsRightIdeal J
IsLeftIdeal (subgroup_rightideal_quotient I J)
Proof.
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsRightIdeal J
IsLeftIdeal (subgroup_rightideal_quotient I J)
  snapply (isrightideal_subgroup_leftideal_quotient (R:=rng_op R) I J).
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsRightIdeal J
IsRightIdeal I
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsRightIdeal J
IsLeftIdeal J
  -
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsRightIdeal J
IsRightIdeal I exact H.
  -
R: Ring
I, J: Subgroup R
H: IsLeftIdeal I
H0: IsRightIdeal J
IsLeftIdeal J exact _.
Defined.

(** We define the right ideal quotient as a right ideal. *)
Definition rightideal_quotient {R : Ring}
  : RightIdeal R -> Subgroup R -> RightIdeal R
  := fun I J => Build_RightIdeal R (subgroup_rightideal_quotient (R:=R) I J) _.

(** The ideal quotient is then the intersection of a left and right quotient of both two sided ideals. *)
Definition ideal_quotient {R : Ring}
  : Ideal R -> Ideal R -> Ideal R
  := fun I J =>
    Build_Ideal R
      (subgroup_intersection
        (leftideal_quotient I J)
        (rightideal_quotient I J))
      (Build_IsIdeal _ _ _ _).

(** *** Annihilator *)

(** The left annihilator of a subset is the set of elements that annihilate the subgroup with left multiplication. *)
Definition subgroup_ideal_left_annihilator {R : Ring} (S : R -> Type)
  : Subgroup R.
R: Ring
S: R -> Type
Subgroup R
Proof.
R: Ring
S: R -> Type
Subgroup R
  snapply Build_Subgroup'.
R: Ring
S: R -> Type
R -> Type
R: Ring
S: R -> Type
forall x : R, IsHProp (?H x)
R: Ring
S: R -> Type
?H mon_unit
R: Ring
S: R -> Type
forall x y : R, ?H x -> ?H y -> ?H (sg_op x (inv y))
  (** If we assume [Funext], then it isn't necessary to use [merely] here. *)
  -
R: Ring
S: R -> Type
R -> Type exact (fun r => merely (forall x, S x -> r * x = ring_zero)).
  -
R: Ring
S: R -> Type
forall x : R,
IsHProp
  ((fun r : R =>
    trunctype_type
      (merely
         (forall x0 : R, S x0 -> r * x0 = ring_zero)))
     x) exact _.
  -
R: Ring
S: R -> Type
(fun r : R =>
 trunctype_type
   (merely (forall x : R, S x -> r * x = ring_zero)))
  mon_unit apply tr.
R: Ring
S: R -> Type
forall x : R, S x -> mon_unit * x = ring_zero 
    intros r p.
R: Ring
S: R -> Type
r: R
p: S r
mon_unit * r = ring_zero
    apply rng_mult_zero_l.
  -
R: Ring
S: R -> Type
forall x y : R,
(fun r : R =>
 trunctype_type
   (merely (forall x0 : R, S x0 -> r * x0 = ring_zero)))
  x ->
(fun r : R =>
 trunctype_type
   (merely (forall x0 : R, S x0 -> r * x0 = ring_zero)))
  y ->
(fun r : R =>
 trunctype_type
   (merely (forall x0 : R, S x0 -> r * x0 = ring_zero)))
  (sg_op x (inv y)) intros x y p q.
R: Ring
S: R -> Type
x, y: R
p: (fun r : R =>
 trunctype_type
   (merely
      (forall x : R, S x -> r * x = ring_zero))) x
q: (fun r : R =>
 trunctype_type
   (merely
      (forall x : R, S x -> r * x = ring_zero))) y
(fun r : R =>
 trunctype_type
   (merely (forall x : R, S x -> r * x = ring_zero)))
  (sg_op x (inv y))
    strip_truncations; apply tr.
R: Ring
S: R -> Type
x, y: R
q: forall x : R, S x -> y * x = ring_zero
p: forall x0 : R, S x0 -> x * x0 = ring_zero
forall x0 : R,
S x0 -> sg_op x (inv y) * x0 = ring_zero
    intros r s.
R: Ring
S: R -> Type
x, y: R
q: forall x : R, S x -> y * x = ring_zero
p: forall x0 : R, S x0 -> x * x0 = ring_zero
r: R
s: S r
sg_op x (inv y) * r = ring_zero
    lhs rapply rng_dist_r.
R: Ring
S: R -> Type
x, y: R
q: forall x : R, S x -> y * x = ring_zero
p: forall x0 : R, S x0 -> x * x0 = ring_zero
r: R
s: S r
x * r + inv y * r = ring_zero
    rewrite (p r s).
R: Ring
S: R -> Type
x, y: R
q: forall x : R, S x -> y * x = ring_zero
p: forall x0 : R, S x0 -> x * x0 = ring_zero
r: R
s: S r
ring_zero + inv y * r = ring_zero
    rewrite rng_mult_negate_l.
R: Ring
S: R -> Type
x, y: R
q: forall x : R, S x -> y * x = ring_zero
p: forall x0 : R, S x0 -> x * x0 = ring_zero
r: R
s: S r
ring_zero - y * r = ring_zero
    rewrite (q r s).
R: Ring
S: R -> Type
x, y: R
q: forall x : R, S x -> y * x = ring_zero
p: forall x0 : R, S x0 -> x * x0 = ring_zero
r: R
s: S r
ring_zero - ring_zero = ring_zero
    rewrite <- rng_mult_negate.
R: Ring
S: R -> Type
x, y: R
q: forall x : R, S x -> y * x = ring_zero
p: forall x0 : R, S x0 -> x * x0 = ring_zero
r: R
s: S r
ring_zero + -1 * ring_zero = ring_zero
    rewrite rng_mult_zero_r.
R: Ring
S: R -> Type
x, y: R
q: forall x : R, S x -> y * x = ring_zero
p: forall x0 : R, S x0 -> x * x0 = ring_zero
r: R
s: S r
ring_zero + 0 = ring_zero
    apply left_identity.
Defined.

(** The left annihilator of a subgroup of a ring is a left ideal of the ring. *)
Instance isleftideal_ideal_left_annihilator {R : Ring} (I : R -> Type)
  : IsLeftIdeal (subgroup_ideal_left_annihilator I).
R: Ring
I: R -> Type
IsLeftIdeal (subgroup_ideal_left_annihilator I)
Proof.
R: Ring
I: R -> Type
IsLeftIdeal (subgroup_ideal_left_annihilator I)
  intros r x p.
R: Ring
I: R -> Type
r, x: R
p: subgroup_ideal_left_annihilator I x
subgroup_ideal_left_annihilator I (r * x)
  strip_truncations; apply tr.
R: Ring
I: R -> Type
r, x: R
p: forall x0 : R, I x0 -> x * x0 = ring_zero
forall x0 : R, I x0 -> r * x * x0 = ring_zero
  intros s i.
R: Ring
I: R -> Type
r, x: R
p: forall x0 : R, I x0 -> x * x0 = ring_zero
s: R
i: I s
r * x * s = ring_zero
  rewrite <- rng_mult_assoc, (p s i).
R: Ring
I: R -> Type
r, x: R
p: forall x0 : R, I x0 -> x * x0 = ring_zero
s: R
i: I s
r * ring_zero = ring_zero
  apply rng_mult_zero_r.
Defined.

(** The left annihilator of a left ideal also happens to be a right ideal. In fact, left ideal could be weakened to subset closed under multiplication, however we don't need this generality currently. *)
Instance isrightideal_ideal_left_annihilator {R : Ring} (I : Subgroup R)
  `{IsLeftIdeal R I}
  : IsRightIdeal (subgroup_ideal_left_annihilator I).
R: Ring
I: Subgroup R
H: IsLeftIdeal I
IsRightIdeal (subgroup_ideal_left_annihilator I)
Proof.
R: Ring
I: Subgroup R
H: IsLeftIdeal I
IsRightIdeal (subgroup_ideal_left_annihilator I)
  intros r x p.
R: Ring
I: Subgroup R
H: IsLeftIdeal I
r, x: rng_op R
p: subgroup_ideal_left_annihilator I x
subgroup_ideal_left_annihilator I (r * x)
  strip_truncations; apply tr.
R: Ring
I: Subgroup R
H: IsLeftIdeal I
r, x: rng_op R
p: forall x0 : R, I x0 -> x * x0 = ring_zero
forall x0 : R, I x0 -> r * x * x0 = ring_zero
  intros s i; cbn.
R: Ring
I: Subgroup R
H: IsLeftIdeal I
r, x: rng_op R
p: forall x0 : R, I x0 -> x * x0 = ring_zero
s: R
i: I s
ring_mult x r * s = ring_zero
  rewrite <- rng_mult_assoc.
R: Ring
I: Subgroup R
H: IsLeftIdeal I
r, x: rng_op R
p: forall x0 : R, I x0 -> x * x0 = ring_zero
s: R
i: I s
x * (r * s) = ring_zero
  by apply p, isleftideal.
Defined.

(** Therefore the annihilator of a left ideal is an ideal. *)
Instance isideal_ideal_left_annihilator {R : Ring} (I : Subgroup R)
  `{IsLeftIdeal R I}
  : IsIdeal (subgroup_ideal_left_annihilator I)
  := {}.

(** The left annihilator of a left ideal. *)
Definition ideal_left_annihilator {R : Ring} (I : LeftIdeal R) : Ideal R
  := Build_Ideal R (subgroup_ideal_left_annihilator I) _.

(** The right annihilator of a subset of a ring is the set of elements that annihilate the elements of the subset with right multiplication. *)
Definition subgroup_ideal_right_annihilator {R : Ring} (I : R -> Type)
  : Subgroup R
  := subgroup_ideal_left_annihilator (R:=rng_op R) I.

(** When the subset is a right ideal the right annihilator is a left ideal of the ring. This can be strengthened. See the comment in the left ideal version of this lemma above. *)
Instance isleftideal_ideal_right_annihilator {R : Ring} (I : Subgroup R)
  `{IsRightIdeal R I}
  : IsLeftIdeal (subgroup_ideal_right_annihilator I)
  := isrightideal_ideal_left_annihilator (R:=rng_op R) I.

(** The right annihilator is a right ideal of the ring. *)
Instance isrightideal_ideal_right_annihilator {R : Ring} (I : R -> Type)
  : IsRightIdeal (subgroup_ideal_right_annihilator (R:=R) I)
  := isleftideal_ideal_left_annihilator (R:=rng_op R) I.

(** Therefore the annihilator of a right ideal is an ideal. *)
Instance isideal_ideal_right_annihilator {R : Ring} (I : Subgroup R)
  `{IsRightIdeal R I}
  : IsIdeal (subgroup_ideal_right_annihilator (R:=R) I)
  := {}.

(** The right annihilator of a right ideal. *)
Definition ideal_right_annihilator {R : Ring} (I : RightIdeal R) : Ideal R
  := Build_Ideal R (subgroup_ideal_right_annihilator (R:=R) I)
     (isideal_ideal_right_annihilator (R:=R) I).

(** The annihilator of an ideal is the intersection of the left and right annihilators. *)
Definition ideal_annihilator {R : Ring} (I : Ideal R) : Ideal R
  := ideal_intersection (ideal_left_annihilator I) (ideal_right_annihilator I).

(** ** Properties of ideals *)

(** *** Coprime ideals *)

(** Two ideals are coprime if their sum is the unit ideal. *)
Definition Coprime {R : Ring} (I J : Ideal R) : Type
  := ideal_eq (ideal_sum I J) (ideal_unit R).
Existing Class Coprime.

Instance ishprop_coprime `{Funext} {R : Ring}
  (I J : Ideal R) : IsHProp (Coprime I J).
H: Funext
R: Ring
I, J: Ideal R
IsHProp (Coprime I J)
Proof.
H: Funext
R: Ring
I, J: Ideal R
IsHProp (Coprime I J)
    unfold Coprime.
H: Funext
R: Ring
I, J: Ideal R
IsHProp (ideal_eq (ideal_sum I J) (ideal_unit R))
    exact _.
Defined.

Lemma equiv_coprime_sum `{Funext} {R : Ring} (I J : Ideal R)
  : Coprime I J
  <~> hexists (fun '(((i ; p) , (j ; q)) : sig I * sig J)
      => i + j = ring_one).
H: Funext
R: Ring
I, J: Ideal R
Coprime I J <~>
hexists
  (fun pat : {x : _ & I x} * {x : _ & J x} =>
   let x := pat in
   let fst := fst x in
   let snd := snd x in
   let fst0 := fst in
   let i := fst0.1 in
   let p := fst0.2 in
   let snd0 := snd in
   let j := snd0.1 in
   let q := snd0.2 in i + j = ring_one)
Proof.
H: Funext
R: Ring
I, J: Ideal R
Coprime I J <~>
hexists
  (fun pat : {x : _ & I x} * {x : _ & J x} =>
   let x := pat in
   let fst := fst x in
   let snd := snd x in
   let fst0 := fst in
   let i := fst0.1 in
   let p := fst0.2 in
   let snd0 := snd in
   let j := snd0.1 in
   let q := snd0.2 in i + j = ring_one)
  simpl.
H: Funext
R: Ring
I, J: Ideal R
Coprime I J <~>
Tr (-1)
  {pat : {x : _ & I x} * {x : _ & J x} &
  (fst pat).1 + (snd pat).1 = ring_one}
  srapply equiv_iff_hprop.
H: Funext
R: Ring
I, J: Ideal R
Coprime I J ->
Tr (-1)
  {pat : {x : _ & I x} * {x : _ & J x} &
  (fst pat).1 + (snd pat).1 = ring_one}
H: Funext
R: Ring
I, J: Ideal R
Tr (-1)
  {pat : {x : _ & I x} * {x : _ & J x} &
  (fst pat).1 + (snd pat).1 = ring_one} -> Coprime I J
  -
H: Funext
R: Ring
I, J: Ideal R
Coprime I J ->
Tr (-1)
  {pat : {x : _ & I x} * {x : _ & J x} &
  (fst pat).1 + (snd pat).1 = ring_one} intros c.
H: Funext
R: Ring
I, J: Ideal R
c: Coprime I J
Tr (-1)
  {pat : {x : _ & I x} * {x : _ & J x} &
  (fst pat).1 + (snd pat).1 = ring_one}
    pose (snd (c ring_one) tt) as d; clearbody d; clear c.
H: Funext
R: Ring
I, J: Ideal R
d: ideal_sum I J ring_one
Tr (-1)
  {pat : {x : _ & I x} * {x : _ & J x} &
  (fst pat).1 + (snd pat).1 = ring_one}
    strip_truncations.
H: Funext
R: Ring
I, J: Ideal R
d: subgroup_generated_type
  (fun x : R => (I x + J x)%type) ring_one
Tr (-1)
  {pat : {x : _ & I x} * {x : _ & J x} &
  (fst pat).1 + (snd pat).1 = ring_one}
    apply tr.
H: Funext
R: Ring
I, J: Ideal R
d: subgroup_generated_type
  (fun x : R => (I x + J x)%type) ring_one
{pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = ring_one}
    induction d.
H: Funext
R: Ring
I, J: Ideal R
g: R
x: (I g + J g)%type
{pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = g}
H: Funext
R: Ring
I, J: Ideal R
{pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = mon_unit}
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
IHd1: {pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = g}
IHd2: {pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = h}
{pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = sg_op g (inv h)}
    +
H: Funext
R: Ring
I, J: Ideal R
g: R
x: (I g + J g)%type
{pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = g} destruct x.
H: Funext
R: Ring
I, J: Ideal R
g: R
s: I g
{pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = g}
H: Funext
R: Ring
I, J: Ideal R
g: R
s: J g
{pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = g}
      *
H: Funext
R: Ring
I, J: Ideal R
g: R
s: I g
{pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = g} exists ((g ; s), (ring_zero; ideal_in_zero _)).
H: Funext
R: Ring
I, J: Ideal R
g: R
s: I g
g + ring_zero = g
        apply rng_plus_zero_r.
      *
H: Funext
R: Ring
I, J: Ideal R
g: R
s: J g
{pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = g} exists ((ring_zero; ideal_in_zero _), (g ; s)).
H: Funext
R: Ring
I, J: Ideal R
g: R
s: J g
ring_zero + g = g
        apply rng_plus_zero_l.
    +
H: Funext
R: Ring
I, J: Ideal R
{pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = mon_unit} exists ((ring_zero; ideal_in_zero _), (ring_zero; ideal_in_zero _)).
H: Funext
R: Ring
I, J: Ideal R
ring_zero + ring_zero = mon_unit
      apply rng_plus_zero_l.
    +
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
IHd1: {pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = g}
IHd2: {pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = h}
{pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = sg_op g (inv h)} destruct IHd1 as [[[x xi] [y yj]] p].
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
IHd2: {pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = h}
{pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = sg_op g (inv h)}
      destruct IHd2 as [[[w wi] [z zj]] q].
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
{pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = sg_op g (inv h)}
      srefine (((_;_),(_;_));_).
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
R
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
I ?proj1
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
R
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
J ?proj10
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
(fun pat : {x : _ & I x} * {x : _ & J x} =>
 (fst pat).1 + (snd pat).1 = sg_op g (inv h))
  ((?proj1; ?proj2), (?proj10; ?proj20))
      *
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
R exact (x - w).
      *
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
I (x - w) by apply ideal_in_plus_negate.
      *
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
R exact (y - z).
      *
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
J (y - z) by apply ideal_in_plus_negate.
      *
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
(fun pat : {x : _ & I x} * {x : _ & J x} =>
 (fst pat).1 + (snd pat).1 = sg_op g (inv h))
  ((x - w; ideal_in_plus_negate I x w xi wi),
  (y - z; ideal_in_plus_negate J y z yj zj)) cbn.
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
x - w + (y - z) = sg_op g (inv h)
        rhs_V exact (ap011 (fun x y => x - y) p q).
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
x - w + (y - z) = x + y - (w + z)
        lhs_V napply rng_plus_assoc.
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
x + (- w + (y - z)) = x + y - (w + z)
        rhs_V napply rng_plus_assoc.
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
x + (- w + (y - z)) = x + (y - (w + z))
        f_ap.
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
- w + (y - z) = y - (w + z)
        rewrite rng_negate_plus.
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
- w + (y - z) = y + (- w - z)
        rhs_V napply rng_plus_comm.
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
- w + (y - z) = - w - z + y
        rhs_V napply rng_plus_assoc.
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
- w + (y - z) = - w + (- z + y)
        f_ap.
H: Funext
R: Ring
I, J: Ideal R
g, h: R
d1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) g
d2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) h
x: R
xi: I x
y: R
yj: J y
p: x + y = g
w: R
wi: I w
z: R
zj: J z
q: w + z = h
y - z = - z + y
        apply commutativity.
  -
H: Funext
R: Ring
I, J: Ideal R
Tr (-1)
  {pat : {x : _ & I x} * {x : _ & J x} &
  (fst pat).1 + (snd pat).1 = ring_one} -> Coprime I J intro x.
H: Funext
R: Ring
I, J: Ideal R
x: Tr (-1)
  {pat : {x : _ & I x} * {x : _ & J x} &
  (fst pat).1 + (snd pat).1 = ring_one}
Coprime I J
    strip_truncations.
H: Funext
R: Ring
I, J: Ideal R
x: {pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = ring_one}
Coprime I J
    intros r.
H: Funext
R: Ring
I, J: Ideal R
x: {pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = ring_one}
r: R
ideal_sum I J r <-> ideal_unit R r
    split;[intro; exact tt|].
H: Funext
R: Ring
I, J: Ideal R
x: {pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = ring_one}
r: R
ideal_unit R r -> ideal_sum I J r
    intros _.
H: Funext
R: Ring
I, J: Ideal R
x: {pat : {x : _ & I x} * {x : _ & J x} &
(fst pat).1 + (snd pat).1 = ring_one}
r: R
ideal_sum I J r
    destruct x as [[[x xi] [y yj]] p].
H: Funext
R: Ring
I, J: Ideal R
x: R
xi: I x
y: R
yj: J y
p: x + y = ring_one
r: R
ideal_sum I J r
    rewrite <- rng_mult_one_r.
H: Funext
R: Ring
I, J: Ideal R
x: R
xi: I x
y: R
yj: J y
p: x + y = ring_one
r: R
ideal_sum I J (r * 1)
    change (x + y = 1) in p.
H: Funext
R: Ring
I, J: Ideal R
x: R
xi: I x
y: R
yj: J y
p: x + y = 1
r: R
ideal_sum I J (r * 1)
    rewrite <- p.
H: Funext
R: Ring
I, J: Ideal R
x: R
xi: I x
y: R
yj: J y
p: x + y = 1
r: R
ideal_sum I J (r * (x + y))
    rewrite rng_dist_l.
H: Funext
R: Ring
I, J: Ideal R
x: R
xi: I x
y: R
yj: J y
p: x + y = 1
r: R
ideal_sum I J (r * x + r * y)
    apply tr.
H: Funext
R: Ring
I, J: Ideal R
x: R
xi: I x
y: R
yj: J y
p: x + y = 1
r: R
subgroup_generated_type
  (fun x : R => (I x + J x)%type) (r * x + r * y)
    rapply sgt_op'.
H: Funext
R: Ring
I, J: Ideal R
x: R
xi: I x
y: R
yj: J y
p: x + y = 1
r: R
subgroup_generated_type
  (fun x : R => (I x + J x)%type) (r * x)
H: Funext
R: Ring
I, J: Ideal R
x: R
xi: I x
y: R
yj: J y
p: x + y = 1
r: R
subgroup_generated_type
  (fun x : R => (I x + J x)%type) (r * y)
    +
H: Funext
R: Ring
I, J: Ideal R
x: R
xi: I x
y: R
yj: J y
p: x + y = 1
r: R
subgroup_generated_type
  (fun x : R => (I x + J x)%type) (r * x) apply sgt_in.
H: Funext
R: Ring
I, J: Ideal R
x: R
xi: I x
y: R
yj: J y
p: x + y = 1
r: R
(I (mult r x) + J (mult r x))%type
      left.
H: Funext
R: Ring
I, J: Ideal R
x: R
xi: I x
y: R
yj: J y
p: x + y = 1
r: R
I (r * x)
      by apply isleftideal.
    +
H: Funext
R: Ring
I, J: Ideal R
x: R
xi: I x
y: R
yj: J y
p: x + y = 1
r: R
subgroup_generated_type
  (fun x : R => (I x + J x)%type) (r * y) apply sgt_in.
H: Funext
R: Ring
I, J: Ideal R
x: R
xi: I x
y: R
yj: J y
p: x + y = 1
r: R
(I (mult r y) + J (mult r y))%type
      right.
H: Funext
R: Ring
I, J: Ideal R
x: R
xi: I x
y: R
yj: J y
p: x + y = 1
r: R
J (r * y)
      by apply isleftideal.
Defined.

(** *** Ideal notations *)

(** We declare and import a module for various (Unicode) ideal notations. These exist in their own special case, and can be imported and used in other files when needing to reason about ideals. *)

Module Import Notation.
  Infix "⊆" := ideal_subset       : ideal_scope.
  Infix "↔" := ideal_eq           : ideal_scope.
  Infix "+" := ideal_sum          : ideal_scope.
  Infix "⋅" := ideal_product      : ideal_scope.
  Infix "∩" := ideal_intersection : ideal_scope.
  Infix "::" := ideal_quotient    : ideal_scope.
  Notation "〈 X 〉" := (ideal_generated X)  : ideal_scope.
  Notation Ann := ideal_annihilator.
End Notation.

(** *** Ideal lemmas *)

Section IdealLemmas.

  Context {R : Ring}.

  (** Subset relation is antisymmetric. *)
  Lemma ideal_subset_antisymm (I J : Subgroup R) : I ⊆ J -> J ⊆ I -> I ↔ J.
R: Ring
I, J: Subgroup R
I ⊆ J -> J ⊆ I -> I ↔ J
  Proof.
R: Ring
I, J: Subgroup R
I ⊆ J -> J ⊆ I -> I ↔ J
    intros p q x; split; by revert x.
  Defined.

  (** The zero ideal is contained in all ideals. *)
  Lemma ideal_zero_subset (I : Subgroup R) : ideal_zero R ⊆ I.
R: Ring
I: Subgroup R
ideal_zero R ⊆ I
  Proof.
R: Ring
I: Subgroup R
ideal_zero R ⊆ I
    intros x p; rewrite p; apply ideal_in_zero.
  Defined.

  (** The unit ideal contains all ideals. *)
  Lemma ideal_unit_subset (I : Subgroup R) : I ⊆ ideal_unit R.
R: Ring
I: Subgroup R
I ⊆ ideal_unit R
  Proof.
R: Ring
I: Subgroup R
I ⊆ ideal_unit R
    hnf; cbn; trivial.
  Defined.

  (** Intersection includes into the left *)
  Lemma ideal_intersection_subset_l (I J : Ideal R) : I ∩ J ⊆ I.
R: Ring
I, J: Ideal R
I ∩ J ⊆ I
  Proof.
R: Ring
I, J: Ideal R
I ∩ J ⊆ I
    intro; exact fst.
  Defined.

  (** Intersection includes into the right *)
  Lemma ideal_intersection_subset_r (I J : Ideal R) : I ∩ J ⊆ J.
R: Ring
I, J: Ideal R
I ∩ J ⊆ J
  Proof.
R: Ring
I, J: Ideal R
I ∩ J ⊆ J
    intro; exact snd.
  Defined.

  (** Subsets of intersections *)
  Lemma ideal_intersection_subset (I J K : Ideal R)
    : K ⊆ I -> K ⊆ J -> K ⊆ I ∩ J.
R: Ring
I, J, K: Ideal R
K ⊆ I -> K ⊆ J -> K ⊆ I ∩ J
  Proof.
R: Ring
I, J, K: Ideal R
K ⊆ I -> K ⊆ J -> K ⊆ I ∩ J
    intros p q x r; specialize (p x r); specialize (q x r); by split.
  Defined.

  (** Ideals include into their sum on the left *)
  Lemma ideal_sum_subset_l (I J : Ideal R) : I ⊆ (I + J).
R: Ring
I, J: Ideal R
I ⊆ (I + J)
  Proof.
R: Ring
I, J: Ideal R
I ⊆ (I + J)
    intros x p.
R: Ring
I, J: Ideal R
x: R
p: I x
(I + J) x
    apply tr, sgt_in.
R: Ring
I, J: Ideal R
x: R
p: I x
(I x + J x)%type
    left; exact p.
  Defined.

  (** Ideals include into their sum on the right *)
  Lemma ideal_sum_subset_r (I J : Ideal R) : J ⊆ (I + J).
R: Ring
I, J: Ideal R
J ⊆ (I + J)
  Proof.
R: Ring
I, J: Ideal R
J ⊆ (I + J)
    intros x p.
R: Ring
I, J: Ideal R
x: R
p: J x
(I + J) x
    apply tr, sgt_in.
R: Ring
I, J: Ideal R
x: R
p: J x
(I x + J x)%type
    right; exact p.
  Defined.

  #[local] Hint Extern 4 => progress (cbv beta iota) : typeclass_instances.

  (** Products of ideals are included in their left factor *)
  Lemma ideal_product_subset_l (I J : Ideal R) : I ⋅ J ⊆ I.
R: Ring
I, J: Ideal R
I ⋅ J ⊆ I
  Proof.
R: Ring
I, J: Ideal R
I ⋅ J ⊆ I
    intros r p.
R: Ring
I, J: Ideal R
r: R
p: (I ⋅ J) r
I r
    strip_truncations.
R: Ring
I, J: Ideal R
r: R
p: subgroup_generated_type
  (ideal_product_naive_type I J) r
I r
    induction p as [r i | | r s p1 IHp1 p2 IHp2 ].
R: Ring
I, J: Ideal R
r: R
i: ideal_product_naive_type I J r
I r
R: Ring
I, J: Ideal R
I mon_unit
R: Ring
I, J: Ideal R
r, s: R
p1: subgroup_generated_type
  (ideal_product_naive_type I J) r
p2: subgroup_generated_type
  (ideal_product_naive_type I J) s
IHp1: I r
IHp2: I s
I (sg_op r (inv s))
    +
R: Ring
I, J: Ideal R
r: R
i: ideal_product_naive_type I J r
I r destruct i as [s t].
R: Ring
I, J: Ideal R
s, t: R
s0: I s
s1: J t
I (s * t)
      by rapply isrightideal.
    +
R: Ring
I, J: Ideal R
I mon_unit rapply ideal_in_zero.
    +
R: Ring
I, J: Ideal R
r, s: R
p1: subgroup_generated_type
  (ideal_product_naive_type I J) r
p2: subgroup_generated_type
  (ideal_product_naive_type I J) s
IHp1: I r
IHp2: I s
I (sg_op r (inv s)) by rapply ideal_in_plus_negate.
  Defined.

  (** Products of ideals are included in their right factor. *)
  Lemma ideal_product_subset_r (I J : Ideal R) : I ⋅ J ⊆ J.
R: Ring
I, J: Ideal R
I ⋅ J ⊆ J
  Proof.
R: Ring
I, J: Ideal R
I ⋅ J ⊆ J
    intros r p.
R: Ring
I, J: Ideal R
r: R
p: (I ⋅ J) r
J r
    strip_truncations.
R: Ring
I, J: Ideal R
r: R
p: subgroup_generated_type
  (ideal_product_naive_type I J) r
J r
    induction p as [r i | | r s p1 IHp1 p2 IHp2 ].
R: Ring
I, J: Ideal R
r: R
i: ideal_product_naive_type I J r
J r
R: Ring
I, J: Ideal R
J mon_unit
R: Ring
I, J: Ideal R
r, s: R
p1: subgroup_generated_type
  (ideal_product_naive_type I J) r
p2: subgroup_generated_type
  (ideal_product_naive_type I J) s
IHp1: J r
IHp2: J s
J (sg_op r (inv s))
    +
R: Ring
I, J: Ideal R
r: R
i: ideal_product_naive_type I J r
J r destruct i as [s t].
R: Ring
I, J: Ideal R
s, t: R
s0: I s
s1: J t
J (s * t)
      by apply isleftideal.
    +
R: Ring
I, J: Ideal R
J mon_unit rapply ideal_in_zero.
    +
R: Ring
I, J: Ideal R
r, s: R
p1: subgroup_generated_type
  (ideal_product_naive_type I J) r
p2: subgroup_generated_type
  (ideal_product_naive_type I J) s
IHp1: J r
IHp2: J s
J (sg_op r (inv s)) by rapply ideal_in_plus_negate.
  Defined.

  (** Products of ideals preserve subsets on the left *)
  Lemma ideal_product_subset_pres_l (I J K : Ideal R) : I ⊆ J -> I ⋅ K ⊆ J ⋅ K.
R: Ring
I, J, K: Ideal R
I ⊆ J -> I ⋅ K ⊆ J ⋅ K
  Proof.
R: Ring
I, J, K: Ideal R
I ⊆ J -> I ⋅ K ⊆ J ⋅ K
    intros p r q.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
r: R
q: (I ⋅ K) r
(J ⋅ K) r
    strip_truncations.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
r: R
q: subgroup_generated_type
  (ideal_product_naive_type I K) r
(J ⋅ K) r
    induction q as [r i | | r s ].
R: Ring
I, J, K: Ideal R
p: I ⊆ J
r: R
i: ideal_product_naive_type I K r
(J ⋅ K) r
R: Ring
I, J, K: Ideal R
p: I ⊆ J
(J ⋅ K) mon_unit
R: Ring
I, J, K: Ideal R
p: I ⊆ J
r, s: R
q1: subgroup_generated_type
  (ideal_product_naive_type I K) r
q2: subgroup_generated_type
  (ideal_product_naive_type I K) s
IHq1: (J ⋅ K) r
IHq2: (J ⋅ K) s
(J ⋅ K) (sg_op r (inv s))
    +
R: Ring
I, J, K: Ideal R
p: I ⊆ J
r: R
i: ideal_product_naive_type I K r
(J ⋅ K) r destruct i.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
x, y: R
s: I x
s0: K y
(J ⋅ K) (x * y)
      apply tr, sgt_in, ipn_in.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
x, y: R
s: I x
s0: K y
J x
R: Ring
I, J, K: Ideal R
p: I ⊆ J
x, y: R
s: I x
s0: K y
K y
      1: apply p.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
x, y: R
s: I x
s0: K y
I x
R: Ring
I, J, K: Ideal R
p: I ⊆ J
x, y: R
s: I x
s0: K y
K y
      1,2: assumption.
    +
R: Ring
I, J, K: Ideal R
p: I ⊆ J
(J ⋅ K) mon_unit apply ideal_in_zero.
    +
R: Ring
I, J, K: Ideal R
p: I ⊆ J
r, s: R
q1: subgroup_generated_type
  (ideal_product_naive_type I K) r
q2: subgroup_generated_type
  (ideal_product_naive_type I K) s
IHq1: (J ⋅ K) r
IHq2: (J ⋅ K) s
(J ⋅ K) (sg_op r (inv s)) by apply ideal_in_plus_negate.
  Defined.

  (** Products of ideals preserve subsets on the right *)
  Lemma ideal_product_subset_pres_r (I J K : Ideal R) : I ⊆ J -> K ⋅ I ⊆ K ⋅ J.
R: Ring
I, J, K: Ideal R
I ⊆ J -> K ⋅ I ⊆ K ⋅ J
  Proof.
R: Ring
I, J, K: Ideal R
I ⊆ J -> K ⋅ I ⊆ K ⋅ J
    intros p r q.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
r: R
q: (K ⋅ I) r
(K ⋅ J) r
    strip_truncations.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
r: R
q: subgroup_generated_type
  (ideal_product_naive_type K I) r
(K ⋅ J) r
    induction q as [r i | | r s ].
R: Ring
I, J, K: Ideal R
p: I ⊆ J
r: R
i: ideal_product_naive_type K I r
(K ⋅ J) r
R: Ring
I, J, K: Ideal R
p: I ⊆ J
(K ⋅ J) mon_unit
R: Ring
I, J, K: Ideal R
p: I ⊆ J
r, s: R
q1: subgroup_generated_type
  (ideal_product_naive_type K I) r
q2: subgroup_generated_type
  (ideal_product_naive_type K I) s
IHq1: (K ⋅ J) r
IHq2: (K ⋅ J) s
(K ⋅ J) (sg_op r (inv s))
    +
R: Ring
I, J, K: Ideal R
p: I ⊆ J
r: R
i: ideal_product_naive_type K I r
(K ⋅ J) r destruct i.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
x, y: R
s: K x
s0: I y
(K ⋅ J) (x * y)
      apply tr, sgt_in, ipn_in.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
x, y: R
s: K x
s0: I y
K x
R: Ring
I, J, K: Ideal R
p: I ⊆ J
x, y: R
s: K x
s0: I y
J y
      2: apply p.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
x, y: R
s: K x
s0: I y
K x
R: Ring
I, J, K: Ideal R
p: I ⊆ J
x, y: R
s: K x
s0: I y
I y
      1,2: assumption.
    +
R: Ring
I, J, K: Ideal R
p: I ⊆ J
(K ⋅ J) mon_unit apply ideal_in_zero.
    +
R: Ring
I, J, K: Ideal R
p: I ⊆ J
r, s: R
q1: subgroup_generated_type
  (ideal_product_naive_type K I) r
q2: subgroup_generated_type
  (ideal_product_naive_type K I) s
IHq1: (K ⋅ J) r
IHq2: (K ⋅ J) s
(K ⋅ J) (sg_op r (inv s)) by apply ideal_in_plus_negate.
  Defined.

  (** TODO: *)
  (** The product of ideals is an associative operation. *)
  (* Lemma ideal_product_assoc (I J K : Ideal R) : I ⋅ (J ⋅ K) ↔ (I ⋅ J) ⋅ K.
  Proof.
    intros r; split; exact Trunc_functor.
  Abort. *)

  (** Products of ideals are subsets of their intersection. *)
  Lemma ideal_product_subset_intersection (I J : Ideal R) : I ⋅ J ⊆ I ∩ J.
R: Ring
I, J: Ideal R
I ⋅ J ⊆ I ∩ J
  Proof.
R: Ring
I, J: Ideal R
I ⋅ J ⊆ I ∩ J
    apply ideal_intersection_subset.
R: Ring
I, J: Ideal R
I ⋅ J ⊆ I
R: Ring
I, J: Ideal R
I ⋅ J ⊆ J
    +
R: Ring
I, J: Ideal R
I ⋅ J ⊆ I apply ideal_product_subset_l.
    +
R: Ring
I, J: Ideal R
I ⋅ J ⊆ J apply ideal_product_subset_r.
  Defined.

  (** Sums of ideals are the smallest ideal containing the summands. *)
  Lemma ideal_sum_smallest (I J K : Ideal R) : I ⊆ K -> J ⊆ K -> (I + J) ⊆ K.
R: Ring
I, J, K: Ideal R
I ⊆ K -> J ⊆ K -> (I + J) ⊆ K
  Proof.
R: Ring
I, J, K: Ideal R
I ⊆ K -> J ⊆ K -> (I + J) ⊆ K
    intros p q.
R: Ring
I, J, K: Ideal R
p: I ⊆ K
q: J ⊆ K
(I + J) ⊆ K
    refine (ideal_sum_ind I J (fun x _ => K x) p q _ _).
R: Ring
I, J, K: Ideal R
p: I ⊆ K
q: J ⊆ K
K mon_unit
R: Ring
I, J, K: Ideal R
p: I ⊆ K
q: J ⊆ K
forall x y : R,
subgroup_generated_type
  (fun x0 : R => (I x0 + J x0)%type) x ->
subgroup_generated_type
  (fun x0 : R => (I x0 + J x0)%type) y ->
K x -> K y -> K (x - y)
    1: apply ideal_in_zero.
R: Ring
I, J, K: Ideal R
p: I ⊆ K
q: J ⊆ K
forall x y : R,
subgroup_generated_type
  (fun x0 : R => (I x0 + J x0)%type) x ->
subgroup_generated_type
  (fun x0 : R => (I x0 + J x0)%type) y ->
K x -> K y -> K (x - y)
    intros y z s t.
R: Ring
I, J, K: Ideal R
p: I ⊆ K
q: J ⊆ K
y, z: R
s: subgroup_generated_type
  (fun x : R => (I x + J x)%type) y
t: subgroup_generated_type
  (fun x : R => (I x + J x)%type) z
K y -> K z -> K (y - z)
    rapply ideal_in_plus_negate.
  Defined.

  (** Ideals absorb themselves under sum. *)
  Lemma ideal_sum_self (I : Ideal R) : I + I ↔ I.
R: Ring
I: Ideal R
I + I ↔ I
  Proof.
R: Ring
I: Ideal R
I + I ↔ I
    apply ideal_subset_antisymm.
R: Ring
I: Ideal R
(I + I) ⊆ I
R: Ring
I: Ideal R
I ⊆ (I + I)
    1: by rapply ideal_sum_smallest.
R: Ring
I: Ideal R
I ⊆ (I + I)
    rapply ideal_sum_subset_l.
  Defined.

  (** Sums preserve inclusions in the left summand. *)
  Lemma ideal_sum_subset_pres_l (I J K : Ideal R) : I ⊆ J -> (I + K) ⊆ (J + K).
R: Ring
I, J, K: Ideal R
I ⊆ J -> (I + K) ⊆ (J + K)
  Proof.
R: Ring
I, J, K: Ideal R
I ⊆ J -> (I + K) ⊆ (J + K)
    intros p.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
(I + K) ⊆ (J + K)
    apply ideal_sum_smallest.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
I ⊆ (J + K)
R: Ring
I, J, K: Ideal R
p: I ⊆ J
K ⊆ (J + K)
    {
R: Ring
I, J, K: Ideal R
p: I ⊆ J
I ⊆ (J + K) transitivity J.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
I ⊆ J
R: Ring
I, J, K: Ideal R
p: I ⊆ J
J ⊆ (J + K)
      1: exact p.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
J ⊆ (J + K)
      apply ideal_sum_subset_l. }
R: Ring
I, J, K: Ideal R
p: I ⊆ J
K ⊆ (J + K)
    apply ideal_sum_subset_r.
  Defined.

  (** Sums preserve inclusions in the right summand. *)
  Lemma ideal_sum_subset_pres_r (I J K : Ideal R) : I ⊆ J -> (K + I) ⊆ (K + J).
R: Ring
I, J, K: Ideal R
I ⊆ J -> (K + I) ⊆ (K + J)
  Proof.
R: Ring
I, J, K: Ideal R
I ⊆ J -> (K + I) ⊆ (K + J)
    intros p.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
(K + I) ⊆ (K + J)
    apply ideal_sum_smallest.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
K ⊆ (K + J)
R: Ring
I, J, K: Ideal R
p: I ⊆ J
I ⊆ (K + J)
    1: apply ideal_sum_subset_l.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
I ⊆ (K + J)
    transitivity J.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
I ⊆ J
R: Ring
I, J, K: Ideal R
p: I ⊆ J
J ⊆ (K + J)
    1: exact p.
R: Ring
I, J, K: Ideal R
p: I ⊆ J
J ⊆ (K + J)
    apply ideal_sum_subset_r.
  Defined.

  (** Products left distribute over sums *)
  (** Note that this follows from left adjoints preserving colimits. The product of ideals is a functor whose right adjoint is the quotient ideal. *)
  Lemma ideal_dist_l (I J K : Ideal R) : I ⋅ (J + K) ↔ I ⋅ J + I ⋅ K.
R: Ring
I, J, K: Ideal R
I ⋅ (J + K) ↔ I ⋅ J + I ⋅ K
  Proof.
R: Ring
I, J, K: Ideal R
I ⋅ (J + K) ↔ I ⋅ J + I ⋅ K
    (** We split into two directions. *)
    apply ideal_subset_antisymm.
R: Ring
I, J, K: Ideal R
I ⋅ (J + K) ⊆ (I ⋅ J + I ⋅ K)
R: Ring
I, J, K: Ideal R
(I ⋅ J + I ⋅ K) ⊆ I ⋅ (J + K)
    (** We deal with the difficult inclusion first. The proof comes down to breaking down the definition and reassembling into the right. *)
    {
R: Ring
I, J, K: Ideal R
I ⋅ (J + K) ⊆ (I ⋅ J + I ⋅ K) intros r p.
R: Ring
I, J, K: Ideal R
r: R
p: (I ⋅ (J + K)) r
(I ⋅ J + I ⋅ K) r
      strip_truncations.
R: Ring
I, J, K: Ideal R
r: R
p: subgroup_generated_type
  (ideal_product_naive_type I (J + K)) r
(I ⋅ J + I ⋅ K) r
      induction p as [ r i | | r s p1 IHp1 p2 IHp2].
R: Ring
I, J, K: Ideal R
r: R
i: ideal_product_naive_type I (J + K) r
(I ⋅ J + I ⋅ K) r
R: Ring
I, J, K: Ideal R
(I ⋅ J + I ⋅ K) mon_unit
R: Ring
I, J, K: Ideal R
r, s: R
p1: subgroup_generated_type
  (ideal_product_naive_type I (J + K)) r
p2: subgroup_generated_type
  (ideal_product_naive_type I (J + K)) s
IHp1: (I ⋅ J + I ⋅ K) r
IHp2: (I ⋅ J + I ⋅ K) s
(I ⋅ J + I ⋅ K) (sg_op r (inv s))
      -
R: Ring
I, J, K: Ideal R
r: R
i: ideal_product_naive_type I (J + K) r
(I ⋅ J + I ⋅ K) r destruct i as [r s p q].
R: Ring
I, J, K: Ideal R
r, s: R
p: I r
q: (J + K) s
(I ⋅ J + I ⋅ K) (r * s)
        strip_truncations.
R: Ring
I, J, K: Ideal R
r, s: R
p: I r
q: subgroup_generated_type
  (fun x : R => (J x + K x)%type) s
(I ⋅ J + I ⋅ K) (r * s)
        induction q as [ t k | | t k p1 IHp1 p2 IHp2 ].
R: Ring
I, J, K: Ideal R
r: R
p: I r
t: R
k: (J t + K t)%type
(I ⋅ J + I ⋅ K) (r * t)
R: Ring
I, J, K: Ideal R
r: R
p: I r
(I ⋅ J + I ⋅ K) (r * mon_unit)
R: Ring
I, J, K: Ideal R
r: R
p: I r
t, k: R
p1: subgroup_generated_type
  (fun x : R => (J x + K x)%type) t
p2: subgroup_generated_type
  (fun x : R => (J x + K x)%type) k
IHp1: (I ⋅ J + I ⋅ K) (r * t)
IHp2: (I ⋅ J + I ⋅ K) (r * k)
(I ⋅ J + I ⋅ K) (r * sg_op t (inv k))
        +
R: Ring
I, J, K: Ideal R
r: R
p: I r
t: R
k: (J t + K t)%type
(I ⋅ J + I ⋅ K) (r * t) apply tr, sgt_in.
R: Ring
I, J, K: Ideal R
r: R
p: I r
t: R
k: (J t + K t)%type
((I ⋅ J) (mult r t) + (I ⋅ K) (mult r t))%type
          destruct k as [j | k].
R: Ring
I, J, K: Ideal R
r: R
p: I r
t: R
j: J t
((I ⋅ J) (mult r t) + (I ⋅ K) (mult r t))%type
R: Ring
I, J, K: Ideal R
r: R
p: I r
t: R
k: K t
((I ⋅ J) (mult r t) + (I ⋅ K) (mult r t))%type
          *
R: Ring
I, J, K: Ideal R
r: R
p: I r
t: R
j: J t
((I ⋅ J) (mult r t) + (I ⋅ K) (mult r t))%type left; by apply tr, sgt_in, ipn_in.
          *
R: Ring
I, J, K: Ideal R
r: R
p: I r
t: R
k: K t
((I ⋅ J) (mult r t) + (I ⋅ K) (mult r t))%type right; by apply tr, sgt_in, ipn_in.
        +
R: Ring
I, J, K: Ideal R
r: R
p: I r
(I ⋅ J + I ⋅ K) (r * mon_unit) apply tr, sgt_in; left.
R: Ring
I, J, K: Ideal R
r: R
p: I r
(I ⋅ J) (r * mon_unit)
          rewrite rng_mult_zero_r.
R: Ring
I, J, K: Ideal R
r: R
p: I r
(I ⋅ J) 0
          apply ideal_in_zero.
        +
R: Ring
I, J, K: Ideal R
r: R
p: I r
t, k: R
p1: subgroup_generated_type
  (fun x : R => (J x + K x)%type) t
p2: subgroup_generated_type
  (fun x : R => (J x + K x)%type) k
IHp1: (I ⋅ J + I ⋅ K) (r * t)
IHp2: (I ⋅ J + I ⋅ K) (r * k)
(I ⋅ J + I ⋅ K) (r * sg_op t (inv k)) rewrite rng_dist_l.
R: Ring
I, J, K: Ideal R
r: R
p: I r
t, k: R
p1: subgroup_generated_type
  (fun x : R => (J x + K x)%type) t
p2: subgroup_generated_type
  (fun x : R => (J x + K x)%type) k
IHp1: (I ⋅ J + I ⋅ K) (r * t)
IHp2: (I ⋅ J + I ⋅ K) (r * k)
(I ⋅ J + I ⋅ K) (plus (r * t) (r * inv k))
          rewrite rng_mult_negate_r.
R: Ring
I, J, K: Ideal R
r: R
p: I r
t, k: R
p1: subgroup_generated_type
  (fun x : R => (J x + K x)%type) t
p2: subgroup_generated_type
  (fun x : R => (J x + K x)%type) k
IHp1: (I ⋅ J + I ⋅ K) (r * t)
IHp2: (I ⋅ J + I ⋅ K) (r * k)
(I ⋅ J + I ⋅ K) (r * t - r * k)
          by apply ideal_in_plus_negate.
      -
R: Ring
I, J, K: Ideal R
(I ⋅ J + I ⋅ K) mon_unit apply ideal_in_zero.
      -
R: Ring
I, J, K: Ideal R
r, s: R
p1: subgroup_generated_type
  (ideal_product_naive_type I (J + K)) r
p2: subgroup_generated_type
  (ideal_product_naive_type I (J + K)) s
IHp1: (I ⋅ J + I ⋅ K) r
IHp2: (I ⋅ J + I ⋅ K) s
(I ⋅ J + I ⋅ K) (sg_op r (inv s)) by apply ideal_in_plus_negate. }
R: Ring
I, J, K: Ideal R
(I ⋅ J + I ⋅ K) ⊆ I ⋅ (J + K)
    (** This is the easy direction which can use previous lemmas. *)
    apply ideal_sum_smallest.
R: Ring
I, J, K: Ideal R
I ⋅ J ⊆ I ⋅ (J + K)
R: Ring
I, J, K: Ideal R
I ⋅ K ⊆ I ⋅ (J + K)
    1,2: apply ideal_product_subset_pres_r.
R: Ring
I, J, K: Ideal R
J ⊆ (J + K)
R: Ring
I, J, K: Ideal R
K ⊆ (J + K)
    1: apply ideal_sum_subset_l.
R: Ring
I, J, K: Ideal R
K ⊆ (J + K)
    apply ideal_sum_subset_r.
  Defined.

  (** Products distribute over sums on the right. *)
  (** The proof is very similar to the left version *)
  Lemma ideal_dist_r (I J K : Ideal R) : (I + J) ⋅ K ↔ I ⋅ K + J ⋅ K.
R: Ring
I, J, K: Ideal R
(I + J) ⋅ K ↔ I ⋅ K + J ⋅ K
  Proof.
R: Ring
I, J, K: Ideal R
(I + J) ⋅ K ↔ I ⋅ K + J ⋅ K
    apply ideal_subset_antisymm.
R: Ring
I, J, K: Ideal R
(I + J) ⋅ K ⊆ (I ⋅ K + J ⋅ K)
R: Ring
I, J, K: Ideal R
(I ⋅ K + J ⋅ K) ⊆ (I + J) ⋅ K
    {
R: Ring
I, J, K: Ideal R
(I + J) ⋅ K ⊆ (I ⋅ K + J ⋅ K) intros r p.
R: Ring
I, J, K: Ideal R
r: R
p: ((I + J) ⋅ K) r
(I ⋅ K + J ⋅ K) r
      strip_truncations.
R: Ring
I, J, K: Ideal R
r: R
p: subgroup_generated_type
  (ideal_product_naive_type (I + J) K) r
(I ⋅ K + J ⋅ K) r
      induction p as [ r i | | r s p1 IHp1 p2 IHp2].
R: Ring
I, J, K: Ideal R
r: R
i: ideal_product_naive_type (I + J) K r
(I ⋅ K + J ⋅ K) r
R: Ring
I, J, K: Ideal R
(I ⋅ K + J ⋅ K) mon_unit
R: Ring
I, J, K: Ideal R
r, s: R
p1: subgroup_generated_type
  (ideal_product_naive_type (I + J) K) r
p2: subgroup_generated_type
  (ideal_product_naive_type (I + J) K) s
IHp1: (I ⋅ K + J ⋅ K) r
IHp2: (I ⋅ K + J ⋅ K) s
(I ⋅ K + J ⋅ K) (sg_op r (inv s))
      -
R: Ring
I, J, K: Ideal R
r: R
i: ideal_product_naive_type (I + J) K r
(I ⋅ K + J ⋅ K) r destruct i as [r s p q].
R: Ring
I, J, K: Ideal R
r, s: R
p: (I + J) r
q: K s
(I ⋅ K + J ⋅ K) (r * s)
        strip_truncations.
R: Ring
I, J, K: Ideal R
r, s: R
q: K s
p: subgroup_generated_type
  (fun x : R => (I x + J x)%type) r
(I ⋅ K + J ⋅ K) (r * s)
        induction p as [ t k | | t k p1 IHp1 p2 IHp2 ].
R: Ring
I, J, K: Ideal R
s: R
q: K s
t: R
k: (I t + J t)%type
(I ⋅ K + J ⋅ K) (t * s)
R: Ring
I, J, K: Ideal R
s: R
q: K s
(I ⋅ K + J ⋅ K) (mon_unit * s)
R: Ring
I, J, K: Ideal R
s: R
q: K s
t, k: R
p1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) t
p2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) k
IHp1: (I ⋅ K + J ⋅ K) (t * s)
IHp2: (I ⋅ K + J ⋅ K) (k * s)
(I ⋅ K + J ⋅ K) (sg_op t (inv k) * s)
        +
R: Ring
I, J, K: Ideal R
s: R
q: K s
t: R
k: (I t + J t)%type
(I ⋅ K + J ⋅ K) (t * s) apply tr, sgt_in.
R: Ring
I, J, K: Ideal R
s: R
q: K s
t: R
k: (I t + J t)%type
((I ⋅ K) (mult t s) + (J ⋅ K) (mult t s))%type
          destruct k as [j | k].
R: Ring
I, J, K: Ideal R
s: R
q: K s
t: R
j: I t
((I ⋅ K) (mult t s) + (J ⋅ K) (mult t s))%type
R: Ring
I, J, K: Ideal R
s: R
q: K s
t: R
k: J t
((I ⋅ K) (mult t s) + (J ⋅ K) (mult t s))%type
          *
R: Ring
I, J, K: Ideal R
s: R
q: K s
t: R
j: I t
((I ⋅ K) (mult t s) + (J ⋅ K) (mult t s))%type left; by apply tr, sgt_in, ipn_in.
          *
R: Ring
I, J, K: Ideal R
s: R
q: K s
t: R
k: J t
((I ⋅ K) (mult t s) + (J ⋅ K) (mult t s))%type right; by apply tr, sgt_in, ipn_in.
        +
R: Ring
I, J, K: Ideal R
s: R
q: K s
(I ⋅ K + J ⋅ K) (mon_unit * s) apply tr, sgt_in; left.
R: Ring
I, J, K: Ideal R
s: R
q: K s
(I ⋅ K) (mon_unit * s)
          rewrite rng_mult_zero_l.
R: Ring
I, J, K: Ideal R
s: R
q: K s
(I ⋅ K) 0
          apply ideal_in_zero.
        +
R: Ring
I, J, K: Ideal R
s: R
q: K s
t, k: R
p1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) t
p2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) k
IHp1: (I ⋅ K + J ⋅ K) (t * s)
IHp2: (I ⋅ K + J ⋅ K) (k * s)
(I ⋅ K + J ⋅ K) (sg_op t (inv k) * s) rewrite rng_dist_r.
R: Ring
I, J, K: Ideal R
s: R
q: K s
t, k: R
p1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) t
p2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) k
IHp1: (I ⋅ K + J ⋅ K) (t * s)
IHp2: (I ⋅ K + J ⋅ K) (k * s)
(I ⋅ K + J ⋅ K) (plus (t * s) (inv k * s))
          rewrite rng_mult_negate_l.
R: Ring
I, J, K: Ideal R
s: R
q: K s
t, k: R
p1: subgroup_generated_type
  (fun x : R => (I x + J x)%type) t
p2: subgroup_generated_type
  (fun x : R => (I x + J x)%type) k
IHp1: (I ⋅ K + J ⋅ K) (t * s)
IHp2: (I ⋅ K + J ⋅ K) (k * s)
(I ⋅ K + J ⋅ K) (t * s - k * s)
          by apply ideal_in_plus_negate.
      -
R: Ring
I, J, K: Ideal R
(I ⋅ K + J ⋅ K) mon_unit apply ideal_in_zero.
      -
R: Ring
I, J, K: Ideal R
r, s: R
p1: subgroup_generated_type
  (ideal_product_naive_type (I + J) K) r
p2: subgroup_generated_type
  (ideal_product_naive_type (I + J) K) s
IHp1: (I ⋅ K + J ⋅ K) r
IHp2: (I ⋅ K + J ⋅ K) s
(I ⋅ K + J ⋅ K) (sg_op r (inv s)) by apply ideal_in_plus_negate. }
R: Ring
I, J, K: Ideal R
(I ⋅ K + J ⋅ K) ⊆ (I + J) ⋅ K
    apply ideal_sum_smallest.
R: Ring
I, J, K: Ideal R
I ⋅ K ⊆ (I + J) ⋅ K
R: Ring
I, J, K: Ideal R
J ⋅ K ⊆ (I + J) ⋅ K
    1,2: apply ideal_product_subset_pres_l.
R: Ring
I, J, K: Ideal R
I ⊆ (I + J)
R: Ring
I, J, K: Ideal R
J ⊆ (I + J)
    1: apply ideal_sum_subset_l.
R: Ring
I, J, K: Ideal R
J ⊆ (I + J)
    apply ideal_sum_subset_r.
  Defined.

  (** Ideal sums are commutative *)
  Lemma ideal_sum_comm (I J : Ideal R) : I + J ↔ J + I.
R: Ring
I, J: Ideal R
I + J ↔ J + I
  Proof.
R: Ring
I, J: Ideal R
I + J ↔ J + I
    apply ideal_subset_antisymm; apply ideal_sum_smallest.
R: Ring
I, J: Ideal R
I ⊆ (J + I)
R: Ring
I, J: Ideal R
J ⊆ (J + I)
R: Ring
I, J: Ideal R
J ⊆ (I + J)
R: Ring
I, J: Ideal R
I ⊆ (I + J)
    1,3: apply ideal_sum_subset_r.
R: Ring
I, J: Ideal R
J ⊆ (J + I)
R: Ring
I, J: Ideal R
I ⊆ (I + J)
    1,2: apply ideal_sum_subset_l.
  Defined.

  (** Zero ideal is left additive identity. *) 
  Lemma ideal_sum_zero_l I : ideal_zero R + I ↔ I.
R: Ring
I: Ideal R
ideal_zero R + I ↔ I
  Proof.
R: Ring
I: Ideal R
ideal_zero R + I ↔ I
    apply ideal_subset_antisymm.
R: Ring
I: Ideal R
(ideal_zero R + I) ⊆ I
R: Ring
I: Ideal R
I ⊆ (ideal_zero R + I)
    1: apply ideal_sum_smallest.
R: Ring
I: Ideal R
ideal_zero R ⊆ I
R: Ring
I: Ideal R
I ⊆ I
R: Ring
I: Ideal R
I ⊆ (ideal_zero R + I)
    1: apply ideal_zero_subset.
R: Ring
I: Ideal R
I ⊆ I
R: Ring
I: Ideal R
I ⊆ (ideal_zero R + I)
    1: reflexivity.
R: Ring
I: Ideal R
I ⊆ (ideal_zero R + I)
    apply ideal_sum_subset_r.
  Defined.

  (** Zero ideal is right additive identity. *)
  Lemma ideal_sum_zero_r I : I + ideal_zero R ↔ I.
R: Ring
I: Ideal R
I + ideal_zero R ↔ I
  Proof.
R: Ring
I: Ideal R
I + ideal_zero R ↔ I
    apply ideal_subset_antisymm.
R: Ring
I: Ideal R
(I + ideal_zero R) ⊆ I
R: Ring
I: Ideal R
I ⊆ (I + ideal_zero R)
    1: apply ideal_sum_smallest.
R: Ring
I: Ideal R
I ⊆ I
R: Ring
I: Ideal R
ideal_zero R ⊆ I
R: Ring
I: Ideal R
I ⊆ (I + ideal_zero R)
    1: reflexivity.
R: Ring
I: Ideal R
ideal_zero R ⊆ I
R: Ring
I: Ideal R
I ⊆ (I + ideal_zero R)
    1: apply ideal_zero_subset.
R: Ring
I: Ideal R
I ⊆ (I + ideal_zero R)
    apply ideal_sum_subset_l.
  Defined.

  (** Unit ideal is left multiplicative identity. *)
  Lemma ideal_product_unit_l I : ideal_unit R ⋅ I ↔ I.
R: Ring
I: Ideal R
ideal_unit R ⋅ I ↔ I
  Proof.
R: Ring
I: Ideal R
ideal_unit R ⋅ I ↔ I
    apply ideal_subset_antisymm.
R: Ring
I: Ideal R
ideal_unit R ⋅ I ⊆ I
R: Ring
I: Ideal R
I ⊆ ideal_unit R ⋅ I
    1: apply ideal_product_subset_r.
R: Ring
I: Ideal R
I ⊆ ideal_unit R ⋅ I
    intros r p.
R: Ring
I: Ideal R
r: R
p: I r
(ideal_unit R ⋅ I) r
    rewrite <- rng_mult_one_l.
R: Ring
I: Ideal R
r: R
p: I r
(ideal_unit R ⋅ I) (1 * r)
    by apply tr, sgt_in, ipn_in.
  Defined.

  (** Unit ideal is right multiplicative identity. *)
  Lemma ideal_product_unit_r I : I ⋅ ideal_unit R ↔ I.
R: Ring
I: Ideal R
I ⋅ ideal_unit R ↔ I
  Proof.
R: Ring
I: Ideal R
I ⋅ ideal_unit R ↔ I
    apply ideal_subset_antisymm.
R: Ring
I: Ideal R
I ⋅ ideal_unit R ⊆ I
R: Ring
I: Ideal R
I ⊆ I ⋅ ideal_unit R
    1: apply ideal_product_subset_l.
R: Ring
I: Ideal R
I ⊆ I ⋅ ideal_unit R
    intros r p.
R: Ring
I: Ideal R
r: R
p: I r
(I ⋅ ideal_unit R) r
    rewrite <- rng_mult_one_r.
R: Ring
I: Ideal R
r: R
p: I r
(I ⋅ ideal_unit R) (r * 1)
    by apply tr, sgt_in, ipn_in.
  Defined.

  (** Intersecting with unit ideal on the left does nothing. *)
  Lemma ideal_intresection_unit_l I : ideal_unit R ∩ I ↔ I.
R: Ring
I: Ideal R
ideal_unit R ∩ I ↔ I
  Proof.
R: Ring
I: Ideal R
ideal_unit R ∩ I ↔ I
    apply ideal_subset_antisymm.
R: Ring
I: Ideal R
ideal_unit R ∩ I ⊆ I
R: Ring
I: Ideal R
I ⊆ ideal_unit R ∩ I
    1: apply ideal_intersection_subset_r.
R: Ring
I: Ideal R
I ⊆ ideal_unit R ∩ I
    apply ideal_intersection_subset.
R: Ring
I: Ideal R
I ⊆ ideal_unit R
R: Ring
I: Ideal R
I ⊆ I
    1: apply ideal_unit_subset.
R: Ring
I: Ideal R
I ⊆ I
    reflexivity.
  Defined.

  (** Intersecting with unit ideal on right does nothing. *)
  Lemma ideal_intersection_unit_r I : I ∩ ideal_unit R ↔ I.
R: Ring
I: Ideal R
I ∩ ideal_unit R ↔ I
  Proof.
R: Ring
I: Ideal R
I ∩ ideal_unit R ↔ I
    apply ideal_subset_antisymm.
R: Ring
I: Ideal R
I ∩ ideal_unit R ⊆ I
R: Ring
I: Ideal R
I ⊆ I ∩ ideal_unit R
    1: apply ideal_intersection_subset_l.
R: Ring
I: Ideal R
I ⊆ I ∩ ideal_unit R
    apply ideal_intersection_subset.
R: Ring
I: Ideal R
I ⊆ I
R: Ring
I: Ideal R
I ⊆ ideal_unit R
    1: reflexivity.
R: Ring
I: Ideal R
I ⊆ ideal_unit R
    apply ideal_unit_subset.
  Defined.

  (** Product of intersection and sum is subset of sum of products *)
  Lemma ideal_product_intersection_sum_subset (I J : Ideal R)
    : (I ∩ J) ⋅ (I + J) ⊆ (I ⋅ J + J ⋅ I).
R: Ring
I, J: Ideal R
(I ∩ J) ⋅ (I + J) ⊆ (I ⋅ J + J ⋅ I)
  Proof.
R: Ring
I, J: Ideal R
(I ∩ J) ⋅ (I + J) ⊆ (I ⋅ J + J ⋅ I)
    etransitivity.
R: Ring
I, J: Ideal R
(I ∩ J) ⋅ (I + J) ⊆ ?Goal
R: Ring
I, J: Ideal R
?Goal ⊆ (I ⋅ J + J ⋅ I)
    1: rapply ideal_dist_l.
R: Ring
I, J: Ideal R
((I ∩ J) ⋅ I + (I ∩ J) ⋅ J) ⊆ (I ⋅ J + J ⋅ I)
    etransitivity.
R: Ring
I, J: Ideal R
((I ∩ J) ⋅ I + (I ∩ J) ⋅ J) ⊆ ?Goal
R: Ring
I, J: Ideal R
?Goal ⊆ (I ⋅ J + J ⋅ I)
    1: rapply ideal_sum_subset_pres_r.
R: Ring
I, J: Ideal R
(I ∩ J) ⋅ J ⊆ ?Goal0
R: Ring
I, J: Ideal R
((I ∩ J) ⋅ I + ?Goal0) ⊆ (I ⋅ J + J ⋅ I)
    1: rapply ideal_product_subset_pres_l.
R: Ring
I, J: Ideal R
I ∩ J ⊆ ?Goal0
R: Ring
I, J: Ideal R
((I ∩ J) ⋅ I + ?Goal0 ⋅ J) ⊆ (I ⋅ J + J ⋅ I)
    1: apply ideal_intersection_subset_l.
R: Ring
I, J: Ideal R
((I ∩ J) ⋅ I + I ⋅ J) ⊆ (I ⋅ J + J ⋅ I)
    etransitivity.
R: Ring
I, J: Ideal R
((I ∩ J) ⋅ I + I ⋅ J) ⊆ ?Goal
R: Ring
I, J: Ideal R
?Goal ⊆ (I ⋅ J + J ⋅ I)
    1: rapply ideal_sum_subset_pres_l.
R: Ring
I, J: Ideal R
(I ∩ J) ⋅ I ⊆ ?Goal0
R: Ring
I, J: Ideal R
(?Goal0 + I ⋅ J) ⊆ (I ⋅ J + J ⋅ I)
    1: rapply ideal_product_subset_pres_l.
R: Ring
I, J: Ideal R
I ∩ J ⊆ ?Goal0
R: Ring
I, J: Ideal R
(?Goal0 ⋅ I + I ⋅ J) ⊆ (I ⋅ J + J ⋅ I)
    1: apply ideal_intersection_subset_r.
R: Ring
I, J: Ideal R
(J ⋅ I + I ⋅ J) ⊆ (I ⋅ J + J ⋅ I)
    rapply ideal_sum_comm.
  Defined.

  (** Ideals are subsets of their ideal quotients *)
  Lemma ideal_quotient_subset (I J : Ideal R) : I ⊆ (I :: J).
R: Ring
I, J: Ideal R
I ⊆ (I :: J)
  Proof.
R: Ring
I, J: Ideal R
I ⊆ (I :: J)
    intros x i; split; apply tr; intros r j; cbn.
R: Ring
I, J: Ideal R
x: R
i: I x
r: R
j: J r
I (x * r)
R: Ring
I, J: Ideal R
x: R
i: I x
r: rng_op R
j: J r
I (ring_mult r x)
    -
R: Ring
I, J: Ideal R
x: R
i: I x
r: R
j: J r
I (x * r) by rapply isrightideal.
    -
R: Ring
I, J: Ideal R
x: R
i: I x
r: rng_op R
j: J r
I (ring_mult r x) by rapply isleftideal.
  Defined.

  (** If J divides I then the ideal quotient of J by I is trivial. *)
  Lemma ideal_quotient_trivial (I J : Ideal R)
    : I ⊆ J -> J :: I ↔ ideal_unit R.
R: Ring
I, J: Ideal R
I ⊆ J -> J :: I ↔ ideal_unit R
  Proof.
R: Ring
I, J: Ideal R
I ⊆ J -> J :: I ↔ ideal_unit R
    intros p.
R: Ring
I, J: Ideal R
p: I ⊆ J
J :: I ↔ ideal_unit R
    apply ideal_subset_antisymm.
R: Ring
I, J: Ideal R
p: I ⊆ J
(J :: I) ⊆ ideal_unit R
R: Ring
I, J: Ideal R
p: I ⊆ J
ideal_unit R ⊆ (J :: I)
    1: cbv; trivial.
R: Ring
I, J: Ideal R
p: I ⊆ J
ideal_unit R ⊆ (J :: I)
    intros r _; split; apply tr; intros x q; cbn.
R: Ring
I, J: Ideal R
p: I ⊆ J
r, x: R
q: I x
J (r * x)
R: Ring
I, J: Ideal R
p: I ⊆ J
r: R
x: rng_op R
q: I x
J (ring_mult x r)
    -
R: Ring
I, J: Ideal R
p: I ⊆ J
r, x: R
q: I x
J (r * x) by apply isleftideal, p. 
    -
R: Ring
I, J: Ideal R
p: I ⊆ J
r: R
x: rng_op R
q: I x
J (ring_mult x r) rapply isrightideal.
R: Ring
I, J: Ideal R
p: I ⊆ J
r: R
x: rng_op R
q: I x
J x
      by apply p.
  Defined.

  (** The ideal quotient of I by unit is I. *)
  Lemma ideal_quotient_unit_bottom (I : Ideal R)
    : (I :: ideal_unit R) ↔ I.
R: Ring
I: Ideal R
I :: ideal_unit R ↔ I
  Proof.
R: Ring
I: Ideal R
I :: ideal_unit R ↔ I
    apply ideal_subset_antisymm.
R: Ring
I: Ideal R
(I :: ideal_unit R) ⊆ I
R: Ring
I: Ideal R
I ⊆ (I :: ideal_unit R)
    -
R: Ring
I: Ideal R
(I :: ideal_unit R) ⊆ I intros r [p q].
R: Ring
I: Ideal R
r: R
p: leftideal_quotient I (ideal_unit R) r
q: rightideal_quotient I (ideal_unit R) r
I r
      strip_truncations.
R: Ring
I: Ideal R
r: R
q: forall x : rng_op R, ideal_unit R x -> I (r * x)
p: forall x : R, ideal_unit R x -> I (r * x)
I r
      rewrite <- rng_mult_one_r.
R: Ring
I: Ideal R
r: R
q: forall x : rng_op R, ideal_unit R x -> I (r * x)
p: forall x : R, ideal_unit R x -> I (r * x)
I (r * 1)
      exact (p ring_one tt).
    -
R: Ring
I: Ideal R
I ⊆ (I :: ideal_unit R) apply ideal_quotient_subset.
  Defined.

  (** The ideal quotient of unit by I is unit. *)
  Lemma ideal_quotient_unit_top (I : Ideal R)
    : (ideal_unit R :: I) ↔ ideal_unit R.
R: Ring
I: Ideal R
ideal_unit R :: I ↔ ideal_unit R
  Proof.
R: Ring
I: Ideal R
ideal_unit R :: I ↔ ideal_unit R
    split.
R: Ring
I: Ideal R
x: R
(ideal_unit R :: I) x -> ideal_unit R x
R: Ring
I: Ideal R
x: R
ideal_unit R x -> (ideal_unit R :: I) x
    -
R: Ring
I: Ideal R
x: R
(ideal_unit R :: I) x -> ideal_unit R x cbn; trivial.
    -
R: Ring
I: Ideal R
x: R
ideal_unit R x -> (ideal_unit R :: I) x intros ?; split; apply tr;
      cbn; split; trivial. 
  Defined.

  (** The ideal quotient by a sum is an intersection of ideal quotients. *)
  Lemma ideal_quotient_sum (I J K : Ideal R)
    : (I :: (J + K)) ↔ (I :: J) ∩ (I :: K).
R: Ring
I, J, K: Ideal R
I :: J + K ↔ (I :: J) ∩ (I :: K)
  Proof.
R: Ring
I, J, K: Ideal R
I :: J + K ↔ (I :: J) ∩ (I :: K)
    apply ideal_subset_antisymm.
R: Ring
I, J, K: Ideal R
(I :: J + K) ⊆ (I :: J) ∩ (I :: K)
R: Ring
I, J, K: Ideal R
(I :: J) ∩ (I :: K) ⊆ (I :: J + K)
    {
R: Ring
I, J, K: Ideal R
(I :: J + K) ⊆ (I :: J) ∩ (I :: K) intros r [p q]; strip_truncations; split; split; apply tr; intros x jk.
R: Ring
I, J, K: Ideal R
r: R
q: forall x : rng_op R, (J + K)%ideal x -> I (r * x)
p: forall x : R, (J + K)%ideal x -> I (r * x)
x: R
jk: J x
I (r * x)
R: Ring
I, J, K: Ideal R
r: R
q: forall x : rng_op R, (J + K)%ideal x -> I (r * x)
p: forall x : R, (J + K)%ideal x -> I (r * x)
x: rng_op R
jk: J x
I (r * x)
R: Ring
I, J, K: Ideal R
r: R
q: forall x : rng_op R, (J + K)%ideal x -> I (r * x)
p: forall x : R, (J + K)%ideal x -> I (r * x)
x: R
jk: K x
I (r * x)
R: Ring
I, J, K: Ideal R
r: R
q: forall x : rng_op R, (J + K)%ideal x -> I (r * x)
p: forall x : R, (J + K)%ideal x -> I (r * x)
x: rng_op R
jk: K x
I (r * x)
      -
R: Ring
I, J, K: Ideal R
r: R
q: forall x : rng_op R, (J + K)%ideal x -> I (r * x)
p: forall x : R, (J + K)%ideal x -> I (r * x)
x: R
jk: J x
I (r * x) by rapply p; rapply ideal_sum_subset_l.
      -
R: Ring
I, J, K: Ideal R
r: R
q: forall x : rng_op R, (J + K)%ideal x -> I (r * x)
p: forall x : R, (J + K)%ideal x -> I (r * x)
x: rng_op R
jk: J x
I (r * x) by rapply q; rapply ideal_sum_subset_l.
      -
R: Ring
I, J, K: Ideal R
r: R
q: forall x : rng_op R, (J + K)%ideal x -> I (r * x)
p: forall x : R, (J + K)%ideal x -> I (r * x)
x: R
jk: K x
I (r * x) by rapply p; rapply ideal_sum_subset_r.
      -
R: Ring
I, J, K: Ideal R
r: R
q: forall x : rng_op R, (J + K)%ideal x -> I (r * x)
p: forall x : R, (J + K)%ideal x -> I (r * x)
x: rng_op R
jk: K x
I (r * x) by rapply q; rapply ideal_sum_subset_r. }
R: Ring
I, J, K: Ideal R
(I :: J) ∩ (I :: K) ⊆ (I :: J + K)
    intros r [[p q] [u v]]; strip_truncations; split; apply tr;
    intros x jk; strip_truncations.
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
x: R
jk: subgroup_generated_type
  (fun x : R => (J x + K x)%type) x
I (r * x)
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
x: rng_op R
jk: subgroup_generated_type
  (fun x : R => (J x + K x)%type) x
I (r * x)
    -
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
x: R
jk: subgroup_generated_type
  (fun x : R => (J x + K x)%type) x
I (r * x) induction jk as [? [] | | ? ? ? ? ? ? ].
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g: R
s: J g
I (r * g)
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g: R
s: K g
I (r * g)
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
I (r * mon_unit)
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g, h: R
jk1: subgroup_generated_type (fun x : R => (J x + K x)%type) g
jk2: subgroup_generated_type (fun x : R => (J x + K x)%type) h
IHjk1: I (r * g)
IHjk2: I (r * h)
I (r * sg_op g (inv h))
      +
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g: R
s: J g
I (r * g) by apply p.
      +
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g: R
s: K g
I (r * g) by apply u.
      +
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
I (r * mon_unit) apply u, ideal_in_zero.
      +
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g, h: R
jk1: subgroup_generated_type (fun x : R => (J x + K x)%type) g
jk2: subgroup_generated_type (fun x : R => (J x + K x)%type) h
IHjk1: I (r * g)
IHjk2: I (r * h)
I (r * sg_op g (inv h)) rewrite rng_dist_l.
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g, h: R
jk1: subgroup_generated_type (fun x : R => (J x + K x)%type) g
jk2: subgroup_generated_type (fun x : R => (J x + K x)%type) h
IHjk1: I (r * g)
IHjk2: I (r * h)
I (plus (r * g) (r * inv h))
        rewrite rng_mult_negate_r.
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g, h: R
jk1: subgroup_generated_type (fun x : R => (J x + K x)%type) g
jk2: subgroup_generated_type (fun x : R => (J x + K x)%type) h
IHjk1: I (r * g)
IHjk2: I (r * h)
I (r * g - r * h)
        by apply ideal_in_plus_negate.
    -
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
x: rng_op R
jk: subgroup_generated_type
  (fun x : R => (J x + K x)%type) x
I (r * x) induction jk as [? [] | | ? ? ? ? ? ? ].
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g: R
s: J g
I (r * g)
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g: R
s: K g
I (r * g)
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
I (r * mon_unit)
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g, h: R
jk1: subgroup_generated_type (fun x : R => (J x + K x)%type) g
jk2: subgroup_generated_type (fun x : R => (J x + K x)%type) h
IHjk1: I (r * g)
IHjk2: I (r * h)
I (r * sg_op g (inv h))
      +
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g: R
s: J g
I (r * g) by apply q.
      +
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g: R
s: K g
I (r * g) by apply v.
      +
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
I (r * mon_unit) apply v, ideal_in_zero.
      +
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g, h: R
jk1: subgroup_generated_type (fun x : R => (J x + K x)%type) g
jk2: subgroup_generated_type (fun x : R => (J x + K x)%type) h
IHjk1: I (r * g)
IHjk2: I (r * h)
I (r * sg_op g (inv h)) change (I ((g - h) * r)).
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g, h: R
jk1: subgroup_generated_type (fun x : R => (J x + K x)%type) g
jk2: subgroup_generated_type (fun x : R => (J x + K x)%type) h
IHjk1: I (r * g)
IHjk2: I (r * h)
I ((g - h) * r) 
        rewrite rng_dist_r.
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g, h: R
jk1: subgroup_generated_type (fun x : R => (J x + K x)%type) g
jk2: subgroup_generated_type (fun x : R => (J x + K x)%type) h
IHjk1: I (r * g)
IHjk2: I (r * h)
I (plus (g * r) (- h * r))
        rewrite rng_mult_negate_l.
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> I (r * x)
u: forall x : R, K x -> I (r * x)
q: forall x : rng_op R, J x -> I (r * x)
p: forall x : R, J x -> I (r * x)
g, h: R
jk1: subgroup_generated_type (fun x : R => (J x + K x)%type) g
jk2: subgroup_generated_type (fun x : R => (J x + K x)%type) h
IHjk1: I (r * g)
IHjk2: I (r * h)
I (g * r - h * r)
        by apply ideal_in_plus_negate.
  Defined.

  (** Ideal quotients distribute over intersections. *)
  Lemma ideal_quotient_intersection (I J K : Ideal R)
    : (I ∩ J :: K) ↔ (I :: K) ∩ (J :: K).
R: Ring
I, J, K: Ideal R
I ∩ J :: K ↔ (I :: K) ∩ (J :: K)
  Proof.
R: Ring
I, J, K: Ideal R
I ∩ J :: K ↔ (I :: K) ∩ (J :: K)
    apply ideal_subset_antisymm.
R: Ring
I, J, K: Ideal R
(I ∩ J :: K) ⊆ (I :: K) ∩ (J :: K)
R: Ring
I, J, K: Ideal R
(I :: K) ∩ (J :: K) ⊆ (I ∩ J :: K)
    -
R: Ring
I, J, K: Ideal R
(I ∩ J :: K) ⊆ (I :: K) ∩ (J :: K) intros r [p q]; strip_truncations; split; split; apply tr; intros x k.
R: Ring
I, J, K: Ideal R
r: R
q: forall x : rng_op R, K x -> (I ∩ J) (r * x)
p: forall x : R, K x -> (I ∩ J) (r * x)
x: R
k: K x
I (r * x)
R: Ring
I, J, K: Ideal R
r: R
q: forall x : rng_op R, K x -> (I ∩ J) (r * x)
p: forall x : R, K x -> (I ∩ J) (r * x)
x: rng_op R
k: K x
I (r * x)
R: Ring
I, J, K: Ideal R
r: R
q: forall x : rng_op R, K x -> (I ∩ J) (r * x)
p: forall x : R, K x -> (I ∩ J) (r * x)
x: R
k: K x
J (r * x)
R: Ring
I, J, K: Ideal R
r: R
q: forall x : rng_op R, K x -> (I ∩ J) (r * x)
p: forall x : R, K x -> (I ∩ J) (r * x)
x: rng_op R
k: K x
J (r * x)
      1,3: by apply p.
R: Ring
I, J, K: Ideal R
r: R
q: forall x : rng_op R, K x -> (I ∩ J) (r * x)
p: forall x : R, K x -> (I ∩ J) (r * x)
x: rng_op R
k: K x
I (r * x)
R: Ring
I, J, K: Ideal R
r: R
q: forall x : rng_op R, K x -> (I ∩ J) (r * x)
p: forall x : R, K x -> (I ∩ J) (r * x)
x: rng_op R
k: K x
J (r * x)
      1,2: by apply q.
    -
R: Ring
I, J, K: Ideal R
(I :: K) ∩ (J :: K) ⊆ (I ∩ J :: K) intros r [[p q] [u v]].
R: Ring
I, J, K: Ideal R
r: R
p: leftideal_quotient I K r
q: rightideal_quotient I K r
u: leftideal_quotient J K r
v: rightideal_quotient J K r
(I ∩ J :: K) r
      strip_truncations; split; apply tr; intros x k; split.
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> J (r * x)
u: forall x : R, K x -> J (r * x)
q: forall x : rng_op R, K x -> I (r * x)
p: forall x : R, K x -> I (r * x)
x: R
k: K x
I (r * x)
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> J (r * x)
u: forall x : R, K x -> J (r * x)
q: forall x : rng_op R, K x -> I (r * x)
p: forall x : R, K x -> I (r * x)
x: R
k: K x
J (r * x)
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> J (r * x)
u: forall x : R, K x -> J (r * x)
q: forall x : rng_op R, K x -> I (r * x)
p: forall x : R, K x -> I (r * x)
x: rng_op R
k: K x
I (r * x)
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> J (r * x)
u: forall x : R, K x -> J (r * x)
q: forall x : rng_op R, K x -> I (r * x)
p: forall x : R, K x -> I (r * x)
x: rng_op R
k: K x
J (r * x)
      +
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> J (r * x)
u: forall x : R, K x -> J (r * x)
q: forall x : rng_op R, K x -> I (r * x)
p: forall x : R, K x -> I (r * x)
x: R
k: K x
I (r * x) by apply p.
      +
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> J (r * x)
u: forall x : R, K x -> J (r * x)
q: forall x : rng_op R, K x -> I (r * x)
p: forall x : R, K x -> I (r * x)
x: R
k: K x
J (r * x) by apply u.
      +
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> J (r * x)
u: forall x : R, K x -> J (r * x)
q: forall x : rng_op R, K x -> I (r * x)
p: forall x : R, K x -> I (r * x)
x: rng_op R
k: K x
I (r * x) by apply q.
      +
R: Ring
I, J, K: Ideal R
r: R
v: forall x : rng_op R, K x -> J (r * x)
u: forall x : R, K x -> J (r * x)
q: forall x : rng_op R, K x -> I (r * x)
p: forall x : R, K x -> I (r * x)
x: rng_op R
k: K x
J (r * x) by apply v.
  Defined.

  (** Annihilators reverse the order of inclusion. *)
  Lemma ideal_annihilator_subset (I J : Ideal R) : I ⊆ J -> Ann J ⊆ Ann I.
R: Ring
I, J: Ideal R
I ⊆ J -> Ann J ⊆ Ann I
  Proof.
R: Ring
I, J: Ideal R
I ⊆ J -> Ann J ⊆ Ann I
    intros p x [q q']; hnf in q, q'; strip_truncations;
      split; apply tr; intros y i.
R: Ring
I, J: Ideal R
p: I ⊆ J
x: R
q': forall x0 : rng_op R, J x0 -> x * x0 = ring_zero
q: forall x0 : R, J x0 -> x * x0 = ring_zero
y: R
i: I y
x * y = ring_zero
R: Ring
I, J: Ideal R
p: I ⊆ J
x: R
q': forall x0 : rng_op R, J x0 -> x * x0 = ring_zero
q: forall x0 : R, J x0 -> x * x0 = ring_zero
y: rng_op R
i: I y
x * y = ring_zero
    -
R: Ring
I, J: Ideal R
p: I ⊆ J
x: R
q': forall x0 : rng_op R, J x0 -> x * x0 = ring_zero
q: forall x0 : R, J x0 -> x * x0 = ring_zero
y: R
i: I y
x * y = ring_zero by apply q, p.
    -
R: Ring
I, J: Ideal R
p: I ⊆ J
x: R
q': forall x0 : rng_op R, J x0 -> x * x0 = ring_zero
q: forall x0 : R, J x0 -> x * x0 = ring_zero
y: rng_op R
i: I y
x * y = ring_zero by apply q', p.
  Defined.

  (** The annihilator of an ideal is equal to a quotient of zero. *)
  Lemma ideal_annihilator_zero_quotient (I : Ideal R)
    : Ann I ↔ ideal_zero R :: I.
R: Ring
I: Ideal R
Ann I ↔ ideal_zero R :: I
  Proof.
R: Ring
I: Ideal R
Ann I ↔ ideal_zero R :: I
    intros x; split.
R: Ring
I: Ideal R
x: R
Ann I x -> (ideal_zero R :: I) x
R: Ring
I: Ideal R
x: R
(ideal_zero R :: I) x -> Ann I x
    -
R: Ring
I: Ideal R
x: R
Ann I x -> (ideal_zero R :: I) x intros [p q]; strip_truncations; split; apply tr; intros y i.
R: Ring
I: Ideal R
x: R
q: forall x0 : rng_op R, I x0 -> x * x0 = ring_zero
p: forall x0 : R, I x0 -> x * x0 = ring_zero
y: R
i: I y
ideal_zero R (x * y)
R: Ring
I: Ideal R
x: R
q: forall x0 : rng_op R, I x0 -> x * x0 = ring_zero
p: forall x0 : R, I x0 -> x * x0 = ring_zero
y: rng_op R
i: I y
ideal_zero R (x * y)
      +
R: Ring
I: Ideal R
x: R
q: forall x0 : rng_op R, I x0 -> x * x0 = ring_zero
p: forall x0 : R, I x0 -> x * x0 = ring_zero
y: R
i: I y
ideal_zero R (x * y) exact (p y i).
      +
R: Ring
I: Ideal R
x: R
q: forall x0 : rng_op R, I x0 -> x * x0 = ring_zero
p: forall x0 : R, I x0 -> x * x0 = ring_zero
y: rng_op R
i: I y
ideal_zero R (x * y) exact (q y i).
    -
R: Ring
I: Ideal R
x: R
(ideal_zero R :: I) x -> Ann I x intros [p q]; strip_truncations; split; apply tr; intros y i.
R: Ring
I: Ideal R
x: R
q: forall x0 : rng_op R,
I x0 -> ideal_zero R (x * x0)
p: forall x0 : R, I x0 -> ideal_zero R (x * x0)
y: R
i: I y
x * y = ring_zero
R: Ring
I: Ideal R
x: R
q: forall x0 : rng_op R,
I x0 -> ideal_zero R (x * x0)
p: forall x0 : R, I x0 -> ideal_zero R (x * x0)
y: rng_op R
i: I y
x * y = ring_zero
      +
R: Ring
I: Ideal R
x: R
q: forall x0 : rng_op R,
I x0 -> ideal_zero R (x * x0)
p: forall x0 : R, I x0 -> ideal_zero R (x * x0)
y: R
i: I y
x * y = ring_zero exact (p y i).
      +
R: Ring
I: Ideal R
x: R
q: forall x0 : rng_op R,
I x0 -> ideal_zero R (x * x0)
p: forall x0 : R, I x0 -> ideal_zero R (x * x0)
y: rng_op R
i: I y
x * y = ring_zero exact (q y i).
  Defined.

End IdealLemmas.

(** ** Preimage of ideals under ring homomorphisms *)

(** The preimage of an ideal under a ring homomorphism is also itself an ideal. This is also known as the contraction of an ideal. *)

Instance isleftideal_preimage {R S : Ring} (f : R $-> S)
  (I : Subgroup S) `{IsLeftIdeal S I}
  : IsLeftIdeal (subgroup_preimage f I).
R, S: Ring
f: R $-> S
I: Subgroup S
H: IsLeftIdeal I
IsLeftIdeal (subgroup_preimage f I)
Proof.
R, S: Ring
f: R $-> S
I: Subgroup S
H: IsLeftIdeal I
IsLeftIdeal (subgroup_preimage f I)
  intros r x Ifx.
R, S: Ring
f: R $-> S
I: Subgroup S
H: IsLeftIdeal I
r, x: R
Ifx: subgroup_preimage f I x
subgroup_preimage f I (r * x)
  nrefine (transport I (rng_homo_mult f _ _)^ _).
R, S: Ring
f: R $-> S
I: Subgroup S
H: IsLeftIdeal I
r, x: R
Ifx: subgroup_preimage f I x
I (f r * f x)
  rapply isleftideal.
R, S: Ring
f: R $-> S
I: Subgroup S
H: IsLeftIdeal I
r, x: R
Ifx: subgroup_preimage f I x
I (f x)
  exact Ifx.
Defined.

Instance isrightideal_preimage {R S : Ring} (f : R $-> S)
  (I : Subgroup S) `{IsRightIdeal S I}
  : IsRightIdeal (subgroup_preimage f I)
  := isleftideal_preimage (R:=rng_op R) (S:=rng_op S)
      (fmap rng_op f) I.

Instance isideal_preimage {R S : Ring} (f : R $-> S)
  (I : Subgroup S) `{IsIdeal S I}
  : IsIdeal (subgroup_preimage f I)
  := {}.

Definition ideal_preimage {R S : Ring} (f : R $-> S) (I : Ideal S)
  : Ideal R
  := Build_Ideal R (subgroup_preimage f I) _.

(** ** Extensions of ideals *)

(** The extension of an ideal under a ring homomorphism is the ideal generated by the image of the ideal. *)
Definition ideal_extension {R S : Ring} (f : R $-> S) (I : Ideal R) : Ideal S
  := ideal_generated (fun s => exists r, I r /\ f r = s).

(** The extension of a preimage is always a subset of the original ideal. *)
Definition ideal_subset_extension_preimage {R S : Ring} (f : R $-> S)
  (I : Ideal S)
  : ideal_extension f (ideal_preimage f I) ⊆ I.
R, S: Ring
f: R $-> S
I: Ideal S
ideal_extension f (ideal_preimage f I) ⊆ I
Proof.
R, S: Ring
f: R $-> S
I: Ideal S
ideal_extension f (ideal_preimage f I) ⊆ I
  intros x.
R, S: Ring
f: R $-> S
I: Ideal S
x: S
ideal_extension f (ideal_preimage f I) x -> I x
  apply Trunc_rec.
R, S: Ring
f: R $-> S
I: Ideal S
x: S
ideal_generated_type
  (fun s : S =>
   {r : R & (ideal_preimage f I r * (f r = s))%type})
  x -> I x
  intros y.
R, S: Ring
f: R $-> S
I: Ideal S
x: S
y: ideal_generated_type
  (fun s : S =>
   {r : R &
   (ideal_preimage f I r * (f r = s))%type}) x
I x
  induction y.
R, S: Ring
f: R $-> S
I: Ideal S
r: S
x: {r0 : R &
(ideal_preimage f I r0 * (f r0 = r))%type}
I r
R, S: Ring
f: R $-> S
I: Ideal S
I ring_zero
R, S: Ring
f: R $-> S
I: Ideal S
r, s: S
y1: ideal_generated_type
  (fun s : S =>
   {r : R &
   (ideal_preimage f I r * (f r = s))%type}) r
y2: ideal_generated_type
  (fun s : S =>
   {r : R &
   (ideal_preimage f I r * (f r = s))%type}) s
IHy1: I r
IHy2: I s
I (r - s)
R, S: Ring
f: R $-> S
I: Ideal S
r, s: S
y: ideal_generated_type
  (fun s : S =>
   {r : R &
   (ideal_preimage f I r * (f r = s))%type}) s
IHy: I s
I (r * s)
R, S: Ring
f: R $-> S
I: Ideal S
r, s: S
y: ideal_generated_type
  (fun s : S =>
   {r : R &
   (ideal_preimage f I r * (f r = s))%type}) r
IHy: I r
I (r * s)
  +
R, S: Ring
f: R $-> S
I: Ideal S
r: S
x: {r0 : R &
(ideal_preimage f I r0 * (f r0 = r))%type}
I r destruct x as [s [p q]].
R, S: Ring
f: R $-> S
I: Ideal S
r: S
s: R
p: ideal_preimage f I s
q: f s = r
I r
    destruct q; exact p.
  +
R, S: Ring
f: R $-> S
I: Ideal S
I ring_zero apply ideal_in_zero.
  +
R, S: Ring
f: R $-> S
I: Ideal S
r, s: S
y1: ideal_generated_type
  (fun s : S =>
   {r : R &
   (ideal_preimage f I r * (f r = s))%type}) r
y2: ideal_generated_type
  (fun s : S =>
   {r : R &
   (ideal_preimage f I r * (f r = s))%type}) s
IHy1: I r
IHy2: I s
I (r - s) by apply ideal_in_plus_negate.
  +
R, S: Ring
f: R $-> S
I: Ideal S
r, s: S
y: ideal_generated_type
  (fun s : S =>
   {r : R &
   (ideal_preimage f I r * (f r = s))%type}) s
IHy: I s
I (r * s) by rapply isleftideal.
  +
R, S: Ring
f: R $-> S
I: Ideal S
r, s: S
y: ideal_generated_type
  (fun s : S =>
   {r : R &
   (ideal_preimage f I r * (f r = s))%type}) r
IHy: I r
I (r * s) by rapply isrightideal.
Defined.

(** TODO: Maximal ideals *)
(** TODO: Principal ideal *)
(** TODO: Prime ideals *)
(** TODO: Radical ideals *)
(** TODO: Minimal ideals *)
(** TODO: Primary ideals *)