First-order language of groups

InductiveGroup function symbols#✓fully proved

The function symbols of the first-order language of groups, graded by arity, are a constant symbol for the identity (arity \(0\)), a symbol for inversion (arity \(1\)) and a symbol for multiplication (arity \(2\)); there are no others.

inductive GroupFunction : ℕ → Type
  | one : GroupFunction 0
  | inv : GroupFunction 1
  | mul : GroupFunction 2

Used by 6

Used byThe first-order language of groups · The function symbols of the language of groups · The canonical structure on a group · Inversion in the canonical structure · Multiplication in the canonical structure · The identity in the canonical structure

DefinitionThe first-order language of groups#✓fully proved

The first-order language of groups has the group function symbols (a constant for the identity, a unary symbol for inversion and a binary symbol for multiplication) as its function symbols and no relation symbols.

def groupLanguage : FirstOrder.Language where
  Functions := GroupFunction
  Relations := fun _ => Empty

Uses 1 · Used by 7

Statement usesGroup function symbols

Used byFirst-order axiomatizable classes of groups · The function symbols of the language of groups · The language of groups has no relation symbols · The canonical structure on a group · Inversion in the canonical structure · Multiplication in the canonical structure · The identity in the canonical structure

DefinitionThe canonical structure on a group#✓fully proved

For a group \(G\), the canonical structure on \(G\) for the first-order language of groups interprets the identity constant as the identity \(1\) of \(G\), inversion as \(x \mapsto x^{-1}\) and multiplication as \((x, y) \mapsto xy\); there are no relation symbols to interpret.

@[reducible]
def groupLanguageStructure (G : Type u) [Group G] : groupLanguage.Structure G where
  funMap := fun {_} f x =>
    match f with
    | .one => 1
    | .inv => (x 0)⁻¹
    | .mul => x 0 * x 1
  RelMap := fun {_} r => nomatch r

Uses 2 · Used by 4

Statement usesGroup function symbols · The first-order language of groups

Used byFirst-order axiomatizable classes of groups · Inversion in the canonical structure · Multiplication in the canonical structure · The identity in the canonical structure

TheoremThe function symbols of the language of groups#✓fully proved

For every \(n \in \mathbb{N}\), the \(n\)-ary function symbols of the first-order language of groups are exactly the group function symbols of arity \(n\).

theorem groupLanguage_functions (n : ℕ) :
    groupLanguage.Functions n = GroupFunction n

Uses 2

Statement usesGroup function symbols · The first-order language of groups

TheoremThe language of groups has no relation symbols#✓fully proved

For every \(n \in \mathbb{N}\), the first-order language of groups has no \(n\)-ary relation symbols.

theorem groupLanguage_relations (n : ℕ) :
    groupLanguage.Relations n = Empty

Uses 1

Statement usesThe first-order language of groups

TheoremMultiplication in the canonical structure#✓fully proved

For every group \(G\) and every pair \((x_0, x_1)\) of elements of \(G\), the multiplication symbol of the language of groups, interpreted in the canonical structure on \(G\), sends \((x_0, x_1)\) to \(x_0 x_1\).

theorem groupLanguageStructure_mul (G : Type u) [Group G] (x : Fin 2 → G) :
    (groupLanguageStructure G).funMap GroupFunction.mul x = x 0 * x 1

Uses 3

Statement usesGroup function symbols · The first-order language of groups · The canonical structure on a group

TheoremInversion in the canonical structure#✓fully proved

For every group \(G\) and every one-element tuple \((x_0)\) of elements of \(G\), the inversion symbol of the language of groups, interpreted in the canonical structure on \(G\), sends \((x_0)\) to \(x_0^{-1}\).

theorem groupLanguageStructure_inv (G : Type u) [Group G] (x : Fin 1 → G) :
    (groupLanguageStructure G).funMap GroupFunction.inv x = (x 0)⁻¹

Uses 3

Statement usesGroup function symbols · The first-order language of groups · The canonical structure on a group

TheoremThe identity in the canonical structure#✓fully proved

For every group \(G\), the identity constant symbol of the language of groups, interpreted in the canonical structure on \(G\), takes the value \(1\) at the empty tuple, where \(1\) is the identity of \(G\).

theorem groupLanguageStructure_one (G : Type u) [Group G] (x : Fin 0 → G) :
    (groupLanguageStructure G).funMap GroupFunction.one x = 1

Uses 3

Statement usesGroup function symbols · The first-order language of groups · The canonical structure on a group

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.