Independent bases of laws

DefinitionConsequence of a set of laws#✓fully proved

Let \(F\) be the free group on countably many generators \(x_0, x_1, x_2, \dots\), let \(W \subseteq F\) be a set of laws and let \(w \in F\). Then \(w\) is a consequence of \(W\) if \(w\) holds in every group \(G\) satisfying all laws in \(W\): whenever every homomorphism \(F \to G\) sends each element of \(W\) to \(1\), every homomorphism \(F \to G\) sends \(w\) to \(1\).

def LawConsequence (W : Set (FreeGroup ℕ)) (w : FreeGroup ℕ) : Prop :=
  ∀ (G : Type) [Group G], SatisfiesLaws W G → SatisfiesLaws {w} G

Uses 1 · Used by 1

Statement usesGroups satisfying a set of laws

Used byIndependent basis of laws

DefinitionIndependent basis of laws#✓fully proved

Let \(F\) be the free group on countably many generators \(x_0, x_1, x_2, \dots\) and let \(W \subseteq F\) be a set of laws. The variety defined by \(W\) has an independent basis of identities if there is a set \(B \subseteq F\) of laws such that a law is a consequence of \(B\) exactly when it is a consequence of \(W\), and no \(b \in B\) is a consequence of \(B \setminus \{b\}\).

def HasIndependentLawBasis (W : Set (FreeGroup ℕ)) : Prop :=
  ∃ B : Set (FreeGroup ℕ), (∀ w, LawConsequence B w ↔ LawConsequence W w) ∧
    ∀ b ∈ B, ¬ LawConsequence (B \ {b}) b

Uses 1

Statement usesConsequence of a set of laws

DefinitionConsequence of a set of quasi-identities#✓fully proved

Let \(Q\) be a set of quasi-identities and \(q\) a quasi-identity. Then \(q\) is a consequence of \(Q\) if \(q\) holds in every group in which all members of \(Q\) hold.

def QuasiIdentityConsequence (Q : Set QuasiIdentity) (q : QuasiIdentity) : Prop :=
  ∀ (G : Type) [Group G], Models Q G → q.HoldsIn G

Uses 3 · Used by 1

Statement usesThe quasivariety defined by a set of quasi-identities · Quasi-identities of groups · Quasi-identities holding in a group

Used byIndependent basis of quasi-identities

DefinitionIndependent basis of quasi-identities#✓fully proved

The quasi-identities of a group \(G\) have an independent basis if there is a set \(B\) of quasi-identities such that a quasi-identity is a consequence of \(B\) exactly when it holds in \(G\), and no \(b \in B\) is a consequence of \(B \setminus \{b\}\).

def HasIndependentQuasiIdentityBasis (G : Type) [Group G] : Prop :=
  ∃ B : Set QuasiIdentity, (∀ q, QuasiIdentityConsequence B q ↔ q.HoldsIn G) ∧
    ∀ b ∈ B, ¬ QuasiIdentityConsequence (B \ {b}) b

Uses 3

Statement usesConsequence of a set of quasi-identities · Quasi-identities of groups · Quasi-identities holding in a group

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.