ALGEBRAIC STRUCTURE

Results presented here are formalized in Ground Zero library using Lean Theorem Prover.

ALGEBRA

Definition. Signature over given types $ι, υ : \mathcal{U}$ (called indices) is an element of type $ι + υ \rightarrow \mathbb{N}$.
Where $A + B : \mathcal{U}$ denotes coproduct type.

Definition. Vector of length $n$ over type $A : \mathcal{U}$ (denoted $\mathrm{vect}(A, n)$) is a type: $$ \underbrace{A \times A \times … \times A}_{\text{n times}} \times \textbf{1} $$
Where $\textbf{1} : \mathcal{U}$ denotes unit type that contains only $\star : \textbf{1}$.

Definition. Assume we have types $A, B : \mathcal{U}$, function $f : A \rightarrow B$, and a natural number $n : \mathbb{N}$. Then we define function $f^{\mathrm{map}} : \mathrm{vect}(A, n) \rightarrow \mathrm{vect}(B, n)$: $$ f^{\mathrm{map}}(a_1, a_2, …, a_n, \star) ≔ (f(a_1), f(a_2), …, f(a_n), \star) $$

Definition. $n$-ary algebraic operation over given type $A : \mathcal{U}$ is an element of type: $$ \mathrm{vect}(A, n) \rightarrow A $$

Definition. $n$-ary algebraic relation over given type $A : \mathcal{U}$ is an element of type: $$ \mathrm{vect}(A, n) \rightarrow Ω $$
Where $Ω$ denotes type of all propositions, i.e. $$ Ω ≔ \sum_{A : \mathcal{U}} isProp(A) $$

Definition. Algebraic structure over signature $\mathrm{deg}$ constists of: (i) 0-Type called carrier, (ii) $\mathrm{deg}(\mathrm{inl}(i))$-ary algebraic operation for each $i : ι$, (iii) $\mathrm{deg}(\mathrm{inr}(i))$-ary algebraic relation for each $i : υ$.
Or, more explicitly: $$ \mathrm{Alg}(\mathrm{deg}) ≔ \sum_{A : \text{0-Type}} \left( \prod_{i : ι} \mathrm{vect}(A, \mathrm{deg}(\mathrm{inl}(i))) \rightarrow A \right) \times \\ \left( \prod_{i : υ} \mathrm{vect}(A, \mathrm{deg}(\mathrm{inr}(i))) \rightarrow Ω \right) $$
We will write $Γ^{\mathrm{car}}$ for carrier of algebraic structure $Γ$, $Γ^{\mathrm{op}}$ for its algebraic operations, and $Γ^{\mathrm{rel}}$ for its relations.

Mappings

Definition (Homomorphism). Given two algebraic structures $Γ, Λ$ over signature $\mathrm{deg}$ and a function between them $φ : Γ^{\mathrm{car}} \rightarrow Λ^{\mathrm{car}}$, we say that $φ$ is homomorphism iff holds:
(i) $φ(Γ^{\mathrm{op}}(i, v)) = Λ^{\mathrm{op}}(i, φ^{\mathrm{map}}(v))$,
(ii) $Γ^{\mathrm{rel}}(i, v) = Λ^{\mathrm{rel}}(i, φ^{\mathrm{map}}(v))$,
for each $i : ι$ or $i : υ$ and $v : \mathrm{deg}(\mathrm{inr}(i))$.

Theorem. Composition of two homomorphisms is also homomorphism.

Definition (Isomorphism). We say that $φ : Γ^{\mathrm{car}} \rightarrow Λ^{\mathrm{car}}$ is an ismorphism iff it is bijective and homomorphism. Then we can say that $Γ$ and $Λ$ are isomorphic and write $φ : Γ \cong Λ$.

Theorem. Isomorphism is an equivalence relation, i.e.
(i) $Γ \cong Γ$,
(ii) $Γ \cong Λ \rightarrow Λ \cong Γ$,
(iii) $Γ \cong Λ \rightarrow Λ \cong Δ \rightarrow Γ \cong Δ$.

Theorem (Univalence for Algebraic Structures). $$ (Γ \cong Λ) \simeq (Γ = Λ) $$