feat(ModelTheory): add CardinalLTGenerated substructure API

Author: iosephusferrum

Mathlib/ModelTheory/FinitelyGenerated.lean

@@ -74,6 +74,20 @@ theorem fg_closure {s : Set M} (hs : s.Finite) : FG (closure L s) :=
 theorem fg_closure_singleton (x : M) : FG (closure L ({x} : Set M)) :=
   fg_closure (finite_singleton x)
 
+theorem FG.cardinalLTGenerated {N : L.Substructure M} (hN : N.FG) {κ : Cardinal}
+    (hκ : Cardinal.aleph0 ≤ κ) : N.CardinalLTGenerated κ := by
+  obtain ⟨S, hS, hSN⟩ := fg_def.1 hN
+  haveI : Finite S := hS.to_subtype
+  exact ⟨S, hasCardinalLT_of_finite S κ hκ, hSN⟩
+
+theorem cardinalLTGenerated_aleph0_iff {N : L.Substructure M} :
+    N.CardinalLTGenerated Cardinal.aleph0 ↔ N.FG := by
+  constructor
+  · rintro ⟨S, hS, hSN⟩
+    rw [hasCardinalLT_aleph0_iff] at hS
+    exact fg_def.2 ⟨S, hS, hSN⟩
+  · exact fun hN ↦ hN.cardinalLTGenerated le_rfl
+
 theorem FG.sup {N₁ N₂ : L.Substructure M} (hN₁ : N₁.FG) (hN₂ : N₂.FG) : (N₁ ⊔ N₂).FG :=
   let ⟨t₁, ht₁⟩ := fg_def.1 hN₁
   let ⟨t₂, ht₂⟩ := fg_def.1 hN₂

Mathlib/ModelTheory/PartialEquiv.lean

@@ -28,9 +28,9 @@ This file defines partial isomorphisms between first-order structures.
 - `FirstOrder.Language.embedding_from_cg` shows that if structures `M` and `N` form an equivalence
   pair with `M` countably-generated, then any finite-generated partial equivalence between them
   can be extended to an embedding `M ↪[L] N`.
-- `FirstOrder.Language.equiv_from_cg` shows that if countably-generated structures `M` and `N` form
-  an equivalence pair in both directions, then any finite-generated partial equivalence between them
-  can be extended to an isomorphism `M ↪[L] N`.
+- `FirstOrder.Language.equiv_between_cg` shows that if countably-generated structures `M` and `N`
+  form an equivalence pair in both directions, then any finite-generated partial equivalence between
+  them can be extended to an isomorphism `M ≃[L] N`.
 - The proofs of these results are adapted in part from David Wärn's approach to countable dense
   linear orders, a special case of this phenomenon in the case where `L = Language.order`.
 
@@ -528,6 +528,8 @@ theorem equiv_between_cg (M_cg : Structure.CG L M) (N_cg : Structure.CG L N)
   rw [toEquivOfEqTop_toEmbedding]
   apply Embedding.toPartialEquiv_toEmbedding
 
+@[deprecated (since := "2026-06-13")] alias equiv_from_cg := equiv_between_cg
+
 end FGEquiv
 
 end Language

Mathlib/ModelTheory/Substructures.lean

@@ -9,6 +9,7 @@ public import Mathlib.Data.Fintype.Order
 public import Mathlib.Order.Closure
 public import Mathlib.ModelTheory.Semantics
 public import Mathlib.ModelTheory.Encoding
+public import Mathlib.SetTheory.Cardinal.HasCardinalLT
 
 /-!
 # First-Order Substructures
@@ -22,6 +23,8 @@ substructures appearing in the algebra library.
     substructures of the `L`-structure `M`.
 - `FirstOrder.Language.Substructure.closure` is defined so that if `s : Set M`, `closure L s` is
     the least substructure of `M` containing `s`.
+- `FirstOrder.Language.Substructure.CardinalLTGenerated` is defined so that
+    `S.CardinalLTGenerated κ` means that `S` is generated by a set of cardinality less than `κ`.
 - `FirstOrder.Language.Substructure.comap` is defined so that `s.comap f` is the preimage of the
     substructure `s` under the homomorphism `f`, as a substructure.
 - `FirstOrder.Language.Substructure.map` is defined so that `s.map f` is the image of the
@@ -376,6 +379,32 @@ theorem closure_iUnion {ι} (s : ι → Set M) : closure L (⋃ i, s i) = ⨆ i,
 theorem closure_insert (s : Set M) (m : M) : closure L (insert m s) = closure L {m} ⊔ closure L s :=
   closure_union {m} s
 
+/-- A substructure of `M` is `κ`-generated if it is the closure of a subset of cardinality
+less than `κ`. -/
+def CardinalLTGenerated (S : L.Substructure M) (κ : Cardinal) : Prop :=
+  ∃ s : Set M, HasCardinalLT s κ ∧ closure L s = S
+
+theorem cardinalLTGenerated_def {S : L.Substructure M} {κ : Cardinal} :
+    S.CardinalLTGenerated κ ↔ ∃ s : Set M, HasCardinalLT s κ ∧ closure L s = S :=
+  Iff.rfl
+
+theorem cardinalLTGenerated_closure {s : Set M} {κ : Cardinal} (hs : HasCardinalLT s κ) :
+    CardinalLTGenerated (closure L s) κ :=
+  ⟨s, hs, rfl⟩
+
+theorem cardinalLTGenerated_closure_singleton (m : M) {κ : Cardinal}
+    (hκ : Cardinal.aleph0 ≤ κ) : CardinalLTGenerated (closure L ({m} : Set M)) κ := by
+  haveI : Finite ({m} : Set M) := (finite_singleton m).to_subtype
+  exact cardinalLTGenerated_closure (hasCardinalLT_of_finite ({m} : Set M) κ hκ)
+
+theorem CardinalLTGenerated.sup {S T : L.Substructure M} {κ : Cardinal}
+    (hS : S.CardinalLTGenerated κ) (hT : T.CardinalLTGenerated κ)
+    (hκ : Cardinal.aleph0 ≤ κ) : (S ⊔ T).CardinalLTGenerated κ :=
+  let ⟨s, hs⟩ := cardinalLTGenerated_def.1 hS
+  let ⟨t, ht⟩ := cardinalLTGenerated_def.1 hT
+  cardinalLTGenerated_def.2
+    ⟨s ∪ t, hasCardinalLT_union hκ hs.1 ht.1, by rw [closure_union, hs.2, ht.2]⟩
+
 instance small_bot : Small.{u} (⊥ : L.Substructure M) := by
   rw [← closure_empty]
   haveI : Small.{u} (∅ : Set M) := small_subsingleton _
@@ -539,6 +568,14 @@ theorem map_closure (f : M →[L] N) (s : Set M) : (closure L s).map f = closure
 theorem closure_image (f : M →[L] N) : closure L (f '' s) = map f (closure L s) :=
   (map_closure f s).symm
 
+theorem CardinalLTGenerated.map {f : M →[L] N} {S : L.Substructure M} {κ : Cardinal}
+    (hS : S.CardinalLTGenerated κ) : (S.map f).CardinalLTGenerated κ := by
+  rcases hS with ⟨s, hs_card, hs⟩
+  refine ⟨f '' s, ?_, by rw [closure_image, hs]⟩
+  exact hs_card.of_surjective
+    (fun x : s ↦ ⟨f x.1, x.1, x.2, rfl⟩)
+    (by rintro ⟨_, x, hx, rfl⟩; exact ⟨⟨x, hx⟩, rfl⟩)
+
 section GaloisCoinsertion
 
 variable {ι : Type*} {f : M →[L] N}