CoRN.old.twoelemmonoid
Require Export CMonoids.
Require Export twoelemsemigroup.
Require Export Nm_to_cycm.
Section p68E1b1.
Definition M1_is_CMonoid:(is_CMonoid M1_as_CSemiGroup e1):=
(Build_is_CMonoid M1_as_CSemiGroup e1 e1_is_rht_unit e1_is_lft_unit).
Definition M1_as_CMonoid:CMonoid:=
(Build_CMonoid M1_as_CSemiGroup e1 M1_is_CMonoid).
Definition M2_is_CMonoid :=
(Build_is_CMonoid M2_as_CSemiGroup e1 e1_is_rht_unit_M2 e1_is_lft_unit_M2).
Definition M2_as_CMonoid:CMonoid:=
(Build_CMonoid M2_as_CSemiGroup e1 M2_is_CMonoid).
Lemma two_element_CMonoids:
∀ (op :(CSetoid_bin_fun M1_as_CSetoid M1_as_CSetoid M1_as_CSetoid))
(H: (is_CSemiGroup M1_as_CSetoid op)),
(is_unit (Build_CSemiGroup M1_as_CSetoid op H) e1)->
(∀ (x y:M1_as_CSetoid),(op x y)= (M1_mult_as_bin_fun x y)) or
(∀ (x y:M1_as_CSetoid), (op x y)= (M2_mult_as_bin_fun x y)).
Proof.
intros op H unit0.
cut (((op u u)=e1) or ((op u u)= u)).
intro H0.
unfold is_unit in unit0.
simpl in unit0.
elim H0.
clear H0.
intro H0.
left.
simpl.
intros x y.
unfold M1_CS_mult.
case x.
case y.
simpl.
set (unit1:= (unit0 e1)).
unfold M1_eq in unit1.
intuition.
simpl.
set (unit1:= (unit0 u)).
unfold M1_eq in unit1.
intuition.
case y.
simpl.
set (unit1:= (unit0 u)).
unfold M1_eq in unit1.
intuition.
simpl.
exact H0.
clear H0.
intro H0.
right.
simpl.
intros x y.
unfold M1_CS_mult.
case x.
case y.
simpl.
set (unit1:= (unit0 e1)).
unfold M1_eq in unit1.
intuition.
simpl.
set (unit1:= (unit0 u)).
unfold M1_eq in unit1.
intuition.
case y.
simpl.
set (unit1:= (unit0 u)).
unfold M1_eq in unit1.
intuition.
simpl.
exact H0.
apply (M1_eq_dec (op u u)).
Qed.
End p68E1b1.
Section p69E1.
Let PM1M2:=(direct_product_as_CMonoid M1_as_CMonoid M2_as_CMonoid).
Let uu: PM1M2.
Proof.
simpl.
exact (pairT u u).
Defined.
Let e1u: PM1M2.
Proof.
simpl.
exact (pairT e1 u).
Defined.
Lemma ex_69 : uu [+] uu [=]e1u.
Proof.
simpl.
unfold M1_eq.
intuition.
Qed.
End p69E1.
Section p71E1_.
Lemma M1_is_generated_by_u: (∀(m:M1_as_CMonoid),
{n:nat | (@power_CMonoid M1_as_CMonoid u n)[=]m}):CProp.
Proof.
simpl.
intro m.
induction m.
∃ 0.
simpl.
set (H:= (eq_reflexive M1_as_CSetoid e1)).
intuition.
∃ 1.
simpl.
set (H:= (eq_reflexive M1_as_CSetoid u)).
intuition.
Qed.
Lemma not_injective_f:
Not(injective (f_as_CSetoid_fun M1_as_CMonoid u M1_is_generated_by_u)).
Proof.
red.
unfold injective.
simpl.
intro H.
set (H3:=(H 0 2)).
cut (0 {#N} 2).
intro H4.
set (H5:= (H3 H4)).
set (H6:=(ap_imp_neq _ (@power_CMonoid M1_as_CMonoid u 0) (@power_CMonoid M1_as_CMonoid u 2) H5)).
unfold cs_neq in H6.
simpl in H6.
apply H6.
set (H7:= (eq_reflexive_unfolded M1_as_CMonoid e1)).
intuition.
unfold ap_nat.
unfold CNot.
intro H4.
cut False.
intuition.
intuition.
Qed.
End p71E1_.
Section p71E2b1.
Lemma not_isomorphic_M1_M2: Not (isomorphic M1_as_CMonoid M2_as_CMonoid).
Proof.
unfold Not.
unfold isomorphic.
simpl.
unfold isomorphism.
unfold morphism.
simpl.
intro H.
elim H.
clear H.
intros f H.
elim H.
clear H.
intros H H0.
elim H.
clear H.
intros H H2.
unfold bijective in H0.
elim H0.
clear H0.
intros H0 H3.
unfold surjective in H3.
simpl in H3.
elim (H3 u).
intros x H4.
cut (M1_eq (f u) u).
intros H5.
set (H1:= not_M1_eq_e1_u).
unfold Not in H1.
apply H1.
unfold M1_eq in H, H2, H5 |- ×.
set (H6:=(H2 u u)).
simpl in H6.
rewrite → H in H6.
rewrite → H5 in H6.
simpl in H6.
exact H6.
unfold M1_eq in H, H4 |- ×.
set (H1:= (M1_eq_dec x)).
unfold M1_eq in H1.
elim H1.
intro H5.
rewrite H5 in H4.
rewrite H4 in H.
set (H6:= not_M1_eq_e1_u).
unfold Not in H6.
unfold M1_eq in H6.
elim H6.
cut (u=e1).
intuition.
exact H.
intro H5.
rewrite H5 in H4.
exact H4.
Qed.
End p71E2b1.