Elementary embeddings of models of ZF

This module defines nontrivial elementary embeddings of a model of ZF into itself, their critical points, and the basic properties of the iterates of the critical point.

class NontrivialElementaryEmbedding (M : Type u_1) [ZFStructure M] extends 𝓛ZF.ElementaryEmbedding M M : Type u_1

The NontrivialElementaryEmbedding type.

• toFun : M → M
• map_formula' ⦃n : ℕ⦄ (φ : 𝓛ZF.Formula (Fin n)) (x : Fin n → M) : φ.Realize (↑self.toElementaryEmbedding ∘ x) ↔ φ.Realize x
• nontrivial' : self.toElementaryEmbedding ≠ FirstOrder.Language.ElementaryEmbedding.refl 𝓛ZF M

@[implicit_reducible]

instance NontrivialElementaryEmbedding.instFunLike {M : Type u_1} [ZFStructure M] : FunLike (NontrivialElementaryEmbedding M) M M

Equations

• NontrivialElementaryEmbedding.instFunLike = { coe := fun (j : NontrivialElementaryEmbedding M) => ⇑j.toElementaryEmbedding, coe_injective := ⋯ }

theorem NontrivialElementaryEmbedding.ext {M : Type u_1} [ZFStructure M] {j k : NontrivialElementaryEmbedding M} (eq : ∀ (x : M), j x = k x) : j = k

theorem NontrivialElementaryEmbedding.ext_iff {M : Type u_1} [ZFStructure M] {j k : NontrivialElementaryEmbedding M} : j = k ↔ ∀ (x : M), j x = k x

instance NontrivialElementaryEmbedding.instElementaryEmbeddingClass {M : Type u_1} [ZFStructure M] : ElementaryEmbeddingClass (NontrivialElementaryEmbedding M) M M

theorem NontrivialElementaryEmbedding.nontrivial {M : Type u_1} [ZFStructure M] {j : NontrivialElementaryEmbedding M} : ∃ (x : M), j x ≠ x

theorem SetTheory.IsOrdinal.le_j {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {F : Type u_1} [FunLike F M M] [ElementaryEmbeddingClass F M M] {j : F} {α : M} (ord_α : IsOrdinal α) : α ≤ j α

theorem SetTheory.j_natCast {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {F : Type u_1} [FunLike F M M] [ElementaryEmbeddingClass F M M] {j : F} (n : ℕ) : j ↑n = ↑n

theorem SetTheory.j_eq_of_mem_ωₛ {M₀ : Type 1} [ZFStructure M₀] [hM₀ : IsVonNeumannWithOmega M₀] {F₀ : Type u_1} [FunLike F₀ M₀ M₀] [ElementaryEmbeddingClass F₀ M₀ M₀] {j₀ : F₀} {α : M₀} (hα : α ∈ ωₘ) : j₀ α = α

theorem SetTheory.crit_exists {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {j : NontrivialElementaryEmbedding M} : ∃ (α : M), IsOrdinal α ∧ j α ≠ α

noncomputable def SetTheory.crit {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (j : NontrivialElementaryEmbedding M) : M

The crit declaration.

Equations

• SetTheory.crit j = sInf {α : M | j α ≠ α ∧ SetTheory.IsOrdinal α}

theorem SetTheory.crit_eq_ordinal_sInf {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {j : NontrivialElementaryEmbedding M} : crit j = ↑(sInf {α : Ordinals M | j ↑α ≠ ↑α})

@[simp]

theorem SetTheory.isOrdinal_crit {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {j : NontrivialElementaryEmbedding M} : IsOrdinal (crit j)

theorem SetTheory.j_crit_ne_crit {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {j : NontrivialElementaryEmbedding M} : j (crit j) ≠ crit j

theorem SetTheory.crit_mem_j_crit {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {j : NontrivialElementaryEmbedding M} : crit j ∈ j (crit j)

theorem SetTheory.j_eq_of_mem_crit {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {j : NontrivialElementaryEmbedding M} {α : M} (hα : α ∈ crit j) : j α = α

theorem SetTheory.j_ne_crit {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {j : NontrivialElementaryEmbedding M} {α : M} : j α ≠ crit j

theorem SetTheory.isStrongLimit_crit {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {j : NontrivialElementaryEmbedding M} : IsStrongLimit (crit j)

theorem SetTheory.ωₘ_le_crit {M₀ : Type 1} [ZFStructure M₀] [hM₀ : IsVonNeumannWithOmega M₀] {j₀ : NontrivialElementaryEmbedding M₀} : ωₘ ≤ crit j₀

theorem SetTheory.isOrdinal_crit_iter {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {j : NontrivialElementaryEmbedding M} (n : ℕ) : IsOrdinal ((⇑j)^[n] (crit j))

theorem SetTheory.crit_iter_mem_succ {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {j : NontrivialElementaryEmbedding M} (n : ℕ) : (⇑j)^[n] (crit j) ∈ (⇑j)^[n + 1] (crit j)

theorem SetTheory.crit_iter_lt_succ {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {j : NontrivialElementaryEmbedding M} (n : ℕ) : (⇑j)^[n] (crit j) < (⇑j)^[n + 1] (crit j)

theorem SetTheory.isStrongLimit_crit_iter {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] {j : NontrivialElementaryEmbedding M} (n : ℕ) : IsStrongLimit ((⇑j)^[n] (crit j))

@[reducible]

def SetTheory.hasOmegaOfNontrivialSelfEmbedding {M : Type 1} [ZFStructure M] [hM : IsVonNeumann M] (j : NontrivialElementaryEmbedding M) : IsVonNeumannWithOmega M

The hasOmegaOfNontrivialSelfEmbedding declaration.

Equations

• One or more equations did not get rendered due to their size.