Composition of partial equivalences

Partial equivalences f : M ≃ₚ[L] N and g : N ≃ₚ[L] P compose when the codomain of f lies in the domain of g. The composite has the domain of f, applies f, then g, and has as codomain the image under g of the codomain of f. It is monotone in both partial equivalences.

Main definitions

• FirstOrder.Language.PartialEquiv.comp: the composite of compatible partial equivalences.

Main results

• FirstOrder.Language.PartialEquiv.toEquiv_apply_of_le: a larger partial equivalence agrees with a smaller one on the smaller domain.
• FirstOrder.Language.PartialEquiv.mem_cod_comp: the codomain of a composite.
• FirstOrder.Language.PartialEquiv.comp_le_comp: composition is monotone in both arguments.
• FirstOrder.Language.FGEquiv.exists_le_and_le_dom_of_fg: in a family of finitely generated partial equivalences closed under forth extensions, every member extends to cover any finitely generated substructure.

theorem FirstOrder.Language.PartialEquiv.toEquiv_apply_of_le {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.PartialEquiv M N} (h : f ≤ g) {x : M} (hx : x ∈ f.dom) : ↑(g.toEquiv ⟨x, ⋯⟩) = ↑(f.toEquiv ⟨x, hx⟩)

A larger partial equivalence takes the same values on the domain of a smaller one.

noncomputable def FirstOrder.Language.PartialEquiv.comp {L : Language} {M : Type w} {N : Type w'} {P : Type w''} [L.Structure M] [L.Structure N] [L.Structure P] (g : L.PartialEquiv N P) (f : L.PartialEquiv M N) (h : f.cod ≤ g.dom) : L.PartialEquiv M P

The composite of partial equivalences f : M ≃ₚ[L] N and g : N ≃ₚ[L] P when the codomain of f lies in the domain of g. It has the domain of f.

@[simp]

theorem FirstOrder.Language.PartialEquiv.dom_comp {L : Language} {M : Type w} {N : Type w'} {P : Type w''} [L.Structure M] [L.Structure N] [L.Structure P] (g : L.PartialEquiv N P) (f : L.PartialEquiv M N) (h : f.cod ≤ g.dom) : (g.comp f h).dom = f.dom

The composite has the domain of the first partial equivalence.

@[simp]

theorem FirstOrder.Language.PartialEquiv.comp_apply {L : Language} {M : Type w} {N : Type w'} {P : Type w''} [L.Structure M] [L.Structure N] [L.Structure P] (g : L.PartialEquiv N P) (f : L.PartialEquiv M N) (h : f.cod ≤ g.dom) (x : ↥(g.comp f h).dom) : ↑((g.comp f h).toEquiv x) = ↑(g.toEquiv ((Substructure.inclusion h) (f.toEquiv ((Substructure.inclusion ⋯) x))))

The composite applies the first partial equivalence, then the second.

@[simp]

theorem FirstOrder.Language.PartialEquiv.mem_cod_comp {L : Language} {M : Type w} {N : Type w'} {P : Type w''} [L.Structure M] [L.Structure N] [L.Structure P] (g : L.PartialEquiv N P) (f : L.PartialEquiv M N) (h : f.cod ≤ g.dom) {p : P} : p ∈ (g.comp f h).cod ↔ ∃ (y : ↥f.cod), ↑(g.toEquiv ((Substructure.inclusion h) y)) = p

The codomain of the composite is the image under the second partial equivalence of the codomain of the first.

theorem FirstOrder.Language.PartialEquiv.cod_comp_le {L : Language} {M : Type w} {N : Type w'} {P : Type w''} [L.Structure M] [L.Structure N] [L.Structure P] (g : L.PartialEquiv N P) (f : L.PartialEquiv M N) (h : f.cod ≤ g.dom) : (g.comp f h).cod ≤ g.cod

The codomain of the composite lies in the codomain of the second partial equivalence.

theorem FirstOrder.Language.PartialEquiv.cod_comp_of_eq {L : Language} {M : Type w} {N : Type w'} {P : Type w''} [L.Structure M] [L.Structure N] [L.Structure P] (g : L.PartialEquiv N P) (f : L.PartialEquiv M N) (h : f.cod ≤ g.dom) (he : f.cod = g.dom) : (g.comp f h).cod = g.cod

When the codomain of the first partial equivalence is the domain of the second, the composite has the codomain of the second.

theorem FirstOrder.Language.PartialEquiv.comp_le_comp {L : Language} {M : Type w} {N : Type w'} {P : Type w''} [L.Structure M] [L.Structure N] [L.Structure P] {f f' : L.PartialEquiv M N} {g g' : L.PartialEquiv N P} (hf : f ≤ f') (hg : g ≤ g') (h : f.cod ≤ g.dom) (h' : f'.cod ≤ g'.dom) : g.comp f h ≤ g'.comp f' h'

Composition of partial equivalences is monotone in both arguments.

theorem FirstOrder.Language.FGEquiv.exists_le_and_le_dom_of_fg {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {T : Set (L.FGEquiv M N)} (hT : ∀ g ∈ T, ∀ (m : M), ∃ g' ∈ T, m ∈ (↑g').dom ∧ g ≤ g') {g : L.FGEquiv M N} (hg : g ∈ T) {A : L.Substructure M} (hA : A.FG) : ∃ g' ∈ T, A ≤ (↑g').dom ∧ g ≤ g'

In a family of finitely generated partial equivalences closed under forth extensions, every member extends within the family to one whose domain contains a given finitely generated substructure.