feat(model_theory/language_map): Cardinality of languages with consta…

…nts (#13981)

`first_order.language.card_with_constants` shows that the cardinality of `L[[A]]` is `L.card + # A`.

src/logic/equiv/basic.lean

@@ -1244,6 +1244,14 @@ def sigma_prod_distrib {ι : Type*} (α : ι → Type*) (β : Type*) :
  λ p, by { rcases p with ⟨⟨_, _⟩, _⟩, refl },
  λ p, by { rcases p with ⟨_, ⟨_, _⟩⟩, refl }⟩
 
+/-- An equivalence that separates out the 0th fiber of `(Σ (n : ℕ), f n)`. -/
+def sigma_nat_succ (f : ℕ → Type u) :
+  (Σ n, f n) ≃ f 0 ⊕ Σ n, f (n + 1) :=
+⟨λ x, @sigma.cases_on ℕ f (λ _, f 0 ⊕ Σ n, f (n + 1)) x (λ n, @nat.cases_on (λ i, f i → (f 0 ⊕
+  Σ (n : ℕ), f (n + 1))) n (λ (x : f 0), sum.inl x) (λ (n : ℕ) (x : f n.succ), sum.inr ⟨n, x⟩)),
+  sum.elim (sigma.mk 0) (sigma.map nat.succ (λ _, id)),
+  by { rintro ⟨(n | n), x⟩; refl }, by { rintro (x | ⟨n, x⟩); refl }⟩
+
 /-- The product `bool × α` is equivalent to `α ⊕ α`. -/
 def bool_prod_equiv_sum (α : Type u) : bool × α ≃ α ⊕ α :=
 calc bool × α ≃ (unit ⊕ unit) × α       : prod_congr bool_equiv_punit_sum_punit (equiv.refl _)

src/model_theory/basic.lean

@@ -59,19 +59,45 @@ structure language :=
 (functions : ℕ → Type u) (relations : ℕ → Type v)
 
 /-- Used to define `first_order.language₂`. -/
-def sequence₂ (a₀ a₁ a₂ : Type u) : ℕ → Type u
+@[simp] def sequence₂ (a₀ a₁ a₂ : Type u) : ℕ → Type u
 | 0 := a₀
 | 1 := a₁
 | 2 := a₂
 | _ := pempty
 
-instance {a₀ a₁ a₂ : Type u} [h : inhabited a₀] : inhabited (sequence₂ a₀ a₁ a₂ 0) := h
+namespace sequence₂
+
+variables (a₀ a₁ a₂ : Type u)
+
+instance inhabited₀ [h : inhabited a₀] : inhabited (sequence₂ a₀ a₁ a₂ 0) := h
+
+instance inhabited₁ [h : inhabited a₁] : inhabited (sequence₂ a₀ a₁ a₂ 1) := h
+
+instance inhabited₂ [h : inhabited a₂] : inhabited (sequence₂ a₀ a₁ a₂ 2) := h
+
+instance {n : ℕ} : is_empty (sequence₂ a₀ a₁ a₂ (n + 3)) := pempty.is_empty
+
+@[simp] lemma lift_mk {i : ℕ} :
+  cardinal.lift (# (sequence₂ a₀ a₁ a₂ i)) = # (sequence₂ (ulift a₀) (ulift a₁) (ulift a₂) i) :=
+begin
+  rcases i with (_ | _ | _ | i);
+  simp only [sequence₂, mk_ulift, mk_fintype, fintype.card_of_is_empty, nat.cast_zero, lift_zero],
+end
+
+@[simp] lemma sum_card :
+  cardinal.sum (λ i, # (sequence₂ a₀ a₁ a₂ i)) = # a₀ + # a₁ + # a₂ :=
+begin
+  rw [sum_nat_eq_add_sum_succ, sum_nat_eq_add_sum_succ, sum_nat_eq_add_sum_succ],
+  simp [add_assoc],
+end
+
+end sequence₂
 
 namespace language
 
 /-- A constructor for languages with only constants, unary and binary functions, and
 unary and binary relations. -/
-protected def mk₂ (c f₁ f₂ : Type u) (r₁ r₂ : Type v) : language :=
+@[simps] protected def mk₂ (c f₁ f₂ : Type u) (r₁ r₂ : Type v) : language :=
 ⟨sequence₂ c f₁ f₂, sequence₂ pempty r₁ r₂⟩
 
 /-- The empty language has no symbols. -/
@@ -88,6 +114,10 @@ variable (L : language.{u v})
 /-- The type of constants in a given language. -/
 @[nolint has_inhabited_instance] protected def «constants» := L.functions 0
 
+@[simp] lemma constants_mk₂ (c f₁ f₂ : Type u) (r₁ r₂ : Type v) :
+  (language.mk₂ c f₁ f₂ r₁ r₂).constants = c :=
+rfl
+
 /-- The type of symbols in a given language. -/
 @[nolint has_inhabited_instance] def symbols := (Σl, L.functions l) ⊕ (Σl, L.relations l)
 
@@ -208,6 +238,12 @@ begin
     add_comm (cardinal.sum (λ i, (# (L'.functions i)).lift)), add_assoc, add_assoc]
 end
 
+@[simp] lemma card_mk₂ (c f₁ f₂ : Type u) (r₁ r₂ : Type v) :
+  (language.mk₂ c f₁ f₂ r₁ r₂).card =
+    cardinal.lift.{v} (# c) + cardinal.lift.{v} (# f₁) + cardinal.lift.{v} (# f₂)
+    + cardinal.lift.{u} (# r₁) + cardinal.lift.{u} (# r₂) :=
+by simp [card_eq_card_functions_add_card_relations, add_assoc]
+
 variables (L) (M : Type w)
 
 /-- A first-order structure on a type `M` consists of interpretations of all the symbols in a given

src/model_theory/bundled.lean

@@ -101,6 +101,14 @@ def ulift (M : Model.{u v w} T) : Model.{u v (max w w')} T :=
   nonempty' := M.nonempty',
   is_model := (@Lhom.on_Theory_model L L' M (φ.reduct M) _ φ _ T).1 M.is_model, }
 
+instance left_Structure {L' : language} {T : (L.sum L').Theory} (M : T.Model) :
+  L.Structure M :=
+(Lhom.sum_inl : L →ᴸ L.sum L').reduct M
+
+instance right_Structure {L' : language} {T : (L.sum L').Theory} (M : T.Model) :
+  L'.Structure M :=
+(Lhom.sum_inr : L' →ᴸ L.sum L').reduct M
+
 end Model
 
 variables {T}

src/model_theory/language_map.lean

@@ -31,7 +31,8 @@ universes u v u' v' w
 
 namespace first_order
 namespace language
-open Structure
+open Structure cardinal
+open_locale cardinal
 
 variables (L : language.{u v}) (L' : language.{u' v'}) {M : Type w} [L.Structure M]
 
@@ -257,36 +258,36 @@ end Lequiv
 section constants_on
 variables (α : Type u')
 
-/-- The function symbols of a language with constants indexed by a type. -/
-def constants_on_functions : ℕ → Type u'
-| 0 := α
-| _ := pempty
-
-instance [h : inhabited α] : inhabited (constants_on_functions α 0) := h
-
 /-- A language with constants indexed by a type. -/
-def constants_on : language.{u' 0} := ⟨constants_on_functions α, λ _, empty⟩
+@[simp] def constants_on : language.{u' 0} :=
+  language.mk₂ α pempty pempty pempty pempty
 
 variables {α}
 
-@[simp] lemma constants_on_constants : (constants_on α).constants = α := rfl
+lemma constants_on_constants : (constants_on α).constants = α := rfl
 
 instance is_algebraic_constants_on : is_algebraic (constants_on α) :=
-language.is_algebraic_of_empty_relations
+language.is_algebraic_mk₂
 
 instance is_relational_constants_on [ie : is_empty α] : is_relational (constants_on α) :=
-⟨λ n, nat.cases_on n ie (λ _, pempty.is_empty)⟩
+language.is_relational_mk₂
+
+instance is_empty_functions_constants_on_succ {n : ℕ} :
+  is_empty ((constants_on α).functions (n + 1)) :=
+nat.cases_on n pempty.is_empty (λ n, nat.cases_on n pempty.is_empty (λ _, pempty.is_empty))
+
+lemma card_constants_on : (constants_on α).card = # α :=
+by simp
 
 /-- Gives a `constants_on α` structure to a type by assigning each constant a value. -/
 def constants_on.Structure (f : α → M) : (constants_on α).Structure M :=
-{ fun_map := λ n, nat.cases_on n (λ a _, f a) (λ _, pempty.elim),
-  rel_map := λ _, empty.elim }
+Structure.mk₂ f pempty.elim pempty.elim pempty.elim pempty.elim
 
 variables {β : Type v'}
 
 /-- A map between index types induces a map between constant languages. -/
 def Lhom.constants_on_map (f : α → β) : (constants_on α) →ᴸ (constants_on β) :=
-⟨λ n, nat.cases_on n f (λ _, pempty.elim), λ n, empty.elim⟩
+Lhom.mk₂ f pempty.elim pempty.elim pempty.elim pempty.elim
 
 lemma constants_on_map_is_expansion_on {f : α → β} {fα : α → M} {fβ : β → M}
   (h : fβ ∘ f = fα) :
@@ -295,8 +296,8 @@ lemma constants_on_map_is_expansion_on {f : α → β} {fα : α → M} {fβ : 
 begin
   letI := constants_on.Structure fα,
   letI := constants_on.Structure fβ,
-  exact ⟨λ n, nat.cases_on n (λ F x, (congr_fun h F : _)) (λ n F, pempty.elim F),
-    λ _ R, empty.elim R⟩,
+  exact ⟨λ n, nat.cases_on n (λ F x, (congr_fun h F : _)) (λ n F, is_empty_elim F),
+    λ _ R, is_empty_elim R⟩
 end
 
 end constants_on
@@ -313,6 +314,10 @@ def with_constants : language.{(max u w) v} := L.sum (constants_on α)
 
 localized "notation L`[[`:95 α`]]`:90 := L.with_constants α" in first_order
 
+@[simp] lemma card_with_constants :
+  (L[[α]]).card = cardinal.lift.{w} L.card + cardinal.lift.{max u v} (# α) :=
+by rw [with_constants, card_sum, card_constants_on]
+
 /-- The language map adding constants.  -/
 @[simps] def Lhom_with_constants : L →ᴸ L[[α]] := Lhom.sum_inl
 

src/model_theory/substructures.lean

@@ -603,7 +603,7 @@ def with_constants (S : L.substructure M) {A : set M} (h : A ⊆ S) : L[[A]].sub
     { exact S.fun_mem f },
     { cases n,
       { exact λ _ _, h f.2 },
-      { exact pempty.elim f } }
+      { exact is_empty_elim f } }
   end }
 
 variables {A : set M} {s : set M} (h : A ⊆ S)

src/set_theory/cardinal/basic.lean

@@ -696,6 +696,13 @@ begin
   exact sum_le_sum _ _ (le_sup _)
 end
 
+theorem sum_nat_eq_add_sum_succ (f : ℕ → cardinal.{u}) :
+  cardinal.sum f = f 0 + cardinal.sum (λ i, f (i + 1)) :=
+begin
+  refine (equiv.sigma_nat_succ (λ i, quotient.out (f i))).cardinal_eq.trans _,
+  simp only [mk_sum, mk_out, lift_id, mk_sigma],
+end
+
 theorem sup_eq_zero {ι} {f : ι → cardinal} [is_empty ι] : sup f = 0 :=
 by { rw ←nonpos_iff_eq_zero, exact sup_le is_empty_elim }