---

Lemma: free_abmon_umap_properties
∀S:DSet. ∀M:FAbMon(S). ∀N:AbMon. ∀p:|S| ⟶ |N|.
  ((((M.umap N p) o M.inj) = p ∈ (|S| ⟶ |N|))
  ∧ (∀f:MonHom(M.mon,N). (((f o M.inj) = p ∈ (|S| ⟶ |N|)) ⇒ (f = (M.umap N p) ∈ (|M.mon| ⟶ |N|)))))

Lemma: free_abmon_umap_properties_1
∀S:DSet. ∀M:FAbMon(S). ∀N:AbMon. ∀p:|S| ⟶ |N|.  (((M.umap N p) o M.inj) = p ∈ (|S| ⟶ |N|))

Lemma: free_abmon_endomorph_is_id
∀S:DSet. ∀M:FAbMon(S). ∀f:MonHom(M.mon,M.mon).
  (((f o M.inj) = M.inj ∈ (|S| ⟶ |M.mon|)) ⇒ (f = Id{|M.mon|} ∈ (|M.mon| ⟶ |M.mon|)))

Lemma: free_abmon_unique
∀S:DSet. ∀M,N:FAbMon(S).  ∃f:MonHom(M.mon,N.mon). ∃g:MonHom(N.mon,M.mon). InvFuns(|M.mon|;|N.mon|;f;g)

