---

Definition: algebra_sig
algebra_sig{i:l}(A) ==
  car:Type
  × eq:car ⟶ car ⟶ 𝔹
  × le:car ⟶ car ⟶ 𝔹
  × plus:car ⟶ car ⟶ car
  × zero:car
  × minus:car ⟶ car
  × times:car ⟶ car ⟶ car
  × one:car
  × div:car ⟶ car ⟶ (car?)
  × (A ⟶ car ⟶ car)

Lemma: algebra_sig_wf
∀A:Type. (algebra_sig{i:l}(A) ∈ 𝕌')

Definition: alg_car
a.car ==  fst(a)

Lemma: alg_car_wf
∀A:Type. ∀a:algebra_sig{i:l}(A).  (a.car ∈ Type)

Definition: alg_eq
a.eq ==  fst(snd(a))

Lemma: alg_eq_wf
∀A:Type. ∀a:algebra_sig{i:l}(A).  (a.eq ∈ a.car ⟶ a.car ⟶ 𝔹)

Definition: alg_le
a.le ==  fst(snd(snd(a)))

Lemma: alg_le_wf
∀A:Type. ∀a:algebra_sig{i:l}(A).  (a.le ∈ a.car ⟶ a.car ⟶ 𝔹)

Definition: alg_plus
a.plus ==  fst(snd(snd(snd(a))))

Lemma: alg_plus_wf
∀A:Type. ∀a:algebra_sig{i:l}(A).  (a.plus ∈ a.car ⟶ a.car ⟶ a.car)

Definition: alg_zero
a.zero ==  fst(snd(snd(snd(snd(a)))))

Lemma: alg_zero_wf
∀A:Type. ∀a:algebra_sig{i:l}(A).  (a.zero ∈ a.car)

Definition: alg_minus
a.minus ==  fst(snd(snd(snd(snd(snd(a))))))

Lemma: alg_minus_wf
∀A:Type. ∀a:algebra_sig{i:l}(A).  (a.minus ∈ a.car ⟶ a.car)

Definition: alg_times
a.times ==  fst(snd(snd(snd(snd(snd(snd(a)))))))

Lemma: alg_times_wf
∀A:Type. ∀a:algebra_sig{i:l}(A).  (a.times ∈ a.car ⟶ a.car ⟶ a.car)

Definition: alg_one
a.one ==  fst(snd(snd(snd(snd(snd(snd(snd(a))))))))

Lemma: alg_one_wf
∀A:Type. ∀a:algebra_sig{i:l}(A).  (a.one ∈ a.car)

Definition: alg_div
a.div ==  fst(snd(snd(snd(snd(snd(snd(snd(snd(a)))))))))

Lemma: alg_div_wf
∀A:Type. ∀a:algebra_sig{i:l}(A).  (a.div ∈ a.car ⟶ a.car ⟶ (a.car?))

Definition: alg_act
a.act ==  snd(snd(snd(snd(snd(snd(snd(snd(snd(a)))))))))

Lemma: alg_act_wf
∀A:Type. ∀a:algebra_sig{i:l}(A).  (a.act ∈ A ⟶ a.car ⟶ a.car)

Lemma: subtype_rel_algebra
∀A1,A2:Type.  ((A1 ⊆r A2) ⇒ (algebra_sig{i:l}(A2) ⊆r algebra_sig{[i | j]:l}(A1)))

Lemma: algebra_sig_inc
∀A:Type. (algebra_sig{i:l}(A) ⊆r algebra_sig{[i | j]:l}(A))

Definition: rng_of_alg
a↓rg ==  <a.car, a.eq, a.le, a.plus, a.zero, a.minus, a.times, a.one, a.div>

Lemma: rng_of_alg_wf
∀A:Type. ∀a:algebra_sig{i:l}(A).  (a↓rg ∈ RngSig)

Definition: grp_of_module
m↓grp ==  m↓rg↓+gp

Lemma: grp_of_module_wf
∀A:Type. ∀m:algebra_sig{i:l}(A).  (m↓grp ∈ GrpSig)

Definition: module
A-Module ==
  {m:algebra_sig{i:l}(|A|)| 
   IsGroup(m.car;m.plus;m.zero;m.minus)
   ∧ Comm(m.car;m.plus)
   ∧ IsAction(|A|;*;1;m.car;m.act)
   ∧ IsBilinear(|A|;m.car;m.car;+A;m.plus;m.plus;m.act)} 

Definition: dmodule
A-DModule ==  {m:A-Module| IsEqFun(m.car;m.eq)} 

Lemma: module_wf
∀A:RngSig. (A-Module ∈ 𝕌')

Lemma: dmodule_wf
∀A:RngSig. (A-DModule ∈ 𝕌')

Lemma: module_properties
∀A:RngSig. ∀m:A-Module.
  (IsGroup(m.car;m.plus;m.zero;m.minus)
  ∧ Comm(m.car;m.plus)
  ∧ IsAction(|A|;*;1;m.car;m.act)
  ∧ IsBilinear(|A|;m.car;m.car;+A;m.plus;m.plus;m.act))

Lemma: module_plus_assoc
∀[A:Rng]. ∀[m:A-Module]. ∀[x,y,z:m.car].  ((x m.plus (y m.plus z)) = ((x m.plus y) m.plus z) ∈ m.car)

Lemma: module_plus_ident
∀[A:Rng]. ∀[m:A-Module]. ∀[x:m.car].  (((x m.plus m.zero) = x ∈ m.car) ∧ ((m.zero m.plus x) = x ∈ m.car))

Lemma: module_plus_inv
∀[A:Rng]. ∀[m:A-Module]. ∀[x:m.car].
  (((x m.plus (m.minus x)) = m.zero ∈ m.car) ∧ (((m.minus x) m.plus x) = m.zero ∈ m.car))

Lemma: module_plus_comm
∀[A:Rng]. ∀[m:A-Module]. ∀[x,y:m.car].  ((x m.plus y) = (y m.plus x) ∈ m.car)

Lemma: module_action_p
∀[A:Rng]. ∀[m:A-Module].
  ((∀[a,b:|A|]. ∀[u:m.car].  (((a * b) m.act u) = (a m.act (b m.act u)) ∈ m.car))
  ∧ (∀[u:m.car]. ((1 m.act u) = u ∈ m.car)))

Lemma: module_act_plus
∀[A:Rng]. ∀[m:A-Module].
  ((∀[a1,a2:|A|]. ∀[b:m.car].  (((a1 +A a2) m.act b) = ((a1 m.act b) m.plus (a2 m.act b)) ∈ m.car))
  ∧ (∀[a:|A|]. ∀[b1,b2:m.car].  ((a m.act (b1 m.plus b2)) = ((a m.act b1) m.plus (a m.act b2)) ∈ m.car)))

Lemma: module_eqfun_p
∀[A:Rng]. ∀[m:A-DModule]. ∀[x,y:m.car].  uiff(↑(x m.eq y);x = y ∈ m.car)

Lemma: grp_of_module_wf2
∀a:RngSig. ∀m:a-Module.  (m↓grp ∈ AbGrp)

Lemma: module_act_zero_l
∀A:Rng. ∀m:A-Module. ∀u:m.car.  ((0 m.act u) = m.zero ∈ m.car)

Lemma: module_act_zero_r
∀A:Rng. ∀m:A-Module. ∀a:|A|.  ((a m.act m.zero) = m.zero ∈ m.car)

Lemma: module_act_minus_l
∀A:Rng. ∀m:A-Module. ∀a:|A|. ∀u:m.car.  (((-A a) m.act u) = (m.minus (a m.act u)) ∈ m.car)

Lemma: module_act_minus_r
∀A:Rng. ∀m:A-Module. ∀a:|A|. ∀u:m.car.  ((a m.act (m.minus u)) = (m.minus (a m.act u)) ∈ m.car)

Lemma: module_act_is_grp_hom
∀A:Rng. ∀m:A-Module. ∀a:|A|.  IsMonHom{m↓grp,m↓grp}(m.act a)

Lemma: module_act_grp_hom_l
∀A:Rng. ∀m:A-Module. ∀u:m.car.  IsMonHom{A↓+gp,m↓grp}(λa:|A|. m.act a u)

Lemma: module_over_triv_rng
∀A:Rng. ∀m:A-Module.  ((1 = 0 ∈ |A|) ⇒ (∀u:m.car. (u = m.zero ∈ m.car)))

Definition: module_hom_p
(compound):: 
module_hom_p(a; m; n; f) ==
  FunThru2op(m.car;n.car;m.plus;n.plus;f) ∧ (∀u:|a|. fun_thru_1op(m.car;n.car;m.act u;n.act u;f))

Lemma: module_hom_p_wf
∀a:RngSig. ∀m,n:algebra_sig{i:l}(|a|). ∀f:m.car ⟶ n.car.  (module_hom_p(a; m; n; f) ∈ ℙ)

Lemma: sq_stable__module_hom_p
∀A:RngSig. ∀M,N:algebra_sig{i:l}(|A|). ∀f:M.car ⟶ N.car.  SqStable(module_hom_p(A; M; N; f))

Lemma: module_hom_is_grp_hom
∀A:Rng. ∀m,n:A-Module. ∀f:m.car ⟶ n.car.  (module_hom_p(A; m; n; f) ⇒ IsMonHom{m↓grp,n↓grp}(f))

Definition: module_hom
module_hom(A; M; N) ==  {f:M.car ⟶ N.car| module_hom_p(A; M; N; f)} 

Lemma: module_hom_wf
∀A:RngSig. ∀M,N:algebra_sig{i:l}(|A|).  (module_hom(A; M; N) ∈ Type)

Lemma: module_hom_properties
∀A:RngSig. ∀M,N:algebra_sig{i:l}(|A|). ∀f:module_hom(A; M; N).  module_hom_p(A; M; N; f)

Lemma: module_hom_plus
∀[A:RngSig]. ∀[M,N:algebra_sig{i:l}(|A|)]. ∀[f:module_hom(A; M; N)]. ∀[a1,a2:M.car].
  ((f (a1 M.plus a2)) = ((f a1) N.plus (f a2)) ∈ N.car)

Lemma: module_hom_action
∀[A:RngSig]. ∀[M,N:algebra_sig{i:l}(|A|)]. ∀[f:module_hom(A; M; N)]. ∀[u:|A|].
  ∀a:M.car. ((f (M.act u a)) = (N.act u (f a)) ∈ N.car)

Definition: algebra
algebra{i:l}(A) ==
  {m:A-Module| 
   IsMonoid(m.car;m.times;m.one) ∧ BiLinear(m.car;m.plus;m.times) ∧ (∀a:|A|. Dist1op2opLR(m.car;m.act a;m.times))} 

Lemma: algebra_wf
∀A:RngSig. (algebra{i:l}(A) ∈ 𝕌')

Lemma: algebra_subtype_algebra_sig
∀A:RngSig. (algebra{i:l}(A) ⊆r algebra_sig{i:l}(|A|))

Lemma: algebra_subtype_module
∀A:RngSig. (algebra{i:l}(A) ⊆r A-Module)

Lemma: algebra_properties
∀A:Rng. ∀m:algebra{i:l}(A).
  (IsMonoid(m.car;m.times;m.one) ∧ BiLinear(m.car;m.plus;m.times) ∧ (∀a:|A|. Dist1op2opLR(m.car;m.act a;m.times)))

Lemma: algebra_times_assoc
∀[A:Rng]. ∀[m:algebra{i:l}(A)]. ∀[x,y,z:m.car].  ((x m.times (y m.times z)) = ((x m.times y) m.times z) ∈ m.car)

Lemma: algebra_times_one
∀[A:Rng]. ∀[m:algebra{i:l}(A)]. ∀[x:m.car].  (((x m.times m.one) = x ∈ m.car) ∧ ((m.one m.times x) = x ∈ m.car))

Lemma: algebra_bilinear
∀[A:Rng]. ∀[m:algebra{i:l}(A)]. ∀[a,x,y:m.car].
  (((a m.times (x m.plus y)) = ((a m.times x) m.plus (a m.times y)) ∈ m.car)
  ∧ (((x m.plus y) m.times a) = ((x m.times a) m.plus (y m.times a)) ∈ m.car))

Lemma: algebra_act_times_r
∀[A:Rng]. ∀[m:algebra{i:l}(A)]. ∀[a:|A|]. ∀[u,v:m.car].
  (((m.act a (u m.times v)) = ((m.act a u) m.times v) ∈ m.car)
  ∧ ((m.act a (u m.times v)) = (u m.times (m.act a v)) ∈ m.car))

Lemma: algebra_act_times_lr
∀A:Rng. ∀m:algebra{i:l}(A). ∀a,b:|A|. ∀u,v:m.car.
  (((a * b) m.act (u m.times v)) = ((a m.act u) m.times (b m.act v)) ∈ m.car)

Definition: calgebra
CAlg(A) ==  {m:algebra{i:l}(A)| Comm(m.car;m.times)} 

Lemma: calgebra_wf
∀A:RngSig. (CAlg(A) ∈ 𝕌')

Lemma: calgebra_properties
∀A:Rng. ∀m:CAlg(A).  Comm(m.car;m.times)

Lemma: calgebra_times_comm
∀[A:Rng]. ∀[m:CAlg(A)]. ∀[x,y:m.car].  ((x m.times y) = (y m.times x) ∈ m.car)

Definition: rng_to_alg
rng_to_alg(r) ==  <|r|, =b, ≤b, +r, 0, -r, *, 1, ÷r, *>

Lemma: rng_to_alg_wf
∀R:CRng. (rng_to_alg(R) ∈ algebra{i:l}(R))

Definition: alg_hom_p
(compound):: 
alg_hom_p(a; m; n; f) ==
  module_hom_p(a; m; n; f) ∧ FunThru2op(m.car;n.car;m.times;n.times;f) ∧ ((f m.one) = n.one ∈ n.car)

Lemma: alg_hom_p_wf
∀a:RngSig. ∀m,n:algebra_sig{i:l}(|a|). ∀f:m.car ⟶ n.car.  (alg_hom_p(a; m; n; f) ∈ ℙ)

Lemma: sq_stable__alg_hom_p
∀a:RngSig. ∀m,n:algebra_sig{i:l}(|a|). ∀f:m.car ⟶ n.car.  SqStable(alg_hom_p(a; m; n; f))

Definition: algebra_hom
algebra_hom(A; M; N) ==
  {f:module_hom(A; M; N)| FunThru2op(M.car;N.car;M.times;N.times;f) ∧ ((f M.one) = N.one ∈ N.car)} 

Lemma: algebra_hom_wf
∀A:RngSig. ∀M,N:algebra_sig{i:l}(|A|).  (algebra_hom(A; M; N) ∈ Type)

Lemma: algebra_hom_properties
∀A:RngSig. ∀M,N:algebra_sig{i:l}(|A|). ∀f:algebra_hom(A; M; N).
  (FunThru2op(M.car;N.car;M.times;N.times;f) ∧ ((f M.one) = N.one ∈ N.car))

Lemma: rng_of_alg_wf2
∀a:CRng. ∀m:algebra{i:l}(a).  (m↓rg ∈ Rng)

Lemma: alg_act_is_rng_chom
∀a:CRng. ∀m:algebra{i:l}(a).  rng_chom_p(a;m↓rg;λx:|a|. m.act x m.one)



Home Index