Isomorphisms, embeddings, and injective homomorphisms

We define isomorphisms between finite structures, prove they form an equivalence relation, and show that isomorphic structures have the same cardinality. We also define embeddings (injective maps that preserve and reflect relations, as in model theory) and the weaker injective homomorphisms (which only preserve them).

structure Complexity.DescriptiveComplexity.Iso {V : Vocabulary} (A B : FinStruct V) : Type

An isomorphism between two finite structures over the same vocabulary.

• toFun : Fin A.card → Fin B.card

  The forward map on the universe

• invFun : Fin B.card → Fin A.card

  The inverse map on the universe

• left_inv (x : Fin A.card) : self.invFun (self.toFun x) = x

  Left inverse

• right_inv (y : Fin B.card) : self.toFun (self.invFun y) = y

  Right inverse

• rel_map (i : Fin V.numRels) (args : Fin (V.relArity i) → Fin A.card) : A.rel i args ↔ B.rel i (self.toFun ∘ args)

  Relations are preserved

• const_map (j : Fin V.numConsts) : self.toFun (A.const j) = B.const j

  Constants are preserved

def Complexity.DescriptiveComplexity.«term_≅_» : Lean.TrailingParserDescr

A ≅ B denotes an isomorphism between finite structures A and B.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DescriptiveComplexity.Iso.refl {V : Vocabulary} (A : FinStruct V) : Iso A A

The identity isomorphism.

Equations

• Complexity.DescriptiveComplexity.Iso.refl A = { toFun := id, invFun := id, left_inv := ⋯, right_inv := ⋯, rel_map := ⋯, const_map := ⋯ }

def Complexity.DescriptiveComplexity.Iso.symm {V : Vocabulary} {A B : FinStruct V} (f : Iso A B) : Iso B A

The inverse of an isomorphism.

Equations

• f.symm = { toFun := f.invFun, invFun := f.toFun, left_inv := ⋯, right_inv := ⋯, rel_map := ⋯, const_map := ⋯ }

def Complexity.DescriptiveComplexity.Iso.trans {V : Vocabulary} {A B C : FinStruct V} (f : Iso A B) (g : Iso B C) : Iso A C

Composition of isomorphisms.

Equations

• f.trans g = { toFun := g.toFun ∘ f.toFun, invFun := f.invFun ∘ g.invFun, left_inv := ⋯, right_inv := ⋯, rel_map := ⋯, const_map := ⋯ }

theorem Complexity.DescriptiveComplexity.Iso.toFun_injective {V : Vocabulary} {A B : FinStruct V} (f : Iso A B) : Function.Injective f.toFun

theorem Complexity.DescriptiveComplexity.Iso.toFun_surjective {V : Vocabulary} {A B : FinStruct V} (f : Iso A B) : Function.Surjective f.toFun

theorem Complexity.DescriptiveComplexity.Iso.card_eq {V : Vocabulary} {A B : FinStruct V} (f : Iso A B) : A.card = B.card

Isomorphic structures have the same cardinality.

structure Complexity.DescriptiveComplexity.InjectiveHom {V : Vocabulary} (A B : FinStruct V) : Type

An injective homomorphism of structure A into structure B: an injective map of universes that preserves constants and carries every relation tuple of A to a relation tuple of B. Relations are preserved but not reflected, so B may relate images of elements that A does not relate; the notion that also reflects them is Embedding.

• toFun : Fin A.card → Fin B.card

  The map of universes

• injective : Function.Injective self.toFun

  The map is injective

• rel_map (i : Fin V.numRels) (args : Fin (V.relArity i) → Fin A.card) : A.rel i args → B.rel i (self.toFun ∘ args)

  Relations are preserved (forward direction only)

• const_map (j : Fin V.numConsts) : self.toFun (A.const j) = B.const j

  Constants are preserved

def Complexity.DescriptiveComplexity.InjectiveHom.ofIso {V : Vocabulary} {A B : FinStruct V} (f : Iso A B) : InjectiveHom A B

Every isomorphism gives an injective homomorphism.

Equations

• Complexity.DescriptiveComplexity.InjectiveHom.ofIso f = { toFun := f.toFun, injective := ⋯, rel_map := ⋯, const_map := ⋯ }

structure Complexity.DescriptiveComplexity.Embedding {V : Vocabulary} (A B : FinStruct V) : Type

An embedding of structure A into structure B, in the model-theoretic sense (Mathlib's FirstOrder.Language.Embedding): an injective map of universes that preserves constants and both preserves and reflects relations. Its image is a substructure of B isomorphic to A, so Nonempty (Embedding A B) says that A is, up to isomorphism, a substructure of B.

• toFun : Fin A.card → Fin B.card

  The map of universes

• injective : Function.Injective self.toFun

  The map is injective

• rel_iff (i : Fin V.numRels) (args : Fin (V.relArity i) → Fin A.card) : A.rel i args ↔ B.rel i (self.toFun ∘ args)

  Relations are preserved and reflected

• const_map (j : Fin V.numConsts) : self.toFun (A.const j) = B.const j

  Constants are preserved

def Complexity.DescriptiveComplexity.Embedding.refl {V : Vocabulary} (A : FinStruct V) : Embedding A A

The identity embedding.

Equations

• Complexity.DescriptiveComplexity.Embedding.refl A = { toFun := id, injective := ⋯, rel_iff := ⋯, const_map := ⋯ }

def Complexity.DescriptiveComplexity.Embedding.trans {V : Vocabulary} {A B C : FinStruct V} (f : Embedding A B) (g : Embedding B C) : Embedding A C

Composition of embeddings.

Equations

• f.trans g = { toFun := g.toFun ∘ f.toFun, injective := ⋯, rel_iff := ⋯, const_map := ⋯ }

def Complexity.DescriptiveComplexity.Embedding.ofIso {V : Vocabulary} {A B : FinStruct V} (f : Iso A B) : Embedding A B

Every isomorphism is an embedding.

Equations

• Complexity.DescriptiveComplexity.Embedding.ofIso f = { toFun := f.toFun, injective := ⋯, rel_iff := ⋯, const_map := ⋯ }

def Complexity.DescriptiveComplexity.Embedding.toInjectiveHom {V : Vocabulary} {A B : FinStruct V} (f : Embedding A B) : InjectiveHom A B

An embedding is in particular an injective homomorphism.

Equations

• f.toInjectiveHom = { toFun := f.toFun, injective := ⋯, rel_map := ⋯, const_map := ⋯ }