Skip to content

Commit

Permalink
refactor: Rename FirstOrder.Language.Structure.rel_map to RelMap (#…
Browse files Browse the repository at this point in the history 
…3910)
  • Loading branch information
@Komyyy
Komyyy committed May 11, 2023
1 parent b5ac03c commit 127ca0a
Show file tree
Hide file tree
Showing 2 changed files with 25 additions and 21 deletions.
34 changes: 19 additions & 15 deletions Mathlib/ModelTheory/Basic.lean
View file
Expand Up @@ -296,9 +296,13 @@ class Structure where
/-- Interpretation of the function symbols -/
funMap : ∀ {n}, L.Functions n → (Fin n → M) → M
/-- Interpretation of the relation symbols -/
rel_map : ∀ {n}, L.Relations n → (Fin n → M) → Prop
RelMap : ∀ {n}, L.Relations n → (Fin n → M) → Prop
set_option linter.uppercaseLean3 false in
#align first_order.language.Structure FirstOrder.Language.Structure
set_option linter.uppercaseLean3 false in
#align first_order.language.Structure.fun_map FirstOrder.Language.Structure.funMap
set_option linter.uppercaseLean3 false in
#align first_order.language.Structure.rel_map FirstOrder.Language.Structure.RelMap

variable (N : Type w') [L.Structure M] [L.Structure N]

Expand Down Expand Up @@ -327,7 +331,7 @@ structure Hom where
map_fun' : ∀ {n} (f : L.Functions n) (x), toFun (funMap f x) = funMap f (toFun ∘ x) := by
intros; trivial
/-- The homomorphism sends related elements to related elements -/
map_rel' : ∀ {n} (r : L.Relations n) (x), rel_map r x → rel_map r (toFun ∘ x) := by
map_rel' : ∀ {n} (r : L.Relations n) (x), RelMap r x → RelMap r (toFun ∘ x) := by
-- Porting note: see porting note on `Hom.map_fun'`
intros; trivial
#align first_order.language.hom FirstOrder.Language.Hom
Expand All @@ -341,7 +345,7 @@ structure Embedding extends M ↪ N where
map_fun' : ∀ {n} (f : L.Functions n) (x), toFun (funMap f x) = funMap f (toFun ∘ x) := by
-- Porting note: see porting note on `Hom.map_fun'`
intros; trivial
map_rel' : ∀ {n} (r : L.Relations n) (x), rel_map r (toFun ∘ x) ↔ rel_map r x := by
map_rel' : ∀ {n} (r : L.Relations n) (x), RelMap r (toFun ∘ x) ↔ RelMap r x := by
-- Porting note: see porting note on `Hom.map_fun'`
intros; trivial
#align first_order.language.embedding FirstOrder.Language.Embedding
Expand All @@ -355,7 +359,7 @@ structure Equiv extends M ≃ N where
map_fun' : ∀ {n} (f : L.Functions n) (x), toFun (funMap f x) = funMap f (toFun ∘ x) := by
-- Porting note: see porting note on `Hom.map_fun'`
intros; trivial
map_rel' : ∀ {n} (r : L.Relations n) (x), rel_map r (toFun ∘ x) ↔ rel_map r x := by
map_rel' : ∀ {n} (r : L.Relations n) (x), RelMap r (toFun ∘ x) ↔ RelMap r x := by
-- Porting note: see porting note on `Hom.map_fun'`
intros; trivial
#align first_order.language.equiv FirstOrder.Language.Equiv
Expand Down Expand Up @@ -442,14 +446,14 @@ set_option linter.uppercaseLean3 false in

@[simp]
theorem relMap_apply₁ (r : r₁) (x : M) :
@Structure.rel_map _ M (Structure.mk₂ c' f₁' f₂' r₁' r₂') 1 r ![x] = (x ∈ r₁' r) :=
@Structure.RelMap _ M (Structure.mk₂ c' f₁' f₂' r₁' r₂') 1 r ![x] = (x ∈ r₁' r) :=
rfl
set_option linter.uppercaseLean3 false in
#align first_order.language.Structure.rel_map_apply₁ FirstOrder.Language.Structure.relMap_apply₁

@[simp]
theorem relMap_apply₂ (r : r₂) (x y : M) :
@Structure.rel_map _ M (Structure.mk₂ c' f₁' f₂' r₁' r₂') 2 r ![x, y] = r₂' r x y :=
@Structure.RelMap _ M (Structure.mk₂ c' f₁' f₂' r₁' r₂') 2 r ![x, y] = r₂' r x y :=
rfl
set_option linter.uppercaseLean3 false in
#align first_order.language.Structure.rel_map_apply₂ FirstOrder.Language.Structure.relMap_apply₂
Expand All @@ -461,15 +465,15 @@ end Structure
class HomClass (L : outParam Language) (F : Type _) (M N : outParam <| Type _)
[FunLike F M fun _ => N] [L.Structure M] [L.Structure N] where
map_fun : ∀ (φ : F) {n} (f : L.Functions n) (x), φ (funMap f x) = funMap f (φ ∘ x)
map_rel : ∀ (φ : F) {n} (r : L.Relations n) (x), rel_map r x → rel_map r (φ ∘ x)
map_rel : ∀ (φ : F) {n} (r : L.Relations n) (x), RelMap r x → RelMap r (φ ∘ x)
#align first_order.language.hom_class FirstOrder.Language.HomClass

/-- `StrongHomClass L F M N` states that `F` is a type of `L`-homomorphisms which preserve
relations in both directions. -/
class StrongHomClass (L : outParam Language) (F : Type _) (M N : outParam <| Type _)
[FunLike F M fun _ => N] [L.Structure M] [L.Structure N] where
map_fun : ∀ (φ : F) {n} (f : L.Functions n) (x), φ (funMap f x) = funMap f (φ ∘ x)
map_rel : ∀ (φ : F) {n} (r : L.Relations n) (x), rel_map r (φ ∘ x) ↔ rel_map r x
map_rel : ∀ (φ : F) {n} (r : L.Relations n) (x), RelMap r (φ ∘ x) ↔ RelMap r x
#align first_order.language.strong_hom_class FirstOrder.Language.StrongHomClass

--Porting note: using implicit brackets for `Structure` arguments
Expand Down Expand Up @@ -545,7 +549,7 @@ theorem map_constants (φ : M →[L] N) (c : L.Constants) : φ c = c :=

@[simp]
theorem map_rel (φ : M →[L] N) {n : ℕ} (r : L.Relations n) (x : Fin n → M) :
rel_map r x → rel_map r (φ ∘ x) :=
RelMap r x → RelMap r (φ ∘ x) :=
HomClass.map_rel φ r x
#align first_order.language.hom.map_rel FirstOrder.Language.Hom.map_rel

Expand Down Expand Up @@ -631,7 +635,7 @@ theorem map_constants (φ : M ↪[L] N) (c : L.Constants) : φ c = c :=

@[simp]
theorem map_rel (φ : M ↪[L] N) {n : ℕ} (r : L.Relations n) (x : Fin n → M) :
rel_map r (φ ∘ x) ↔ rel_map r x :=
RelMap r (φ ∘ x) ↔ RelMap r x :=
StrongHomClass.map_rel φ r x
#align first_order.language.embedding.map_rel FirstOrder.Language.Embedding.map_rel

Expand Down Expand Up @@ -801,7 +805,7 @@ theorem map_constants (φ : M ≃[L] N) (c : L.Constants) : φ c = c :=

@[simp]
theorem map_rel (φ : M ≃[L] N) {n : ℕ} (r : L.Relations n) (x : Fin n → M) :
rel_map r (φ ∘ x) ↔ rel_map r x :=
RelMap r (φ ∘ x) ↔ RelMap r x :=
StrongHomClass.map_rel φ r x
#align first_order.language.equiv.map_rel FirstOrder.Language.Equiv.map_rel

Expand Down Expand Up @@ -908,7 +912,7 @@ variable (L₁ L₂ : Language) (S : Type _) [L₁.Structure S] [L₂.Structure

instance sumStructure : (L₁.sum L₂).Structure S where
funMap := Sum.elim funMap funMap
rel_map := Sum.elim rel_map rel_map
RelMap := Sum.elim RelMap RelMap
set_option linter.uppercaseLean3 false in
#align first_order.language.sum_Structure FirstOrder.Language.sumStructure

Expand All @@ -928,13 +932,13 @@ theorem funMap_sum_inr {n : ℕ} (f : L₂.Functions n) :

@[simp]
theorem relMap_sum_inl {n : ℕ} (R : L₁.Relations n) :
@rel_map (L₁.sum L₂) S _ n (Sum.inl R) = rel_map R :=
@RelMap (L₁.sum L₂) S _ n (Sum.inl R) = RelMap R :=
rfl
#align first_order.language.rel_map_sum_inl FirstOrder.Language.relMap_sum_inl

@[simp]
theorem relMap_sum_inr {n : ℕ} (R : L₂.Relations n) :
@rel_map (L₁.sum L₂) S _ n (Sum.inr R) = rel_map R :=
@RelMap (L₁.sum L₂) S _ n (Sum.inr R) = RelMap R :=
rfl
#align first_order.language.rel_map_sum_inr FirstOrder.Language.relMap_sum_inr

Expand Down Expand Up @@ -1024,7 +1028,7 @@ variable {L : Language} {M : Type _} {N : Type _} [L.Structure M]
/-- A structure induced by a bijection. -/
@[simps!]
def inducedStructure (e : M ≃ N) : L.Structure N :=
⟨fun f x => e (funMap f (e.symm ∘ x)), fun r x => rel_map r (e.symm ∘ x)⟩
⟨fun f x => e (funMap f (e.symm ∘ x)), fun r x => RelMap r (e.symm ∘ x)⟩
set_option linter.uppercaseLean3 false in
#align equiv.induced_Structure Equiv.inducedStructure

Expand Down
12 changes: 6 additions & 6 deletions Mathlib/ModelTheory/LanguageMap.lean
View file
Expand Up @@ -78,7 +78,7 @@ variable (ϕ : L →ᴸ L')
/-- Pulls a structure back along a language map. -/
def reduct (M : Type _) [L'.Structure M] : L.Structure M where
funMap f xs := funMap (ϕ.onFunction f) xs
rel_map r xs := rel_map (ϕ.onRelation r) xs
RelMap r xs := RelMap (ϕ.onRelation r) xs
#align first_order.language.Lhom.reduct FirstOrder.Language.LHom.reduct

/-- The identity language homomorphism. -/
Expand Down Expand Up @@ -237,8 +237,8 @@ noncomputable def defaultExpansion (ϕ : L →ᴸ L')
funMap {n} f xs :=
if h' : f ∈ Set.range fun f : L.Functions n => onFunction ϕ f then funMap h'.choose xs
else default
rel_map {n} r xs :=
if h' : r ∈ Set.range fun r : L.Relations n => onRelation ϕ r then rel_map h'.choose xs
RelMap {n} r xs :=
if h' : r ∈ Set.range fun r : L.Relations n => onRelation ϕ r then RelMap h'.choose xs
else default
#align first_order.language.Lhom.default_expansion FirstOrder.Language.LHom.defaultExpansion

Expand All @@ -247,7 +247,7 @@ all symbols on that structure. -/
class IsExpansionOn (M : Type _) [L.Structure M] [L'.Structure M] : Prop where
map_onFunction : ∀ {n} (f : L.Functions n) (x : Fin n → M), funMap (ϕ.onFunction f) x = funMap f x
map_onRelation : ∀ {n} (R : L.Relations n) (x : Fin n → M),
rel_map (ϕ.onRelation R) x = rel_map R x
RelMap (ϕ.onRelation R) x = RelMap R x
#align first_order.language.Lhom.is_expansion_on FirstOrder.Language.LHom.IsExpansionOn

@[simp]
Expand All @@ -258,7 +258,7 @@ theorem map_onFunction {M : Type _} [L.Structure M] [L'.Structure M] [ϕ.IsExpan

@[simp]
theorem map_onRelation {M : Type _} [L.Structure M] [L'.Structure M] [ϕ.IsExpansionOn M] {n}
(R : L.Relations n) (x : Fin n → M) : rel_map (ϕ.onRelation R) x = rel_map R x :=
(R : L.Relations n) (x : Fin n → M) : RelMap (ϕ.onRelation R) x = RelMap R x :=
IsExpansionOn.map_onRelation R x
#align first_order.language.Lhom.map_on_relation FirstOrder.Language.LHom.map_onRelation

Expand Down Expand Up @@ -512,7 +512,7 @@ theorem withConstants_funMap_sum_inl [L[[α]].Structure M] [(lhomWithConstants L

@[simp]
theorem withConstants_relMap_sum_inl [L[[α]].Structure M] [(lhomWithConstants L α).IsExpansionOn M]
{n} {R : L.Relations n} {x : Fin n → M} : @rel_map (L[[α]]) M _ n (Sum.inl R) x = rel_map R x :=
{n} {R : L.Relations n} {x : Fin n → M} : @RelMap (L[[α]]) M _ n (Sum.inl R) x = RelMap R x :=
(lhomWithConstants L α).map_onRelation R x
#align first_order.language.with_constants_rel_map_sum_inl FirstOrder.Language.withConstants_relMap_sum_inl

Expand Down

0 comments on commit 127ca0a

Please sign in to comment.