namespace http://mathhub.info/MitM/core/algebra ❚
import top http://mathhub.info/MitM/interfaces❚
import base http://mathhub.info/MitM/Foundation ❚
import num http://mathhub.info/MitM/core/arithmetics ❚
import sets http://mathhub.info/MitM/core/typedsets ❚
theory OperationProps : base:?Logic =
prop_idempotent : {U : type} (U ⟶ U ⟶ U) ⟶ prop ❘ = [U,op] ∀[a] op a a ≐ a ❘ # prop_idempotent 2❙
prop_associative : {U : type} (U ⟶ U ⟶ U) ⟶ prop ❘ = [U,op] ∀[x : U]∀[y : U]∀[z : U] op x (op y z) ≐ op (op x y) z ❘ # prop_associative 2❙
prop_commutative : {U : type} (U ⟶ U ⟶ U) ⟶ prop ❘ = [U,op] ∀[x : U]∀[y] op x y ≐ op y x ❘ # prop_commutative 2❙
prop_leftUnital : {U : type} (U ⟶ U ⟶ U) ⟶ U ⟶ prop ❘ = [U,op,e] ∀[x] op e x ≐ x ❘ # prop_leftUnital 2 3 ❙
prop_rightUnital : {U : type} (U ⟶ U ⟶ U) ⟶ U ⟶ prop ❘ = [U,op,e] ∀[x] op x e ≐ x ❘ # prop_rightUnital 2 3 ❙
prop_leftCancellative : {U : type} (U ⟶ U ⟶ U) ⟶ prop ❘ = [U,op] ∀[a] ∀[b] ∀[c] op a c ≐ op b c ⇒ a ≐ b ❘ # prop_leftCancellative 2❙
prop_rightCancellative : {U : type} (U ⟶ U ⟶ U) ⟶ prop ❘ = [U,op] ∀[a] ∀[b] ∀[c] op c a ≐ op c b ⇒ a ≐ b ❘ # prop_rightCancellative 2❙
prop_inverse : {U : type} (U ⟶ U ⟶ U) ⟶ (U ⟶ U) ⟶ U ⟶ bool ❘ = [U,op,inv,e] ∀[x] op x (inv x) ≐ e ❘ # prop_inverse 2 3 4 ❙
prop_absorption : {U : type} (U ⟶ U ⟶ U) ⟶ (U ⟶ U ⟶ U) ⟶ bool ❘ = [U][m,j] ∀[a] ∀[b] m a (j a b) ≐ a ❘ # prop_absorption 2 3 ❙
prop_distributive : {U : type} (U ⟶ U ⟶ U) ⟶ (U ⟶ U ⟶ U) ⟶ bool ❘
= [U][plus,times] ∀ [x] ∀ [y] ∀ [z] (times x (plus y z)) ≐ (plus (times x y) (times x z)) ❘ # prop_distributive 2 3 ❙
❚
theory Magma : base:?Logic =
include ?OperationProps ❙
include ☞sets:?SetStructures ❙
theory magma_theory : base:?Logic =
include ☞sets:?SetStructures/setstruct_theory ❙
op : U ⟶ U ⟶ U ❘ # 1 ∘ 2 prec 19 ❙
❚
magma = Mod ☞?Magma/magma_theory ❘ role abbreviation ❙
baseset : magma ⟶ type ❘ = [m] (m.universe) ❘ # dom 1 ❙
operation : {G: magma} (G.universe ⟶ G.universe ⟶ G.universe) ❘ # 2 ∘ 3 prec 20 ❘ = [G] [a,b] (G.op) a b ❙
finite: magma ⟶ prop ❙
❚
theory SemiGroup : base:?Logic =
include ?Magma ❙
theory semigroup_theory : base:?Logic =
include ?Magma/magma_theory ❙
axiom_associative : ⊦ prop_associative op ❙
❚
semigroup = Mod ☞?SemiGroup/semigroup_theory ❙
❚
theory Unital : base:?Logic =
include ?Magma ❙
theory unital_theory : base:?Logic =
include ?Magma/magma_theory ❙
unit : U ❘ # e prec -1 ❙
axiom_leftUnital : ⊦ prop_leftUnital op e ❙
axiom_rightUnital : ⊦ prop_rightUnital op e ❙
❚
unital = Mod ☞?Unital/unital_theory ❙
unitOf : {G: unital} dom G ❘ # %I1 e prec 5 ❘ = [G] (G.unit) ❙
❚
theory QuasiGroup : base:?Logic =
include ☞base:?DescriptionOperator ❙
include ☞base:?NaturalDeduction ❙
include ?Magma ❙
theory quasigroup_theory : base:?Logic =
include ?Magma/magma_theory ❙
qg1 : ⊦ ∀[a]∀[b]∃![x] a ∘ x ≐ b ❙
qg2 : ⊦ ∀[a]∀[b]∃![y] y ∘ a ≐ b ❙
leftDivision : U ⟶ U ⟶ U ❘ = [a,b] that U ([x] a ∘ x ≐ b) (forallE (forallE qg1 a) b) ❙
rightDivision : U ⟶ U ⟶ U ❘ = [a,b] that U ([x] x ∘ a ≐ b) (forallE (forallE qg2 a) b) ❙
❚
quasigroup = Mod ☞?QuasiGroup/quasigroup_theory ❙
❚
theory CancellativeMagma : base:?Logic =
include ?Magma ❙
/T MiKo: use this to make a view into quasisgroup Theory: they are cancellative ❙
theory cancellativemagma_theory : base:?Logic =
include ?Magma/magma_theory ❙
axiom_leftCancellative : ⊦ prop_leftCancellative op ❙
axiom_rightCancellative : ⊦ prop_rightCancellative op ❙
❚
cancellativemagma = Mod ☞?CancellativeMagma/cancellativemagma_theory ❙
/T MiKo: how to express the definitions? ❙
leftCancellative : magma ⟶ bool ❙
rightCancellative : magma ⟶ bool ❙
❚
/T Refactor: a Loop is just a unital Quasigroup ❚
theory Loop : base:?Logic =
include ?Unital ❙
include ☞base:?DescriptionOperator ❙
include ☞base:?NaturalDeduction ❙
theory loop_theory : base:?Logic =
include ?Unital/unital_theory ❙
inverse : U ⟶ U ❘ # 1 ⁻¹ prec 24 ❙
axiom_inverse : ⊦ prop_inverse op (inverse) e ❙
❚
loop = Mod ☞?Loop/loop_theory ❙
inverseElement : {U : unital} dom U ⟶ dom U ⟶ prop ❘ = [U][n,m] n ∘ m ≐ unitOf U ❙
inverseExists : loop ⟶ prop ❘ = [G] ∀ [x : dom G] ∃ [y : dom G] inverseElement G x y ❙
inverseOf : {G: loop} dom G ⟶ dom G ❘ # 2 ⁻¹ prec 25 ❘ = [G] [a] (G.inverse) a ❙
❚
theory Monoid : base:?Logic =
include ?SemiGroup ❙
include ?Unital ❙
theory monoid_theory : base:?Logic =
include ?SemiGroup/semigroup_theory ❙
include ?Unital/unital_theory ❙
❚
monoid = Mod ☞?Monoid/monoid_theory ❙
❚
theory Group : base:?Logic =
include ?Monoid ❙
include ?Loop ❙
theory group_theory : base:?Logic =
include ?Monoid/monoid_theory ❙
include ?Loop/loop_theory ❙
❚
group = Mod ☞?Group/group_theory ❙
inverseOf : {G: group} dom G ⟶ dom G ❘ # 2 ⁻¹ prec 25 ❘ = [G] [a] (G.inverse) a ❙
include ☞base:?NatLiterals ❙
include ☞base:?IntLiterals ❙
include ☞base:?InformalProofs ❙
include ☞sets:?FiniteCardinality ❙
automorphisms : group ⟶ ℕ ❙
cyclic : group ⟶ prop ❙
order : group ⟶ ℕ ❘ = [g] | fullset (baseset g) |❙
parity : group ⟶ ℤ ❙
solvable : group ⟶ prop ❙
degree : group ⟶ ℤ ❙
psolvable : group ⟶ ℕ+ ⟶ prop ❙
sylow : group ⟶ ℕ+ ⟶ group ❙
❚
theory AbelianGroup : base:?Logic =
include ?Group ❙
theory abeliangroup_theory : base:?Logic =
include ?Group/group_theory ❙
axiom_commutative : ⊦ prop_commutative op ❙
❚
abeliangroup = Mod ☞?AbelianGroup/abeliangroup_theory ❘ role abbreviation ❙
❚
theory GroupHomomorphism : base:?Logic =
include ?Group❙
theory groupHomomorphism_theory : base:?Logic =
from : group ❘# A❙
to : group ❘# B❙
morph : dom A ⟶ dom B❙
axiom_morphism : ⊦ ∀[x: dom A] ∀[y: dom A] (B.op) (morph x) (morph y) ≐ morph (x ∘ y)❙
❚
groupHomomorphism = Mod ☞?GroupHomomorphism/groupHomomorphism_theory❙
❚