feat(model_theory/substructures): More operations on substructures (#11906)

Defines the substructure `first_order.language.hom.range`.
Defines the homomorphisms `first_order.language.hom.dom_restrict` and `first_order.language.hom.cod_restrict`, and the embeddings `first_order.language.embedding.dom_restrict`, `first_order.language.embedding.cod_restrict` which restrict the domain or codomain of a first-order hom or embedding to a substructure.
Defines the embedding `first_order.language.substructure.inclusion` between nested substructures.

Author: awainverse

src/model_theory/basic.lean

@@ -257,6 +257,10 @@ instance : inhabited (M ↪[L] M) := ⟨refl L M⟩
 lemma comp_assoc (f : M ↪[L] N) (g : N ↪[L] P) (h : P ↪[L] Q) :
   (h.comp g).comp f = h.comp (g.comp f) := rfl
 
+@[simp] lemma comp_to_hom (hnp : N ↪[L] P) (hmn : M ↪[L] N) :
+  (hnp.comp hmn).to_hom = hnp.to_hom.comp hmn.to_hom :=
+by { ext, simp only [coe_to_hom, comp_apply, hom.comp_apply] }
+
 end embedding
 
 namespace equiv

src/model_theory/substructures.lean

@@ -21,6 +21,13 @@ the least substructure of `M` containing `s`.
 substructure `s` under the homomorphism `f`, as a substructure.
 * `first_order.language.substructure.map` is defined so that `s.map f` is the image of the
 substructure `s` under the homomorphism `f`, as a substructure.
+* `first_order.language.hom.range` is defined so that `f.map` is the range of the
+the homomorphism `f`, as a substructure.
+* `first_order.language.hom.dom_restrict` and `first_order.language.hom.cod_restrict` restrict
+the domain and codomain respectively of first-order homomorphisms to substructures.
+* `first_order.language.embedding.dom_restrict` and `first_order.language.embedding.cod_restrict`
+restrict the domain and codomain respectively of first-order embeddings to substructures.
+* `first_order.language.substructure.inclusion` is the inclusion embedding between substructures.
 
 ## Main Results
 * `L.substructure M` forms a `complete_lattice`.
@@ -356,6 +363,15 @@ lemma comap_infi {ι : Sort*} (f : M →[L] N) (s : ι → L.substructure N) :
 @[simp] lemma map_id (S : L.substructure M) : S.map (hom.id L M) = S :=
 ext (λ x, ⟨λ ⟨_, h, rfl⟩, h, λ h, ⟨_, h, rfl⟩⟩)
 
+lemma map_closure (f : M →[L] N) (s : set M) :
+  (closure L s).map f = closure L (f '' s) :=
+eq.symm $ closure_eq_of_le (set.image_subset f subset_closure) $ map_le_iff_le_comap.2 $
+  closure_le.2 $ λ x hx, subset_closure ⟨x, hx, rfl⟩
+
+@[simp] lemma closure_image (f : M →[L] N) :
+  closure L (f '' s) = map f (closure L s) :=
+(map_closure f s).symm
+
 section galois_coinsertion
 
 variables {ι : Type*} {f : M →[L] N} (hf : function.injective f)
@@ -480,6 +496,67 @@ namespace hom
 
 open substructure
 
+/-- The restriction of a first-order hom to a substructure `s ⊆ M` gives a hom `s → N`. -/
+@[simps] def dom_restrict (f : M →[L] N) (p : L.substructure M) : p →[L] N :=
+f.comp p.subtype.to_hom
+
+/-- A first-order hom `f : M → N` whose values lie in a substructure `p ⊆ N` can be restricted to a
+hom `M → p`. -/
+@[simps] def cod_restrict (p : L.substructure N) (f : M →[L] N) (h : ∀c, f c ∈ p) : M →[L] p :=
+{ to_fun := λc, ⟨f c, h c⟩,
+  map_rel' := λ n R x h, f.map_rel R x h }
+
+@[simp] lemma comp_cod_restrict (f : M →[L] N) (g : N →[L] P) (p : L.substructure P)
+  (h : ∀b, g b ∈ p) :
+  ((cod_restrict p g h).comp f : M →[L] p) = cod_restrict p (g.comp f) (assume b, h _) :=
+ext $ assume b, rfl
+
+@[simp] lemma subtype_comp_cod_restrict (f : M →[L] N) (p : L.substructure N) (h : ∀b, f b ∈ p) :
+  p.subtype.to_hom.comp (cod_restrict p f h) = f :=
+ext $ assume b, rfl
+
+/-- The range of a first-order hom `f : M → N` is a submodule of `N`.
+See Note [range copy pattern]. -/
+def range (f : M →[L] N) : L.substructure N :=
+(map f ⊤).copy (set.range f) set.image_univ.symm
+
+theorem range_coe (f : M →[L] N) :
+  (range f : set N) = set.range f := rfl
+
+@[simp] theorem mem_range
+  {f : M →[L] N} {x} : x ∈ range f ↔ ∃ y, f y = x :=
+iff.rfl
+
+lemma range_eq_map
+  (f : M →[L] N) : f.range = map f ⊤ :=
+by { ext, simp }
+
+theorem mem_range_self
+  (f : M →[L] N) (x : M) : f x ∈ f.range := ⟨x, rfl⟩
+
+@[simp] theorem range_id : range (id L M) = ⊤ :=
+set_like.coe_injective set.range_id
+
+theorem range_comp (f : M →[L] N) (g : N →[L] P) :
+  range (g.comp f : M →[L] P) = map g (range f) :=
+set_like.coe_injective (set.range_comp g f)
+
+theorem range_comp_le_range (f : M →[L] N) (g : N →[L] P) :
+  range (g.comp f : M →[L] P) ≤ range g :=
+set_like.coe_mono (set.range_comp_subset_range f g)
+
+theorem range_eq_top {f : M →[L] N} :
+  range f = ⊤ ↔ function.surjective f :=
+by rw [set_like.ext'_iff, range_coe, coe_top, set.range_iff_surjective]
+
+lemma range_le_iff_comap {f : M →[L] N} {p : L.substructure N} :
+  range f ≤ p ↔ comap f p = ⊤ :=
+by rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]
+
+lemma map_le_range {f : M →[L] N} {p : L.substructure M} :
+  map f p ≤ range f :=
+set_like.coe_mono (set.image_subset_range f p)
+
 /-- The substructure of elements `x : M` such that `f x = g x` -/
 def eq_locus (f g : M →[L] N) : substructure L M :=
 { carrier := {x : M | f x = g x},
@@ -504,5 +581,101 @@ eq_of_eq_on_top $ hs ▸ eq_on_closure h
 
 end hom
 
+namespace embedding
+open substructure
+
+/-- The restriction of a first-order embedding to a substructure `s ⊆ M` gives an embedding `s → N`.
+-/
+def dom_restrict (f : M ↪[L] N) (p : L.substructure M) : p ↪[L] N :=
+  f.comp p.subtype
+
+@[simp] lemma dom_restrict_apply (f : M ↪[L] N) (p : L.substructure M) (x : p) :
+  f.dom_restrict p x = f x := rfl
+
+/-- A first-order embedding `f : M → N` whose values lie in a substructure `p ⊆ N` can be restricted
+to an embedding `M → p`. -/
+def cod_restrict (p : L.substructure N) (f : M ↪[L] N) (h : ∀c, f c ∈ p) : M ↪[L] p :=
+{ to_fun := f.to_hom.cod_restrict p h,
+  inj' := λ a b ab, f.injective (subtype.mk_eq_mk.1 ab),
+  map_fun' := λ n F x, (f.to_hom.cod_restrict p h).map_fun' F x,
+  map_rel' := λ n r x, begin
+    simp only,
+    rw [← p.subtype.map_rel, function.comp.assoc],
+    change rel_map r ((hom.comp p.subtype.to_hom (f.to_hom.cod_restrict p h)) ∘ x) ↔ _,
+    rw [hom.subtype_comp_cod_restrict, ← f.map_rel],
+    refl,
+  end }
+
+@[simp] theorem cod_restrict_apply (p : L.substructure N) (f : M ↪[L] N) {h} (x : M) :
+  (cod_restrict p f h x : N) = f x := rfl
+
+@[simp] lemma comp_cod_restrict (f : M ↪[L] N) (g : N ↪[L] P) (p : L.substructure P)
+  (h : ∀b, g b ∈ p) :
+  ((cod_restrict p g h).comp f : M ↪[L] p) = cod_restrict p (g.comp f) (assume b, h _) :=
+ext $ assume b, rfl
+
+@[simp] lemma subtype_comp_cod_restrict (f : M ↪[L] N) (p : L.substructure N) (h : ∀b, f b ∈ p) :
+  p.subtype.comp (cod_restrict p f h) = f :=
+ext $ assume b, rfl
+
+/-- The equivalence between a substructure `s` and its image `s.map f.to_hom`, where `f` is an
+  embedding. -/
+noncomputable def substructure_equiv_map (f : M ↪[L] N) (s : L.substructure M) :
+  s ≃[L] s.map f.to_hom :=
+{ to_fun := cod_restrict (s.map f.to_hom) (f.dom_restrict s) (λ ⟨m, hm⟩, ⟨m, hm, rfl⟩),
+  inv_fun := λ n, ⟨classical.some n.2, (classical.some_spec n.2).1⟩,
+  left_inv := λ ⟨m, hm⟩, subtype.mk_eq_mk.2 (f.injective ((classical.some_spec (cod_restrict
+    (s.map f.to_hom) (f.dom_restrict s) (λ ⟨m, hm⟩, ⟨m, hm, rfl⟩) ⟨m, hm⟩).2).2)),
+  right_inv := λ ⟨n, hn⟩, subtype.mk_eq_mk.2 (classical.some_spec hn).2 }
+
+@[simp] lemma substructure_equiv_map_apply (f : M ↪[L] N) (p : L.substructure M) (x : p) :
+  (f.substructure_equiv_map p x : N) = f x := rfl
+
+/-- The equivalence between the domain and the range of an embedding `f`. -/
+noncomputable def equiv_range (f : M ↪[L] N) :
+  M ≃[L] f.to_hom.range :=
+{ to_fun := cod_restrict f.to_hom.range f f.to_hom.mem_range_self,
+  inv_fun := λ n, classical.some n.2,
+  left_inv := λ m, f.injective (classical.some_spec (cod_restrict f.to_hom.range f
+    f.to_hom.mem_range_self m).2),
+  right_inv := λ ⟨n, hn⟩, subtype.mk_eq_mk.2 (classical.some_spec hn) }
+
+@[simp] lemma equiv_range_apply (f : M ↪[L] N) (x : M) :
+  (f.equiv_range x : N) = f x := rfl
+
+end embedding
+
+namespace equiv
+
+lemma to_hom_range (f : M ≃[L] N) :
+  f.to_hom.range = ⊤ :=
+begin
+  ext n,
+  simp only [hom.mem_range, coe_to_hom, substructure.mem_top, iff_true],
+  exact ⟨f.symm n, apply_symm_apply _ _⟩
+end
+
+end equiv
+
+namespace substructure
+
+/-- The embedding associated to an inclusion of substructures. -/
+def inclusion {S T : L.substructure M} (h : S ≤ T) : S ↪[L] T :=
+S.subtype.cod_restrict _ (λ x, h x.2)
+
+@[simp] lemma coe_inclusion {S T : L.substructure M} (h : S ≤ T) :
+  (inclusion h : S → T) = set.inclusion h := rfl
+
+lemma range_subtype (S : L.substructure M) : S.subtype.to_hom.range = S :=
+begin
+  ext x,
+  simp only [hom.mem_range, embedding.coe_to_hom, coe_subtype],
+  refine ⟨_, λ h, ⟨⟨x, h⟩, rfl⟩⟩,
+  rintros ⟨⟨y, hy⟩, rfl⟩,
+  exact hy,
+end
+
+end substructure
+
 end language
 end first_order