Record is_CMonoid (M : CSemiGroup) (0 : M) : Prop :=
{runit : is_rht_unit (csg_op (c:=M)) 0;
lunit : is_lft_unit (csg_op (c:=M)) 0}.
Record CMonoid : Type :=
{cm_crr :> CSemiGroup;
cm_unit : cm_crr;
cm_proof : is_CMonoid cm_crr cm_unit}.
In the names of lemmas, we will denote 0 with zero.
We denote [#] 0 in the names of lemmas by ap_zero
(and not, e.g. nonzero).
The predicate "non-zero" is defined.
In lemmas we will continue to write x [#] 0, rather than
(nonZeroP x), but the predicate is useful for some high-level definitions,
e.g. for the setoid of non-zeros.
Section CMonoid_axioms.
Variable M : CMonoid.
Lemma CMonoid_is_CMonoid : is_CMonoid M (cm_unit M).
Lemma cm_rht_unit : is_rht_unit csg_op (0:M).
Lemma cm_lft_unit : is_lft_unit csg_op (0:M).
End CMonoid_axioms.
Variable M : CMonoid.
Lemma CMonoid_is_CMonoid : is_CMonoid M (cm_unit M).
Lemma cm_rht_unit : is_rht_unit csg_op (0:M).
Lemma cm_lft_unit : is_lft_unit csg_op (0:M).
End CMonoid_axioms.
Section CMonoid_basics.
Variable M : CMonoid.
Lemma cm_rht_unit_unfolded : forall x : M, x[+]0 [=] x.
Lemma cm_lft_unit_unfolded : forall x : M, 0[+]x [=] x.
Lemma cm_unit_unique_lft : forall x : M, is_lft_unit csg_op x -> x [=] 0.
Lemma cm_unit_unique_rht : forall x : M, is_rht_unit csg_op x -> x [=] 0.
Variable M : CMonoid.
Lemma cm_rht_unit_unfolded : forall x : M, x[+]0 [=] x.
Lemma cm_lft_unit_unfolded : forall x : M, 0[+]x [=] x.
Lemma cm_unit_unique_lft : forall x : M, is_lft_unit csg_op x -> x [=] 0.
Lemma cm_unit_unique_rht : forall x : M, is_rht_unit csg_op x -> x [=] 0.
The proof component of the monoid is irrelevant.
Lemma is_CMonoid_proof_irr : forall (S:CSetoid) (0:S) (plus : CSetoid_bin_op S)
(p q : associative plus), is_CMonoid (Build_CSemiGroup S plus p) 0 ->
is_CMonoid (Build_CSemiGroup S plus q) 0.
Section SubCMonoids.
Variable P : M -> CProp.
Variable Punit : P 0.
Variable op_pres_P : bin_op_pres_pred _ P csg_op.
Let subcrr : CSemiGroup := Build_SubCSemiGroup _ _ op_pres_P.
Lemma ismon_scrr : is_CMonoid subcrr (Build_subcsetoid_crr _ _ _ Punit).
Definition Build_SubCMonoid : CMonoid := Build_CMonoid subcrr _ ismon_scrr.
End SubCMonoids.
End CMonoid_basics.
Section Th13.
Variable M1:CMonoid.
Variable M2:CMonoid.
Definition morphism (f:(CSetoid_fun M1 M2)):CProp:=
(f (0)[=]0 /\ forall (a b:M1), (f (a[+]b))[=] (f a)[+](f b)).
Definition isomorphism (f:(CSetoid_fun M1 M2)):CProp:=
(morphism f) and (bijective f).
End Th13.
Section p71E2b1.
Definition isomorphic (M:CMonoid)(M':CMonoid): CProp:=
{f:(CSetoid_fun M M')|(isomorphism M M' f)}.
End p71E2b1.
Section Th14.
Variable M2:CMonoid.
Definition morphism (f:(CSetoid_fun M1 M2)):CProp:=
(f (0)[=]0 /\ forall (a b:M1), (f (a[+]b))[=] (f a)[+](f b)).
Definition isomorphism (f:(CSetoid_fun M1 M2)):CProp:=
(morphism f) and (bijective f).
End Th13.
Section p71E2b1.
Definition isomorphic (M:CMonoid)(M':CMonoid): CProp:=
{f:(CSetoid_fun M M')|(isomorphism M M' f)}.
End p71E2b1.
Section Th14.
Let f:(CSetoid_fun M1 M2) and isof: (isomorphism M1 M2 f).
Variable M1: CMonoid.
Variable M2: CMonoid.
Variable f: (CSetoid_fun M1 M2).
Variable isof: (isomorphism M1 M2 f).
Lemma iso_imp_bij: (bijective f).
Lemma iso_inv: (isomorphism M2 M1 (Inv f (iso_imp_bij))).
End Th14.
Section p71R2.
Variable M:CMonoid.
Definition automorphism:= (isomorphism M M).
End p71R2.
Section p71E1.
Variable M:CMonoid.
Variable c:M.
Fixpoint power_CMonoid (m:M)(n:nat){struct n}:M:=
match n with
|0 => (cm_unit M)
|(S p) => m [+] (power_CMonoid m p)
end.
End p71E1.
Lemma power_plus:forall (M:CMonoid)(a:M)(m n:nat),
(power_CMonoid a (m+n))[=]
(power_CMonoid a m)[+](power_CMonoid a n).
Definition is_generator (M:CMonoid)(u:M):CProp:=
forall (m:M),{n:nat | (power_CMonoid u n)[=]m}.
Definition cyclic : CMonoid -> CProp :=
fun M =>
{u:M | (forall (m:M),{n:nat | (power_CMonoid u n)[=]m}):CProp}.
Section gen_cyc.
Lemma power_k:forall (M:CMonoid)(u:M)(k l s:nat),(is_generator M u)->
((k<l and
(power_CMonoid u k [=] power_CMonoid u l)
and ((forall (k0 l0:nat), (k0<>l0 and (k0<k or (k0=k and l0<l)))->
(power_CMonoid u k0 [#] power_CMonoid u l0)))):CProp)->
(power_CMonoid u k)[=](power_CMonoid u (k+(s*(l-k)))).
Lemma power_k_n:forall (M:CMonoid)(u:M)(k l n :nat)
(H2:((Z_of_nat (l-k)>0)%Z)),(is_generator M u)->(k<n)->
((k<l and
(power_CMonoid u k [=] power_CMonoid u l)
and ((forall (k0 l0:nat), (k0<> l0 and (k0<k or (k0=k and l0<l)))->
(power_CMonoid u k0 [#] power_CMonoid u l0)))):CProp)->
(power_CMonoid u n)[=](power_CMonoid u (k+(mod_nat (n-k) (l-k) H2))).
Lemma cyc_imp_comm: forall (M:CMonoid)(H:(cyclic M)), (commutes (@csg_op M)).
Lemma weakly_inj1:
forall (M:CMonoid)(u:M)(k l a b:nat),(is_generator M u)->(a<l)->(b<l)->
(k<l and (power_CMonoid u k [=] power_CMonoid u l)
and (forall (k0 l0:nat),k0<>l0 and (k0<k or (k0=k and l0<l))->
(power_CMonoid u k0 [#] power_CMonoid u l0)))->
(power_CMonoid u a)[=](power_CMonoid u b) ->
a=b.
Let M:CMonoid.
Variable M:CMonoid.
Lemma generator_imp_cyclic: (forall (u:M),
(is_generator M u)-> (cyclic M)):CProp.
End gen_cyc.
Definition is_inverse S (op : CSetoid_bin_op S) 0 x x_inv : Prop :=
op x x_inv [=] 0 /\ op x_inv x [=] 0.
Definition invertible (M:CMonoid): M -> CProp :=
fun m =>{inv: (CSetoid_un_op M) | (is_inverse csg_op (@cm_unit M) m (inv m))}.
Section D9M.
Variable M1 M2: CMonoid.
Lemma e1e2_is_rht_unit:
(is_rht_unit (dprod_as_csb_fun M1 M2)(pairT (@cm_unit M1)(@cm_unit M2))).
Lemma e1e2_is_lft_unit:
(is_lft_unit (dprod_as_csb_fun M1 M2)(pairT (@cm_unit M1)(@cm_unit M2))).
Definition direct_product_is_CMonoid:=
(Build_is_CMonoid (direct_product_as_CSemiGroup M1 M2)
(pairT (@cm_unit M1)(@cm_unit M2))
e1e2_is_rht_unit e1e2_is_lft_unit).
Definition direct_product_as_CMonoid :=
(Build_CMonoid (direct_product_as_CSemiGroup M1 M2)
(pairT (@cm_unit M1)(@cm_unit M2)) direct_product_is_CMonoid).
End D9M.
Section p71E2b2.
Variable M1:CMonoid.
Variable M2:CMonoid.
Let f: (direct_product_as_CMonoid M1 M2)->
(direct_product_as_CMonoid M2 M1).
Defined.
Lemma f_strext': (fun_strext f ).
Definition f_as_CSetoid_fun_:= (Build_CSetoid_fun _ _ f f_strext').
Lemma isomorphic_PM1M2_PM2M1:
(isomorphic (direct_product_as_CMonoid M1 M2)
(direct_product_as_CMonoid M2 M1)):CProp.
End p71E2b2.
Definition FS_id (A : CSetoid) : FS_as_CSetoid A A.
Defined.
Lemma id_is_rht_unit :
forall A : CSetoid, is_rht_unit (comp_as_bin_op A) (FS_id A).
Lemma id_is_lft_unit :
forall A : CSetoid, is_lft_unit (comp_as_bin_op A) (FS_id A).
Definition FS_is_CMonoid (A : CSetoid) :=
Build_is_CMonoid (FS_as_CSemiGroup A) (FS_id A) (
id_is_rht_unit A) (id_is_lft_unit A).
Definition FS_as_CMonoid (A : CSetoid) :=
Build_CMonoid (FS_as_CSemiGroup A) (FS_id A) (FS_is_CMonoid A).
Definition PS_as_CMonoid (A : CSetoid) :=
Build_SubCMonoid (FS_as_CMonoid A) (bijective (A:=A) (B:=A)) (
id_is_bij A) (comp_resp_bij A A A).
Lemma is_unit_Astar_empty_word: forall (A:CSetoid),
(is_unit (Astar_as_CSemiGroup A)(empty_word A)).
Section Th12.
Let A:CSetoid.
Variable A:CSetoid.
Lemma nil_is_rht_unit: (is_rht_unit (app_as_csb_fun A) (empty_word A)).
Lemma nil_is_lft_unit: (is_lft_unit (app_as_csb_fun A) (empty_word A)).
Definition free_monoid_is_CMonoid:
is_CMonoid (Astar_as_CSemiGroup A) (empty_word A):=
(Build_is_CMonoid (Astar_as_CSemiGroup A) (empty_word A)
nil_is_rht_unit nil_is_lft_unit).
Definition free_monoid_as_CMonoid:CMonoid:=
(Build_CMonoid (Astar_as_CSemiGroup A)(empty_word A) free_monoid_is_CMonoid).
End Th12.
Section p67R2.
Variable X: CSetoid.
Lemma is_unit_FS_id:(is_unit (FS_as_CSemiGroup X) (FS_id X)).
End p67R2.
Section Th11.
Intersection
The intersection of a collection of monoids is again a monoid. Let M:CMonoid, I:type, C:I->(M->CProp), Cunit: (C i 0) and op_pres_C:forall (i:I), (bin_op_pres_pred _ (C i) csg_op).Variable M:CMonoid.
Variable I:Type.
Variable C:I->(M->CProp).
Variable Cunit: forall (i:I), (C i 0).
Variable op_pres_C: forall (i:I),(bin_op_pres_pred _ (C i) csg_op).
Definition K : M -> CProp :=
(fun m => forall (i:I), (C i m)).
Lemma op_pres_K: bin_op_pres_pred (cm_crr M) K (csg_op (c:=M)).
Definition K_is_Monoid :CMonoid := (Build_SubCMonoid M K Cunit op_pres_K).
End Th11.
Section Th15.
The Monoid generated by a Subset
Let M:CMonoid and D:M->CProp.
Variable M:CMonoid.
Fixpoint cm_Sum (l: list M) {struct l}: M :=
match l with
|nil => 0
|cons a k => a [+] (cm_Sum k)
end.
Variable D : M -> CProp.
Definition Dbrack : M -> CProp :=
fun m => {l: (list M)| (forall (a:M) , member a l -> (D a)) and
(cm_Sum l)[=]m}.
Lemma Dbrack_unit: (Dbrack 0).
Lemma cm_Sum_app:
forall (k l : (list M)), (cm_Sum (app k l))[=] (cm_Sum k)[+](cm_Sum l).
Lemma op_pres_Dbrack : bin_op_pres_pred _ Dbrack csg_op.
Definition Dbrack_as_CMonoid : CMonoid :=
(Build_SubCMonoid M Dbrack Dbrack_unit op_pres_Dbrack).
End Th15.