Isomorphisms, Embeddings, and Substructures

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 and substructures.

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.Embedding {V : Vocabulary} (A B : FinStruct V) : Type

An embedding of structure A into structure B.

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

  The embedding function

• injective : Function.Injective self.toFun

  The embedding 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.Embedding.ofIso {V : Vocabulary} {A B : FinStruct V} (f : Iso A B) : Embedding A B

Every isomorphism gives an embedding.

Equations

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

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

Structure A is a substructure of B if there is an inclusion that both preserves and reflects relations.

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

  The inclusion function

• injective : Function.Injective self.toFun

  The inclusion 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.IsSubstructure.refl {V : Vocabulary} (A : FinStruct V) : IsSubstructure A A

Every structure is a substructure of itself.

Equations

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

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

Substructure is transitive.

Equations

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