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] [flypitch_cpp]
- [J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis][flypitch_itp]
- onFunction : ⦃n : ℕ⦄ → FirstOrder.Language.Functions L n → FirstOrder.Language.Functions L' n
- onRelation : ⦃n : ℕ⦄ → FirstOrder.Language.Relations L n → FirstOrder.Language.Relations L' n
A language homomorphism maps the symbols of one language to symbols of another.
Instances For
A language homomorphism maps the symbols of one language to symbols of another.
Instances For
Defines a map between languages defined with Language.mk₂
.
Instances For
Pulls a structure back along a language map.
Instances For
The identity language homomorphism.
Instances For
The inclusion of the left factor into the sum of two languages.
Instances For
The inclusion of the right factor into the sum of two languages.
Instances For
The inclusion of an empty language into any other language.
Instances For
The composition of two language homomorphisms.
Instances For
A language map defined on two factors of a sum.
Instances For
The map between two sum-languages induced by maps on the two factors.
Instances For
- onFunction : ∀ {n : ℕ}, Function.Injective fun f => FirstOrder.Language.LHom.onFunction ϕ f
- onRelation : ∀ {n : ℕ}, Function.Injective fun R => FirstOrder.Language.LHom.onRelation ϕ R
A language homomorphism is injective when all the maps between symbol types are.
Instances For
Pulls an L
-structure along a language map ϕ : L →ᴸ L'
, and then expands it
to an L'
-structure arbitrarily.
Instances For
- map_onFunction : ∀ {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M), FirstOrder.Language.Structure.funMap (FirstOrder.Language.LHom.onFunction ϕ f) x = FirstOrder.Language.Structure.funMap f x
- map_onRelation : ∀ {n : ℕ} (R : FirstOrder.Language.Relations L n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap (FirstOrder.Language.LHom.onRelation ϕ R) x = FirstOrder.Language.Structure.RelMap R x
A language homomorphism is an expansion on a structure if it commutes with the interpretation of all symbols on that structure.
Instances
- toLHom : L →ᴸ L'
- invLHom : L' →ᴸ L
- left_inv : FirstOrder.Language.LHom.comp s.invLHom s.toLHom = FirstOrder.Language.LHom.id L
- right_inv : FirstOrder.Language.LHom.comp s.toLHom s.invLHom = FirstOrder.Language.LHom.id L'
A language equivalence maps the symbols of one language to symbols of another bijectively.
Instances For
The identity equivalence from a first-order language to itself.
Instances For
The inverse of an equivalence of first-order languages.
Instances For
The composition of equivalences of first-order languages.
Instances For
A language with constants indexed by a type.
Instances For
Gives a constantsOn α
structure to a type by assigning each constant a value.
Instances For
A map between index types induces a map between constant languages.
Instances For
Extends a language with a constant for each element of a parameter set in M
.
Instances For
Extends a language with a constant for each element of a parameter set in M
.
Instances For
The language map adding constants.
Instances For
The constant symbol indexed by a particular element.
Instances For
Adds constants to a language map.
Instances For
The language map removing an empty constant set.
Instances For
The language map extending the constant set.