Lemma: mk_fabmon
∀s:DSet. ∀g:AbMon. ∀i:|s| ⟶ |g|. ∀U:g':AbMon ⟶ (|s| ⟶ |g'|) ⟶ |g| ⟶ |g'|.
  ((∀g':AbMon. ∀f:|s| ⟶ |g'|.
      (IsMonHom{g,g'}(U g' f)
      ∧ (((U g' f) o i) = f ∈ (|s| ⟶ |g'|))
      ∧ (∀u:|g| ⟶ |g'|. (IsMonHom{g,g'}(u) ⇒ ((u o i) = f ∈ (|s| ⟶ |g'|)) ⇒ (u = (U g' f) ∈ (|g| ⟶ |g'|))))))
  ⇒ (<g, i, U> ∈ FAbMon(s)))

Definition: mcopower_sig
mcopower_sig{i:l}(s;g) ==  mon:AbMon × inj:|s| ⟶ |g| ⟶ |mon| × (h:AbMon ⟶ (|s| ⟶ |g| ⟶ |h|) ⟶ |mon| ⟶ |h|)

Lemma: mcopower_sig_wf
∀s:DSet. ∀g:AbMon.  (mcopower_sig{i:l}(s;g) ∈ 𝕌')

Definition: mcopower_mon
m.mon ==  fst(m)

Lemma: mcopower_mon_wf
∀s:DSet. ∀g:AbMon. ∀m:mcopower_sig{i:l}(s;g).  (m.mon ∈ AbMon)

Definition: mcopower_inj
m.inj ==  fst(snd(m))

Lemma: mcopower_inj_wf
∀s:DSet. ∀g:AbMon. ∀m:mcopower_sig{i:l}(s;g).  (m.inj ∈ |s| ⟶ |g| ⟶ |m.mon|)

Definition: mcopower_umap
m.umap ==  snd(snd(m))

Lemma: mcopower_umap_wf
∀s:DSet. ∀g:AbMon. ∀m:mcopower_sig{i:l}(s;g).  (m.umap ∈ h:AbMon ⟶ (|s| ⟶ |g| ⟶ |h|) ⟶ |m.mon| ⟶ |h|)

Definition: mcopower
MCopower(s;g) ==
  {c:mcopower_sig{i:l}(s;g)| 
   (∀j:|s|. IsMonHom{g,c.mon}(c.inj j))
   ∧ (∀h:AbMon. ∀f:|s| ⟶ MonHom(g,h).
        (c.umap h f) = !v:|c.mon| ⟶ |h|. (IsMonHom{c.mon,h}(v) ∧ (∀j:|s|. ((f j) = (v o (c.inj j)) ∈ (|g| ⟶ |h|)))))} 

Lemma: mcopower_wf
∀s:DSet. ∀g:AbMon.  (MCopower(s;g) ∈ 𝕌')

Lemma: mcopower_properties
∀s:DSet. ∀g:AbMon. ∀c:MCopower(s;g).
  ((∀j:|s|. IsMonHom{g,c.mon}(c.inj j))
  ∧ (∀h:AbMon. ∀f:|s| ⟶ MonHom(g,h).
       (c.umap h f) = !v:|c.mon| ⟶ |h|. (IsMonHom{c.mon,h}(v) ∧ (∀j:|s|. ((f j) = (v o (c.inj j)) ∈ (|g| ⟶ |h|))))))

Lemma: mcopower_inj_is_hom
∀s:DSet. ∀g:AbMon. ∀c:MCopower(s;g). ∀j:|s|.  IsMonHom{g,c.mon}(c.inj j)

Lemma: mcopower_umap_is_hom
∀s:DSet. ∀g:AbMon. ∀c:MCopower(s;g). ∀h:AbMon. ∀f:|s| ⟶ MonHom(g,h).  IsMonHom{c.mon,h}(c.umap h f)

Lemma: mcopower_umap_comm_tri
∀s:DSet. ∀g:AbMon. ∀c:MCopower(s;g). ∀h:AbMon. ∀f:|s| ⟶ MonHom(g,h). ∀j:|s|.
  ((f j) = ((c.umap h f) o (c.inj j)) ∈ (|g| ⟶ |h|))

Lemma: mcopower_umap_comm_tri_a
∀s:DSet. ∀g:AbMon. ∀c:MCopower(s;g). ∀h:AbMon. ∀f:|s| ⟶ MonHom(g,h). ∀a:|g|. ∀j:|s|.
  ((f j a) = (c.umap h f (c.inj j a)) ∈ |h|)

Lemma: mcopower_umap_unique
∀s:DSet. ∀g:AbMon. ∀c:MCopower(s;g). ∀h:AbMon. ∀f:|s| ⟶ MonHom(g,h). ∀a':|c.mon| ⟶ |h|.
  (IsMonHom{c.mon,h}(a')
  ⇒ (∀j:|s|. ((f j) = (a' o (c.inj j)) ∈ (|g| ⟶ |h|)))
  ⇒ (a' = (c.umap h f) ∈ (|c.mon| ⟶ |h|)))

Definition: fabmon_of_nat_mcp
fabmon_of_nat_mcp(m) ==  <m.mon, λu.(m.inj u zhgrp(1)), λm',f. (m.umap m' (λz,n. (nat(n) ⋅ (f z))))>

Lemma: fabmon_of_nat_mcp_wf
∀s:DSet. ∀m:MCopower(s;<ℤ+>↓hgrp).  (fabmon_of_nat_mcp(m) ∈ FAbMon(s))

Definition: fabgrp_sig
fabgrp_sig{i:l}(s) ==  grp:AbGrp × inj:|s| ⟶ |grp| × (grp':AbGrp ⟶ (|s| ⟶ |grp'|) ⟶ |grp| ⟶ |grp'|)

Lemma: fabgrp_sig_wf
∀s:DSet. (fabgrp_sig{i:l}(s) ∈ 𝕌')

Definition: fabgrp_grp
f.grp ==  fst(f)

Lemma: fabgrp_grp_wf
∀s:DSet. ∀f:fabgrp_sig{i:l}(s).  (f.grp ∈ AbGrp)

Definition: fabgrp_inj
f.inj ==  fst(snd(f))

Lemma: fabgrp_inj_wf
∀s:DSet. ∀f:fabgrp_sig{i:l}(s).  (f.inj ∈ |s| ⟶ |f.grp|)

Definition: fabgrp_umap
f.umap ==  snd(snd(f))

Lemma: fabgrp_umap_wf
∀s:DSet. ∀f:fabgrp_sig{i:l}(s).  (f.umap ∈ grp':AbGrp ⟶ (|s| ⟶ |grp'|) ⟶ |f.grp| ⟶ |grp'|)

Definition: fabgrp
FAbGrp(s) ==
  {fg:fabgrp_sig{i:l}(s)| 
   ∀g:AbGrp. ∀h:|s| ⟶ |g|.
     (fg.umap g h) = !h':|fg.grp| ⟶ |g|. (IsMonHom{fg.grp,g}(h') ∧ ((h' o fg.inj) = h ∈ (|s| ⟶ |g|)))} 

Lemma: fabgrp_wf
∀s:DSet. (FAbGrp(s) ∈ 𝕌')

Definition: gcopower_sig
gcopower_sig{i:l}(s;g) ==  grp:GrpSig × inj:|s| ⟶ |g| ⟶ |grp| × (h:AbGrp ⟶ (|s| ⟶ |g| ⟶ |h|) ⟶ |grp| ⟶ |h|)

Lemma: gcopower_sig_wf
∀s:PosetSig. ∀g:GrpSig.  (gcopower_sig{i:l}(s;g) ∈ 𝕌')

Definition: gcopower_grp
g1.grp ==  fst(g1)

Lemma: gcopower_grp_wf
∀s:PosetSig. ∀g:GrpSig. ∀g1:gcopower_sig{i:l}(s;g).  (g1.grp ∈ GrpSig)

Definition: gcopower_inj
g1.inj ==  fst(snd(g1))

Lemma: gcopower_inj_wf
∀s:PosetSig. ∀g:GrpSig. ∀g1:gcopower_sig{i:l}(s;g).  (g1.inj ∈ |s| ⟶ |g| ⟶ |g1.grp|)

Definition: gcopower_umap
g1.umap ==  snd(snd(g1))

Lemma: gcopower_umap_wf
∀s:PosetSig. ∀g:GrpSig. ∀g1:gcopower_sig{i:l}(s;g).  (g1.umap ∈ h:AbGrp ⟶ (|s| ⟶ |g| ⟶ |h|) ⟶ |g1.grp| ⟶ |h|)

Definition: mon_p
mon_p(g) ==  IsMonoid(|g|;*;e)

Lemma: mon_p_wf
∀g:GrpSig. (mon_p(g) ∈ ℙ)

Definition: grp_p
grp_p(g) ==  IsGroup(|g|;*;e;~)

Lemma: grp_p_wf
∀g:GrpSig. (grp_p(g) ∈ ℙ)

Definition: rng_p
rng_p(r) ==  grp_p(r↓+gp) ∧ mon_p(r↓xmn) ∧ BiLinear(|r|;+r;*)

Lemma: rng_p_wf
∀r:RngSig. (rng_p(r) ∈ ℙ)

Definition: alg_p
AlgP(r;a) ==
  rng_p(a↓rg)
  ∧ IsAction(|r|;*;1;a.car;a.act)
  ∧ IsBilinear(|r|;a.car;a.car;+r;a.plus;a.plus;a.act)
  ∧ (∀p:|r|. Dist1op2opLR(a.car;a.act p;a.times))

Lemma: alg_p_wf
∀r:RngSig. ∀a:algebra_sig{i:l}(|r|).  (AlgP(r;a) ∈ ℙ)

Definition: gcopower
gcopower{i}(s;g) ==
  {c:gcopower_sig{i:l}(s;g)| 
   IsEqFun(|c.grp|;=b)
   ∧ grp_p(c.grp)
   ∧ Comm(|c.grp|;*)
   ∧ (∀j:|s|. IsMonHom{g,c.grp}(c.inj j))
   ∧ (∀h:AbGrp. ∀f:|s| ⟶ MonHom(g,h).
        (c.umap h f) = !v:|c.grp| ⟶ |h|. (IsMonHom{c.grp,h}(v) ∧ (∀j:|s|. ((f j) = (v o (c.inj j)) ∈ (|g| ⟶ |h|)))))} 

Lemma: gcopower_wf
∀s:DSet. ∀g:AbGrp.  (gcopower{i}(s;g) ∈ 𝕌')

Lemma: gcopower_properties
∀s:DSet. ∀g:AbGrp. ∀c:gcopower{i}(s;g).
  (IsEqFun(|c.grp|;=b)
  ∧ grp_p(c.grp)
  ∧ Comm(|c.grp|;*)
  ∧ (∀j:|s|. IsMonHom{g,c.grp}(c.inj j))
  ∧ (∀h:AbGrp. ∀f:|s| ⟶ MonHom(g,h).
       (c.umap h f) = !v:|c.grp| ⟶ |h|. (IsMonHom{c.grp,h}(v) ∧ (∀j:|s|. ((f j) = (v o (c.inj j)) ∈ (|g| ⟶ |h|))))))

Definition: fma_sig
fma_sig{i:l}(G;A) ==
  alg:algebra_sig{i:l}(|A|) × inj:|G| ⟶ alg.car × (N:algebra{i:l}(A) ⟶ (|G| ⟶ N.car) ⟶ alg.car ⟶ N.car)

Lemma: fma_sig_wf
∀G:GrpSig. ∀A:RngSig.  (fma_sig{i:l}(G;A) ∈ 𝕌')

Definition: fma_alg
f.alg ==  fst(f)

Lemma: fma_alg_wf
∀G:GrpSig. ∀A:RngSig. ∀f:fma_sig{i:l}(G;A).  (f.alg ∈ algebra_sig{i:l}(|A|))

Definition: fma_inj
f.inj ==  fst(snd(f))

Lemma: fma_inj_wf
∀G:GrpSig. ∀A:RngSig. ∀f:fma_sig{i:l}(G;A).  (f.inj ∈ |G| ⟶ f.alg.car)

Definition: fma_umap
f.umap ==  snd(snd(f))

Lemma: fma_umap_wf
∀G:GrpSig. ∀A:RngSig. ∀f:fma_sig{i:l}(G;A).  (f.umap ∈ N:algebra{i:l}(A) ⟶ (|G| ⟶ N.car) ⟶ f.alg.car ⟶ N.car)

Definition: fmonalg
FMonAlg(g;a) ==
  {m:fma_sig{i:l}(g;a)| 
   IsMonHom{g,m.alg↓rg↓xmn}(m.inj)
   ∧ (∀n:algebra{i:l}(a). ∀f:MonHom(g,n↓rg↓xmn).
        (m.umap n f) = !f':m.alg.car ⟶ n.car. (alg_hom_p(a; m.alg; n; f') ∧ ((f' o m.inj) = f ∈ (|g| ⟶ n.car))))} 

Lemma: fmonalg_wf
∀g:AbMon. ∀a:CRng.  (FMonAlg(g;a) ∈ 𝕌')

Lemma: fmonalg_properties
∀g:AbMon. ∀a:CRng. ∀m:FMonAlg(g;a).
  (IsMonHom{g,m.alg↓rg↓xmn}(m.inj)
  ∧ (∀n:algebra{i:l}(a). ∀f:MonHom(g,n↓rg↓xmn).
       (m.umap n f) = !f':m.alg.car ⟶ n.car. (alg_hom_p(a; m.alg; n; f') ∧ ((f' o m.inj) = f ∈ (|g| ⟶ n.car)))))

Definition: polynom_alg
polynom_alg{i:l}(S;A) ==  mo:FAbMon(S) × FMonAlg(mo.mon;A)

Lemma: polynom_alg_wf
∀S:DSet. ∀A:CRng.  (polynom_alg{i:l}(S;A) ∈ 𝕌')

Definition: polyalg_mo
p.mo ==  fst(p)

Lemma: polyalg_mo_wf
∀S:DSet. ∀A:CRng. ∀p:polynom_alg{i:l}(S;A).  (p.mo ∈ FAbMon(S))

Definition: polyalg_poly
p.poly ==  snd(p)

Lemma: polyalg_poly_wf
∀S:DSet. ∀A:CRng. ∀p:polynom_alg{i:l}(S;A).  (p.poly ∈ FMonAlg(p.mo.mon;A))

Definition: rng_from_grp
rng_from_grp(g;times;one;div) ==  <|g|, =b, ≤b, *, e, ~, times, one, div>

Lemma: rng_from_grp_wf
∀g:GrpSig. ∀times:|g| ⟶ |g| ⟶ |g|. ∀one:|g|. ∀div:|g| ⟶ |g| ⟶ (|g|?).  (rng_from_grp(g;times;one;div) ∈ RngSig)

Definition: alg_from_rng
alg_from_rng(A;r;act) ==  <|r|, =b, ≤b, +r, 0, -r, *, 1, ÷r, act>

Lemma: alg_from_rng_wf
∀A:Type. ∀r:RngSig. ∀act:A ⟶ |r| ⟶ |r|.  (alg_from_rng(A;r;act) ∈ algebra_sig{i:l}(A))

Definition: fma_from_gcp
fma_from_gcp(g;r;c;a) ==  <a, λp:|g|. c.inj p 1, λa.(λh:|g| ⟶ a.car. c.umap (a↓grp) (λp:|g|. λv:|r|. a.act v (h p)))>

Lemma: fma_from_gcp_wf
∀g:GrpSig. ∀r:RngSig. ∀c:gcopower_sig{i:l}(g↓set;r↓+gp). ∀a:algebra{i:l}(r).
  (((a↓grp) = c.grp ∈ GrpSig) ⇒ (fma_from_gcp(g;r;c;a) ∈ fma_sig{i:l}(g;r)))



Home Index