feat(ModelTheory): lift of equivalences between direct limits, and di…

…rect limit of system of substructures (#11174)

Define the equivalence between direct limits of isomorphic systems, and the equivalence between the direct limit of a system of substructures and the union of these substructures.
Co-authored-by: Aaron Anderson <awainverse@gmail.com>



Co-authored-by: Gabin <68381468+QuinnLesquimau@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib/ModelTheory/Basic.lean

@@ -667,6 +667,15 @@ theorem ext_iff {f g : M ↪[L] N} : f = g ↔ ∀ x, f x = g x :=
   ⟨fun h _ => h ▸ rfl, fun h => ext h⟩
 #align first_order.language.embedding.ext_iff FirstOrder.Language.Embedding.ext_iff
 
+theorem toHom_injective : @Function.Injective (M ↪[L] N) (M →[L] N) (·.toHom) := by
+  intro f f' h
+  ext
+  exact congr_fun (congr_arg (↑) h) _
+
+@[simp]
+theorem toHom_inj {f g : M ↪[L] N} : f.toHom = g.toHom ↔ f = g :=
+  ⟨fun h ↦ toHom_injective h, fun h ↦ congr_arg (·.toHom) h⟩
+
 theorem injective (f : M ↪[L] N) : Function.Injective f :=
   f.toEmbedding.injective
 #align first_order.language.embedding.injective FirstOrder.Language.Embedding.injective

Mathlib/ModelTheory/DirectLimit.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Aaron Anderson
+Authors: Aaron Anderson, Gabin Kolly
 -/
 import Mathlib.Init.Align
 import Mathlib.Data.Fintype.Order
@@ -18,10 +18,15 @@ This file constructs the direct limit of a directed system of first-order embedd
 ## Main Definitions
 * `FirstOrder.Language.DirectLimit G f` is the direct limit of the directed system `f` of
   first-order embeddings between the structures indexed by `G`.
+* `FirstOrder.Language.DirectLimit.lift` is the universal property of the direct limit: maps
+  from the components to another module that respect the directed system structure give rise to
+  a unique map out of the direct limit.
+* `FirstOrder.Language.DirectLimit.equiv_lift` is the equivalence between limits of
+  isomorphic direct systems.
 -/
 
 
-universe v w u₁ u₂
+universe v w w' u₁ u₂
 
 open FirstOrder
 
@@ -335,6 +340,23 @@ protected theorem inductionOn {C : DirectLimit G f → Prop} (z : DirectLimit G
   h ▸ ih i x
 #align first_order.language.direct_limit.induction_on FirstOrder.Language.DirectLimit.inductionOn
 
+theorem iSup_range_of_eq_top : ⨆ i, (of L ι G f i).toHom.range = ⊤ :=
+  eq_top_iff.2 (fun x _ ↦ DirectLimit.inductionOn x
+    (fun i _ ↦ le_iSup (fun i ↦ Hom.range (Embedding.toHom (of L ι G f i))) i (mem_range_self _)))
+
+/-- Every finitely generated substructure of the direct limit corresponds to some
+substructure in some component of the directed system. -/
+theorem exists_fg_substructure_in_Sigma (S : L.Substructure (DirectLimit G f)) (S_fg : S.FG) :
+    ∃ i, ∃ T : L.Substructure (G i), T.map (of L ι G f i).toHom = S := by
+  let ⟨A, A_closure⟩ := S_fg
+  let ⟨i, y, eq_y⟩ := exists_quotient_mk'_sigma_mk'_eq G _ (fun a : A ↦ a.1)
+  use i
+  use (Substructure.closure L (range y))
+  rw [Substructure.map_closure]
+  simp only [Embedding.coe_toHom, of_apply]
+  rw [← image_univ, image_image, image_univ, ← eq_y,
+    Subtype.range_coe_subtype, Finset.setOf_mem, A_closure]
+
 variable {P : Type u₁} [L.Structure P] (g : ∀ i, G i ↪[L] P)
 variable (Hg : ∀ i j hij x, g j (f i j hij x) = g i x)
 variable (L ι G f)
@@ -387,6 +409,38 @@ theorem lift_unique (F : DirectLimit G f ↪[L] P) (x) :
   DirectLimit.inductionOn x fun i x => by rw [lift_of]; rfl
 #align first_order.language.direct_limit.lift_unique FirstOrder.Language.DirectLimit.lift_unique
 
+lemma range_lift : (lift L ι G f g Hg).toHom.range = ⨆ i, (g i).toHom.range := by
+  simp_rw [Hom.range_eq_map]
+  rw [← iSup_range_of_eq_top, Substructure.map_iSup]
+  simp_rw [Hom.range_eq_map, Substructure.map_map]
+  rfl
+
+variable (L ι G f)
+variable (G' : ι → Type w') [∀ i, L.Structure (G' i)]
+variable (f' : ∀ i j, i ≤ j → G' i ↪[L] G' j)
+variable (g : ∀ i, G i ≃[L] G' i)
+variable (H_commuting : ∀ i j hij x, g j (f i j hij x) = f' i j hij (g i x))
+variable [DirectedSystem G' fun i j h => f' i j h]
+
+/-- The isomorphism between limits of isomorphic systems. -/
+noncomputable def equiv_lift : DirectLimit G f ≃[L] DirectLimit G' f' := by
+  let U i : G i ↪[L] DirectLimit G' f' := (of L _ G' f' i).comp (g i).toEmbedding
+  let F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L _ G f U <| by
+    intro _ _ _ _
+    simp only [U, Embedding.comp_apply, Equiv.coe_toEmbedding, H_commuting, of_f]
+  have surj_f : Function.Surjective F := by
+    intro x
+    rcases x with ⟨i, pre_x⟩
+    use of L _ G f i ((g i).symm pre_x)
+    simp only [F, U, lift_of, Embedding.comp_apply, Equiv.coe_toEmbedding, Equiv.apply_symm_apply]
+    rfl
+  exact ⟨Equiv.ofBijective F ⟨F.injective, surj_f⟩, F.map_fun', F.map_rel'⟩
+
+theorem equiv_lift_of {i : ι} (x : G i) :
+    equiv_lift L ι G f G' f' g H_commuting (of L ι G f i x) = of L ι G' f' i (g i x) := rfl
+
+variable {L ι G f}
+
 /-- The direct limit of countably many countably generated structures is countably generated. -/
 theorem cg {ι : Type*} [Countable ι] [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]
     {G : ι → Type w} [∀ i, L.Structure (G i)] (f : ∀ i j, i ≤ j → G i ↪[L] G j)
@@ -414,6 +468,66 @@ instance cg' {ι : Type*} [Countable ι] [Preorder ι] [IsDirected ι (· ≤ ·
 
 end DirectLimit
 
+section Substructure
+
+variable [Nonempty ι] [IsDirected ι (· ≤ ·)]
+variable {M N : Type*} [L.Structure M] [L.Structure N] (S : ι →o L.Substructure M)
+
+instance : DirectedSystem (fun i ↦ S i) (fun _ _ h ↦ Substructure.inclusion (S.monotone h)) where
+  map_self' := fun _ _ _ ↦ rfl
+  map_map' := fun _ _ _ ↦ rfl
+
+namespace DirectLimit
+
+/-- The map from a direct limit of a system of substructures of `M` into `M`. -/
+def liftInclusion :
+    DirectLimit (fun i ↦ S i) (fun _ _ h ↦ Substructure.inclusion (S.monotone h)) ↪[L] M :=
+  DirectLimit.lift L ι (fun i ↦ S i) (fun _ _ h ↦ Substructure.inclusion (S.monotone h))
+    (fun _ ↦ Substructure.subtype _) (fun _ _ _ _ ↦ rfl)
+
+theorem liftInclusion_of {i : ι} (x : S i) :
+    (liftInclusion S) (of L ι _ (fun _ _ h ↦ Substructure.inclusion (S.monotone h)) i x)
+    = Substructure.subtype (S i) x := rfl
+
+lemma rangeLiftInclusion : (liftInclusion S).toHom.range = ⨆ i, S i := by
+  simp_rw [liftInclusion, range_lift, Substructure.range_subtype]
+
+/-- The isomorphism between a direct limit of a system of substructures and their union. -/
+noncomputable def Equiv_iSup :
+    DirectLimit (fun i ↦ S i) (fun _ _ h ↦ Substructure.inclusion (S.monotone h)) ≃[L]
+    (iSup S : L.Substructure M) := by
+  have liftInclusion_in_sup : ∀ x, liftInclusion S x ∈ (⨆ i, S i) := by
+    simp only [← rangeLiftInclusion, Hom.mem_range, Embedding.coe_toHom]
+    intro x; use x
+  let F := Embedding.codRestrict (⨆ i, S i) _ liftInclusion_in_sup
+  have F_surj : Function.Surjective F := by
+    rintro ⟨m, hm⟩
+    rw [← rangeLiftInclusion, Hom.mem_range] at hm
+    rcases hm with ⟨a, _⟩; use a
+    simpa only [F, Embedding.codRestrict_apply', Subtype.mk.injEq]
+  exact ⟨Equiv.ofBijective F ⟨F.injective, F_surj⟩, F.map_fun', F.map_rel'⟩
+
+theorem Equiv_isup_of_apply {i : ι} (x : S i) :
+    Equiv_iSup S (of L ι _ (fun _ _ h ↦ Substructure.inclusion (S.monotone h)) i x)
+    = Substructure.inclusion (le_iSup _ _) x := rfl
+
+theorem Equiv_isup_symm_inclusion_apply {i : ι} (x : S i) :
+    (Equiv_iSup S).symm (Substructure.inclusion (le_iSup _ _) x)
+    = of L ι _ (fun _ _ h ↦ Substructure.inclusion (S.monotone h)) i x := by
+  apply (Equiv_iSup S).injective
+  simp only [Equiv.apply_symm_apply]
+  rfl
+
+@[simp]
+theorem Equiv_isup_symm_inclusion (i : ι) :
+    (Equiv_iSup S).symm.toEmbedding.comp (Substructure.inclusion (le_iSup _ _))
+    = of L ι _ (fun _ _ h ↦ Substructure.inclusion (S.monotone h)) i := by
+  ext x; exact Equiv_isup_symm_inclusion_apply _ x
+
+end DirectLimit
+
+end Substructure
+
 end Language
 
 end FirstOrder

Mathlib/ModelTheory/Substructures.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Aaron Anderson
+Authors: Aaron Anderson, Gabin Kolly
 -/
 import Mathlib.Order.Closure
 import Mathlib.ModelTheory.Semantics
@@ -943,6 +943,11 @@ theorem codRestrict_apply (p : L.Substructure N) (f : M ↪[L] N) {h} (x : M) :
   rfl
 #align first_order.language.embedding.cod_restrict_apply FirstOrder.Language.Embedding.codRestrict_apply
 
+@[simp]
+theorem codRestrict_apply' (p : L.Substructure N) (f : M ↪[L] N) {h} (x : M) :
+    codRestrict p f h x = ⟨f x, h x⟩ :=
+  rfl
+
 @[simp]
 theorem comp_codRestrict (f : M ↪[L] N) (g : N ↪[L] P) (p : L.Substructure P) (h : ∀ b, g b ∈ p) :
     ((codRestrict p g h).comp f : M ↪[L] p) = codRestrict p (g.comp f) fun _ => h _ :=
@@ -978,6 +983,11 @@ theorem substructureEquivMap_apply (f : M ↪[L] N) (p : L.Substructure M) (x :
   rfl
 #align first_order.language.embedding.substructure_equiv_map_apply FirstOrder.Language.Embedding.substructureEquivMap_apply
 
+@[simp]
+theorem subtype_substructureEquivMap (f : M ↪[L] N) (s : L.Substructure M) :
+    (subtype _).comp (f.substructureEquivMap s).toEmbedding = f.comp (subtype _) := by
+  ext; rfl
+
 /-- The equivalence between the domain and the range of an embedding `f`. -/
 noncomputable def equivRange (f : M ↪[L] N) : M ≃[L] f.toHom.range where
   toFun := codRestrict f.toHom.range f f.toHom.mem_range_self
@@ -994,6 +1004,10 @@ theorem equivRange_apply (f : M ↪[L] N) (x : M) : (f.equivRange x : N) = f x :
   rfl
 #align first_order.language.embedding.equiv_range_apply FirstOrder.Language.Embedding.equivRange_apply
 
+@[simp]
+theorem subtype_equivRange (f : M ↪[L] N) : (subtype _).comp f.equivRange.toEmbedding = f := by
+  ext; rfl
+
 end Embedding
 
 namespace Equiv
@@ -1013,6 +1027,9 @@ def inclusion {S T : L.Substructure M} (h : S ≤ T) : S ↪[L] T :=
   S.subtype.codRestrict _ fun x => h x.2
 #align first_order.language.substructure.inclusion FirstOrder.Language.Substructure.inclusion
 
+@[simp]
+theorem inclusion_self (S : L.Substructure M) : inclusion (le_refl S) = Embedding.refl L S := rfl
+
 @[simp]
 theorem coe_inclusion {S T : L.Substructure M} (h : S ≤ T) :
     (inclusion h : S → T) = Set.inclusion h :=