Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Spaces.Nat.Core.(* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *)Require Import Classes.interfaces.abstract_algebra.Require Import Algebra.AbGroups.Require Export Classes.theory.rings.Require Import Modalities.ReflectiveSubuniverse.(** * Rings *)Declare Scope ring_scope.LocalOpen Scope ring_scope.(** We want to print equivalences as [≅]. *)LocalOpen Scope wc_iso_scope.(** A ring consists of the following data: *)RecordRing := Build_Ring' {
(** An underlying abelian group. *)
ring_abgroup :> AbGroup;
(** A multiplication operation. *)
ring_mult :: Mult ring_abgroup;
(** A multiplicative identity called [one]. *)
ring_one :: One ring_abgroup;
(** Such that all they all satisfy the axioms of a ring. *)
ring_isring :: IsRing ring_abgroup;
(** This field only exists so that opposite rings are definitionally involutive and can safely be ignored. *)
ring_mult_assoc_opp : forallzyx, (x * y) * z = x * (y * z);
}.Arguments ring_mult {_}.Arguments ring_one {_}.Arguments ring_isring {_}.Definitionissig_Ring : _ <~> Ring := ltac:(issig).Global Instancering_plus {R : Ring} : Plus R := plus_abgroup (ring_abgroup R).Global Instancering_zero {R : Ring} : Zero R := zero_abgroup (ring_abgroup R).Global Instancering_negate {R : Ring} : Negate R := negate_abgroup (ring_abgroup R).(** A ring homomorphism between rings is a map of the underlying type and a proof that this map is a ring homomorphism. *)RecordRingHomomorphism (AB : Ring) := {
rng_homo_map :> A -> B;
rng_homo_ishomo :: IsSemiRingPreserving rng_homo_map;
}.Arguments Build_RingHomomorphism {_ _} _ _.Definitionissig_RingHomomorphism (AB : Ring)
: _ <~> RingHomomorphism A B
:= ltac:(issig).
H: Funext A, B: Ring f, g: RingHomomorphism A B
f == g <~> f = g
H: Funext A, B: Ring f, g: RingHomomorphism A B
f == g <~> f = g
H: Funext A, B: Ring f, g: RingHomomorphism A B
f == g <~>
(issig_RingHomomorphism A B)^-1 f =
(issig_RingHomomorphism A B)^-1 g
H: Funext A, B: Ring f, g: RingHomomorphism A B
f == g <~>
((issig_RingHomomorphism A B)^-1 f).1 =
((issig_RingHomomorphism A B)^-1 g).1
apply equiv_path_forall.Defined.Definitionrng_homo_id (A : Ring) : RingHomomorphism A A
:= Build_RingHomomorphism idmap (Build_IsSemiRingPreserving _ _ _).
A, B, C: Ring f: RingHomomorphism B C g: RingHomomorphism A B
RingHomomorphism A C
A, B, C: Ring f: RingHomomorphism B C g: RingHomomorphism A B
RingHomomorphism A C
A, B, C: Ring f: RingHomomorphism B C g: RingHomomorphism A B
A -> C
A, B, C: Ring f: RingHomomorphism B C g: RingHomomorphism A B
IsSemiRingPreserving ?rng_homo_map
A, B, C: Ring f: RingHomomorphism B C g: RingHomomorphism A B
IsSemiRingPreserving (f o g)
rapply compose_sr_morphism.Defined.(** ** Ring laws *)SectionRingLaws.(** Many of these ring laws have already been proven. But we give them names here so that they are easy to find and use. *)Context {AB : Ring} (f : RingHomomorphism A B) (xyz : A).Definitionrng_dist_l : x * (y + z) = x * y + x * z := simple_distribute_l _ _ _.Definitionrng_dist_r : (x + y) * z = x * z + y * z := simple_distribute_r _ _ _.Definitionrng_plus_zero_l : 0 + x = x := left_identity _.Definitionrng_plus_zero_r : x + 0 = x := right_identity _.Definitionrng_plus_negate_l : (- x) + x = 0 := left_inverse _.Definitionrng_plus_negate_r : x + (- x) = 0 := right_inverse _.Definitionrng_plus_comm : x + y = y + x := commutativity x y.Definitionrng_plus_assoc : x + (y + z) = (x + y) + z := simple_associativity x y z.Definitionrng_mult_assoc : x * (y * z) = (x * y) * z := simple_associativity x y z.Definitionrng_negate_negate : - (- x) = x := groups.negate_involutive _.Definitionrng_mult_one_l : 1 * x = x := left_identity _.Definitionrng_mult_one_r : x * 1 = x := right_identity _.Definitionrng_mult_zero_l : 0 * x = 0 := left_absorb _.Definitionrng_mult_zero_r : x * 0 = 0 := right_absorb _.Definitionrng_mult_negate : -1 * x = - x := (negate_mult_l _)^.Definitionrng_mult_negate_negate : -x * -y = x * y := negate_mult_negate _ _.Definitionrng_mult_negate_l : -x * y = -(x * y) := inverse (negate_mult_distr_l _ _).Definitionrng_mult_negate_r : x * -y = -(x * y) := inverse (negate_mult_distr_r _ _).Definitionrng_homo_plus : f (x + y) = f x + f y := preserves_plus x y.Definitionrng_homo_mult : f (x * y) = f x * f y := preserves_mult x y.Definitionrng_homo_zero : f 0 = 0 := preserves_0.Definitionrng_homo_one : f 1 = 1 := preserves_1.Definitionrng_homo_negate : f (-x) = -(f x) := preserves_negate x.Definitionrng_homo_minus_one : f (-1) = -1
:= preserves_negate 1%mc @ ap negate preserves_1.EndRingLaws.(** Isomorphisms of commutative rings *)RecordRingIsomorphism (AB : Ring) := {
rng_iso_homo : RingHomomorphism A B ;
isequiv_rng_iso_homo : IsEquiv rng_iso_homo ;
}.Arguments rng_iso_homo {_ _ }.Coercionrng_iso_homo : RingIsomorphism >-> RingHomomorphism.Global Existing Instanceisequiv_rng_iso_homo.Definitionissig_RingIsomorphism {AB : Ring}
: _ <~> RingIsomorphism A B := ltac:(issig).(** We can construct a ring isomorphism from an equivalence that preserves addition and multiplication. *)DefinitionBuild_RingIsomorphism' (AB : Ring) (e : A <~> B)
`{!IsSemiRingPreserving e}
: RingIsomorphism A B
:= Build_RingIsomorphism A B (Build_RingHomomorphism e _) _.(** The inverse of a Ring isomorphism *)
A, B: Ring
RingIsomorphism A B -> RingIsomorphism B A
A, B: Ring
RingIsomorphism A B -> RingIsomorphism B A
A, B: Ring f: RingHomomorphism A B e: IsEquiv f
RingIsomorphism B A
A, B: Ring f: RingHomomorphism A B e: IsEquiv f
RingHomomorphism B A
A, B: Ring f: RingHomomorphism A B e: IsEquiv f
IsEquiv ?rng_iso_homo
A, B: Ring f: RingHomomorphism A B e: IsEquiv f
RingHomomorphism B A
A, B: Ring f: RingHomomorphism A B e: IsEquiv f
B -> A
A, B: Ring f: RingHomomorphism A B e: IsEquiv f
IsSemiRingPreserving ?rng_homo_map
A, B: Ring f: RingHomomorphism A B e: IsEquiv f
IsSemiRingPreserving f^-1
exact _.
A, B: Ring f: RingHomomorphism A B e: IsEquiv f
IsEquiv
{|
rng_homo_map := f^-1;
rng_homo_ishomo :=
invert_sr_morphism f (rng_homo_ishomo A B f)
|}
exact _.Defined.(** Ring isomorphisms are a reflexive relation *)Global Instancereflexive_ringisomorphism : Reflexive RingIsomorphism
:= funx => Build_RingIsomorphism _ _ (rng_homo_id x) _.(** Ring isomorphisms are a symmetric relation *)Global Instancesymmetry_ringisomorphism : Symmetric RingIsomorphism
:= funxy => rng_iso_inverse.(** Ring isomorphisms are a transitive relation *)Global Instancetransitive_ringisomorphism : Transitive RingIsomorphism
:= funxyzfg => Build_RingIsomorphism _ _ (rng_homo_compose g f) _.(** Underlying group homomorphism of a ring homomorphism *)Definitiongrp_homo_rng_homo {RS : Ring}
: RingHomomorphism R S -> GroupHomomorphism R S
:= funf => @Build_GroupHomomorphism R S f _.Coerciongrp_homo_rng_homo : RingHomomorphism >-> GroupHomomorphism.(** We can construct a ring homomorphism from a group homomorphism that preserves multiplication *)DefinitionBuild_RingHomomorphism' (AB : Ring) (map : GroupHomomorphism A B)
{H : IsMonoidPreserving (Aop:=ring_mult) (Bop:=ring_mult)
(Aunit:=one) (Bunit:=one) map}
: RingHomomorphism A B
:= Build_RingHomomorphism map
(Build_IsSemiRingPreserving _ (grp_homo_ishomo _ _ map) H).(** We can construct a ring isomorphism from a group isomorphism that preserves multiplication *)DefinitionBuild_RingIsomorphism'' (AB : Ring) (e : GroupIsomorphism A B)
{H : IsMonoidPreserving (Aop:=ring_mult) (Bop:=ring_mult) (Aunit:=one) (Bunit:=one) e}
: RingIsomorphism A B
:= @Build_RingIsomorphism' A B e (Build_IsSemiRingPreserving e _ H).(** Here is an alternative way to build a commutative ring using the underlying abelian group. *)DefinitionBuild_Ring (R : AbGroup)
`(Mult R, One R, LeftDistribute R mult (@group_sgop R), RightDistribute R mult (@group_sgop R))
(iscomm : @IsMonoid R mult one)
: Ring
:= Build_Ring' R _ _ (Build_IsRing _ _ _ _ _) (funzyx => (associativity x y z)^).(** Scalar multiplication on the left is a group homomorphism. *)Definitiongrp_homo_rng_left_mult {R : Ring} (r : R)
: GroupHomomorphism R R
:= @Build_GroupHomomorphism R R (funs => r * s) (rng_dist_l r).(** Scalar multiplication on the right is a group homomorphism. *)Definitiongrp_homo_rng_right_mult {R : Ring} (r : R)
: GroupHomomorphism R R
:= @Build_GroupHomomorphism R R (funs => s * r) (funxy => rng_dist_r x y r).(** ** Ring movement lemmas *)SectionRingMovement.(** We adopt a similar naming convention to the [moveR_equiv] style lemmas that can be found in Types.Paths. *)Context {R : Ring} {xyz : R}.Definitionrng_moveL_Mr : - y + x = z <~> x = y + z := @grp_moveL_Mg R x y z.Definitionrng_moveL_rM : x + - z = y <~> x = y + z := @grp_moveL_gM R x y z.Definitionrng_moveR_Mr : y = - x + z <~> x + y = z := @grp_moveR_Mg R x y z.Definitionrng_moveR_rM : x = z + - y <~> x + y = z := @grp_moveR_gM R x y z.Definitionrng_moveL_Vr : x + y = z <~> y = - x + z := @grp_moveL_Vg R x y z.Definitionrng_moveL_rV : x + y = z <~> x = z + - y := @grp_moveL_gV R x y z.Definitionrng_moveR_Vr : x = y + z <~> - y + x = z := @grp_moveR_Vg R x y z.Definitionrng_moveR_rV : x = y + z <~> x + - z = y := @grp_moveR_gV R x y z.Definitionrng_moveL_M0 : - y + x = 0 <~> x = y := @grp_moveL_M1 R x y.Definitionrng_moveL_0M : x + - y = 0 <~> x = y := @grp_moveL_1M R x y.Definitionrng_moveR_M0 : 0 = - x + y <~> x = y := @grp_moveR_M1 R x y.Definitionrng_moveR_0M : 0 = y + - x <~> x = y := @grp_moveR_1M R x y.(** TODO: Movement laws about mult *)EndRingMovement.(** ** Wild category of rings *)Global Instanceisgraph_ring : IsGraph Ring
:= Build_IsGraph _ RingHomomorphism.Global Instanceis01cat_ring : Is01Cat Ring
:= Build_Is01Cat _ _ rng_homo_id (@rng_homo_compose).Global Instanceis2graph_ring : Is2Graph Ring
:= funAB => isgraph_induced (@rng_homo_map A B : _ -> (group_type _ $-> _)).Global Instanceis01cat_ringhomomorphism {AB : Ring} : Is01Cat (A $-> B)
:= is01cat_induced (@rng_homo_map A B).Global Instanceis0gpd_ringhomomorphism {AB : Ring} : Is0Gpd (A $-> B)
:= is0gpd_induced (@rng_homo_map A B).
A, B, C: Ring h: B $-> C
Is0Functor (cat_postcomp A h)
A, B, C: Ring h: B $-> C
Is0Functor (cat_postcomp A h)
A, B, C: Ring h: B $-> C
forallab : A $-> B,
(a $-> b) -> cat_postcomp A h a $-> cat_postcomp A h b
intros [f ?] [g ?] p a ; exact (ap h (p a)).Defined.
A, B, C: Ring h: A $-> B
Is0Functor (cat_precomp C h)
A, B, C: Ring h: A $-> B
Is0Functor (cat_precomp C h)
A, B, C: Ring h: A $-> B
forallab : B $-> C,
(a $-> b) -> cat_precomp C h a $-> cat_precomp C h b
intros [f ?] [g ?] p a ; exact (p (h a)).Defined.(** Ring forms a 1-category. *)
Is1Cat Ring
Is1Cat Ring
by rapply Build_Is1Cat.Defined.
H: Funext
HasMorExt Ring
H: Funext
HasMorExt Ring
H: Funext
forall (ab : Ring) (fg : a $-> b),
IsEquiv GpdHom_path
forall (ab : Ring) (f : a $-> b),
?CatIsEquiv' a b f -> ?CatEquiv' a b
forallab : Ring, ?CatEquiv' a b -> b $-> a
forall (ab : Ring) (f : ?CatEquiv' a b),
?CatIsEquiv' a b (?cate_fun' a b f)
forall (ab : Ring) (f : a $-> b)
(fe : ?CatIsEquiv' a b f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
forall (ab : Ring) (f : ?CatEquiv' a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
forall (ab : Ring) (f : ?CatEquiv' a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
forall (ab : Ring) (f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> ?CatIsEquiv' a b f
Ring -> Ring -> Type
exact RingIsomorphism.
forallab : Ring, (a $-> b) -> Type
exact (funGHf => IsEquiv f).
forallab : Ring, RingIsomorphism a b -> a $-> b
intros G H f; exact f.
forall (ab : Ring) (f : a $-> b),
(fun (GH : Ring) (f0 : G $-> H) => IsEquiv f0) a b f ->
RingIsomorphism a b
exact Build_RingIsomorphism.
forallab : Ring, RingIsomorphism a b -> b $-> a
intros G H; exact rng_iso_inverse.
forall (ab : Ring) (f : RingIsomorphism a b),
(fun (GH : Ring) (f0 : G $-> H) => IsEquiv f0) a b
((fun (GH : Ring) (f0 : RingIsomorphism G H) =>
rng_iso_homo f0) a b f)
cbn; exact _.
forall (ab : Ring) (f : a $-> b)
(fe : (fun (GH : Ring) (f0 : G $-> H) => IsEquiv f0)
a b f),
(fun (GH : Ring) (f0 : RingIsomorphism G H) =>
rng_iso_homo f0) a b
{| rng_iso_homo := f; isequiv_rng_iso_homo := fe |} $==
f
reflexivity.
forall (ab : Ring) (f : RingIsomorphism a b),
(fun (GH : Ring) (x : RingIsomorphism G H) =>
rng_iso_homo (rng_iso_inverse x)) a b f $o
(fun (GH : Ring) (f0 : RingIsomorphism G H) =>
rng_iso_homo f0) a b f $== Id a
intros ????; apply eissect.
forall (ab : Ring) (f : RingIsomorphism a b),
(fun (GH : Ring) (f0 : RingIsomorphism G H) =>
rng_iso_homo f0) a b f $o
(fun (GH : Ring) (x : RingIsomorphism G H) =>
rng_iso_homo (rng_iso_inverse x)) a b f $== Id b
intros ????; apply eisretr.
forall (ab : Ring) (f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a ->
(fun (GH : Ring) (f0 : G $-> H) => IsEquiv f0) a b f
G, H: Ring f: G $-> H g: H $-> G p: f $o g $== Id H q: g $o f $== Id G
(fun (GH : Ring) (f : G $-> H) => IsEquiv f) G H f
exact (isequiv_adjointify f g p q).Defined.(** ** Product ring *)
R, S: Ring f: R $-> S proj1: S proj2: grp_image f proj1 proj0: S proj3: grp_image f proj0 proj4: S proj5: grp_image f proj4
proj1 * (proj0 * proj4) = proj1 * proj0 * proj4
R, S: Ring f: R $-> S proj1: S proj2: grp_image f proj1
1 * proj1 = proj1
R, S: Ring f: R $-> S proj1: S proj2: grp_image f proj1
proj1 * 1 = proj1
R, S: Ring f: R $-> S proj1: S proj2: grp_image f proj1 proj0: S proj3: grp_image f proj0 proj4: S proj5: grp_image f proj4
proj1 * (proj0 * proj4) = proj1 * proj0 * proj4
R, S: Ring f: R $-> S proj1: S proj2: grp_image f proj1
1 * proj1 = proj1
R, S: Ring f: R $-> S proj1: S proj2: grp_image f proj1
proj1 * 1 = proj1
R, S: Ring f: R $-> S proj1: S proj2: grp_image f proj1
1 * proj1 = proj1
R, S: Ring f: R $-> S proj1: S proj2: grp_image f proj1
proj1 * 1 = proj1
R, S: Ring f: R $-> S proj1: S proj2: grp_image f proj1
proj1 * 1 = proj1
apply right_identity.Defined.
R, S: Ring f: RingHomomorphism R S
rng_image f $-> S
R, S: Ring f: RingHomomorphism R S
rng_image f $-> S
R, S: Ring f: RingHomomorphism R S
rng_image f -> S
R, S: Ring f: RingHomomorphism R S
IsSemiRingPreserving ?rng_homo_map
R, S: Ring f: RingHomomorphism R S
IsSemiRingPreserving pr1
repeatsplit.Defined.(** Image of a surjective ring homomorphism *)
R, S: Ring f: RingHomomorphism R S issurj: IsConnMap (Tr (-1)) f
rng_image f ≅ S
R, S: Ring f: RingHomomorphism R S issurj: IsConnMap (Tr (-1)) f
rng_image f ≅ S
R, S: Ring f: RingHomomorphism R S issurj: IsConnMap (Tr (-1)) f
RingHomomorphism (rng_image f) S
R, S: Ring f: RingHomomorphism R S issurj: IsConnMap (Tr (-1)) f
IsEquiv ?rng_iso_homo
R, S: Ring f: RingHomomorphism R S issurj: IsConnMap (Tr (-1)) f
IsEquiv (rng_homo_image_incl f)
exact _.Defined.(** ** Opposite Ring *)(** Given a ring [R] we can reverse the order of the multiplication to get another ring [R^op]. *)
Ring -> Ring
Ring -> Ring
(** Let's carefully pull apart the ring structure and put it back together. Unfortunately, our definition of ring has some redundant data such as multiple hset assumptions, due to the mixing of algebraic strucutres. This isn't a problem in practice, but it does mean using typeclass inference here will pick up the wrong instance, therefore we carefully put it back together. See test/Algebra/Rings/Ring.v for a test checking this operation is definitionally involutive. *)
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
Ring
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
AbGroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
Mult ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
One ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
IsRing ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
forallzyx : ?ring_abgroup, x * y * z = x * (y * z)
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
AbGroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
Mult ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
One ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
IsAbGroup ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
IsMonoid ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
LeftDistribute canonical_names.mult plus
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
RightDistribute canonical_names.mult plus
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
forallzyx : ?ring_abgroup, x * y * z = x * (y * z)
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
AbGroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
Mult ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
One ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
IsAbGroup ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
IsSemiGroup ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
LeftIdentity sg_op mon_unit
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
RightIdentity sg_op mon_unit
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
LeftDistribute canonical_names.mult plus
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
RightDistribute canonical_names.mult plus
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
forallzyx : ?ring_abgroup, x * y * z = x * (y * z)
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
AbGroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
Mult ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
One ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
IsAbGroup ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
IsHSet ?ring_abgroup
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
Associative sg_op
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
LeftIdentity sg_op mon_unit
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
RightIdentity sg_op mon_unit
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
LeftDistribute canonical_names.mult plus
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
RightDistribute canonical_names.mult plus
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
forallzyx : ?ring_abgroup, x * y * z = x * (y * z)
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
AbGroup
exact R.
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
Mult R
exact (funxy => mult y x).
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
One R
exact one.
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
IsAbGroup R
exact is_abgroup.
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
IsHSet R
exact monoid_ishset.
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
Associative sg_op
exact mult_assoc_opp.
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
LeftIdentity sg_op mon_unit
exact ri.
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
RightIdentity sg_op mon_unit
exact li.
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
LeftDistribute canonical_names.mult plus
exact (funxyz => rd y z x).
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
RightDistribute canonical_names.mult plus
exact (funxyz => ld z x y).
R: AbGroup mult: Mult R one: One R is_abgroup: IsAbGroup R monoid_ishset: IsHSet R mult_assoc: Associative sg_op li: LeftIdentity sg_op mon_unit ri: RightIdentity sg_op mon_unit ld: LeftDistribute canonical_names.mult plus rd: RightDistribute canonical_names.mult plus mult_assoc_opp: forallzyx : R,
x * y * z = x * (y * z)
forallzyx : R, x * y * z = x * (y * z)
exact mult_assoc.Defined.(** The opposite ring is a functor. *)
Is0Functor rng_op
Is0Functor rng_op
forallab : Ring, (a $-> b) -> rng_op a $-> rng_op b
R, S: Ring f: R $-> S
rng_op R $-> rng_op S
R, S: Ring f: R $-> S
GroupHomomorphism (rng_op R) (rng_op S)
R, S: Ring f: R $-> S
IsMonoidPreserving ?map
R, S: Ring f: R $-> S
GroupHomomorphism (rng_op R) (rng_op S)
exact f.
R, S: Ring f: R $-> S
IsMonoidPreserving f
R, S: Ring f: R $-> S
IsSemiGroupPreserving f
R, S: Ring f: R $-> S
IsUnitPreserving f
R, S: Ring f: R $-> S
IsSemiGroupPreserving f
exact (funxy => rng_homo_mult f y x).
R, S: Ring f: R $-> S
IsUnitPreserving f
exact (rng_homo_one f).Defined.
Is1Functor rng_op
Is1Functor rng_op
forall (ab : Ring) (fg : a $-> b),
f $== g -> fmap rng_op f $== fmap rng_op g
foralla : Ring, fmap rng_op (Id a) $== Id (rng_op a)
forall (abc : Ring) (f : a $-> b) (g : b $-> c),
fmap rng_op (g $o f) $==
fmap rng_op g $o fmap rng_op f
forall (ab : Ring) (fg : a $-> b),
f $== g -> fmap rng_op f $== fmap rng_op g
R, S: Ring f, g: R $-> S p: f $== g
fmap rng_op f $== fmap rng_op g
exact p.
foralla : Ring, fmap rng_op (Id a) $== Id (rng_op a)
intros R; cbn; reflexivity.
forall (abc : Ring) (f : a $-> b) (g : b $-> c),
fmap rng_op (g $o f) $==
fmap rng_op g $o fmap rng_op f
intros R S T f g; cbn; reflexivity.Defined.(** ** More Ring laws *)(** Powers of ring elements *)Definitionrng_power {R : Ring} (x : R) (n : nat) : R := nat_iter n (x *.) ring_one.(** Power laws *)
R: Ring x: R n, m: nat
rng_power x n * rng_power x m = rng_power x (n + m)
R: Ring x: R n, m: nat
rng_power x n * rng_power x m = rng_power x (n + m)
R: Ring x: R m: nat
rng_power x 0 * rng_power x m = rng_power x (0 + m)
R: Ring x: R n, m: nat IHn: rng_power x n * rng_power x m = rng_power x (n + m)
rng_power x n.+1 * rng_power x m =
rng_power x (n.+1 + m)
R: Ring x: R n, m: nat IHn: rng_power x n * rng_power x m = rng_power x (n + m)
rng_power x n.+1 * rng_power x m =
rng_power x (n.+1 + m)
R: Ring x: R n, m: nat IHn: rng_power x n * rng_power x m = rng_power x (n + m)
x * (nat_iter n (mult x) ring_one * rng_power x m) =
rng_power x (n.+1 + m)