Language Maps #
Maps between first-order languages in the style of the Flypitch project, as well as several important maps between structures.
Main Definitions #
- A
FirstOrder.Language.LHom
, denotedL →ᴸ L'
, is a map between languages, sending the symbols of one to symbols of the same kind and arity in the other. - A
FirstOrder.Language.LEquiv
, denotedL ≃ᴸ L'
, is an invertible language homomorphism. FirstOrder.Language.withConstants
is defined so that ifM
is anL.Structure
andA : Set M
,L.withConstants A
, denotedL[[A]]
, is a language which adds constant symbols for elements ofA
toL
.
References #
For the Flypitch project:
- [J. Han, F. van Doorn, A formal proof of the independence of the continuum hypothesis] [HvD20]
- J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis
A language homomorphism maps the symbols of one language to symbols of another.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The identity language homomorphism.
Equations
Instances For
Equations
- FirstOrder.Language.LHom.instInhabited = { default := FirstOrder.Language.LHom.id L }
The inclusion of an empty language into any other language.
Equations
- FirstOrder.Language.LHom.ofIsEmpty L L' = { onFunction := fun {n : ℕ} (a : L.Functions n) => isEmptyElim a, onRelation := fun {n : ℕ} (a : L.Relations n) => isEmptyElim a }
Instances For
Equations
- FirstOrder.Language.LHom.instUniqueOfIsAlgebraicOfIsRelational = { default := FirstOrder.Language.LHom.ofIsEmpty L L', uniq := ⋯ }
The map between two sum-languages induced by maps on the two factors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A language homomorphism is injective when all the maps between symbol types are.
- onFunction {n : ℕ} : Function.Injective fun (f : L.Functions n) => ϕ.onFunction f
- onRelation {n : ℕ} : Function.Injective fun (R : L.Relations n) => ϕ.onRelation R
Instances For
Pulls an L
-structure along a language map ϕ : L →ᴸ L'
, and then expands it
to an L'
-structure arbitrarily.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A language homomorphism is an expansion on a structure if it commutes with the interpretation of all symbols on that structure.
- map_onFunction {n : ℕ} (f : L.Functions n) (x : Fin n → M) : Structure.funMap (ϕ.onFunction f) x = Structure.funMap f x
- map_onRelation {n : ℕ} (R : L.Relations n) (x : Fin n → M) : Structure.RelMap (ϕ.onRelation R) x = Structure.RelMap R x
Instances
A language equivalence maps the symbols of one language to symbols of another bijectively.
Instances For
A language equivalence maps the symbols of one language to symbols of another bijectively.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The identity equivalence from a first-order language to itself.
Equations
- FirstOrder.Language.LEquiv.refl L = { toLHom := FirstOrder.Language.LHom.id L, invLHom := FirstOrder.Language.LHom.id L, left_inv := ⋯, right_inv := ⋯ }
Instances For
Equations
- FirstOrder.Language.LEquiv.instInhabited = { default := FirstOrder.Language.LEquiv.refl L }
The composition of equivalences of first-order languages.
Equations
- e.trans e' = { toLHom := e'.toLHom.comp e.toLHom, invLHom := e.invLHom.comp e'.invLHom, left_inv := ⋯, right_inv := ⋯ }
Instances For
The type of functions for a language consisting only of constant symbols.
Equations
Instances For
A language with constants indexed by a type.
Equations
- FirstOrder.Language.constantsOn α = { Functions := FirstOrder.Language.constantsOnFunc α, Relations := fun (x : ℕ) => Empty }
Instances For
Gives a constantsOn α
structure to a type by assigning each constant a value.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A map between index types induces a map between constant languages.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extends a language with a constant for each element of a parameter set in M
.
Equations
- L.withConstants α = L.sum (FirstOrder.Language.constantsOn α)
Instances For
Extends a language with a constant for each element of a parameter set in M
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The language map adding constants.
Equations
- L.lhomWithConstants α = FirstOrder.Language.LHom.sumInl
Instances For
The language map extending the constant set.
Equations
- L.lhomWithConstantsMap f = (FirstOrder.Language.LHom.id L).sumMap (FirstOrder.Language.LHom.constantsOnMap f)
Instances For
Equations
- L.withConstantsSelfStructure = L.sumStructure (FirstOrder.Language.constantsOn M) M
Equations
- L.withConstantsStructure α = L.sumStructure (FirstOrder.Language.constantsOn α) M