exists_cg_is_age_of — Mathlib

English

Under suitable hypotheses there exists a countably generated structure M such that L.age M = K.

Русский

При выполнении условий существует счетно-сгенерированная структура M такова, что возраст M равен K.

LaTeX

$$$\exists M : Bundled L.Structure,\; \mathrm{CG}_L(M) \land \mathrm{age}_L(M) = K$$$

Lean4

/-- Sufficient conditions for a class to be the age of a countably-generated structure. -/
theorem exists_cg_is_age_of (hn : K.Nonempty) (hc : (Quotient.mk' '' K).Countable)
    (fg : ∀ M : Bundled.{w} L.Structure, M ∈ K → Structure.FG L M) (hp : Hereditary K) (jep : JointEmbedding K) :
    ∃ M : Bundled.{w} L.Structure, Structure.CG L M ∧ L.age M = K :=
  by
  obtain ⟨F, hF⟩ := hc.exists_eq_range (hn.image _)
  simp only [Set.ext_iff, Quotient.forall, mem_image, mem_range] at hF
  simp_rw [Quotient.eq_mk_iff_out] at hF
  have hF' : ∀ n : ℕ, (F n).out ∈ K := by
    intro n
    obtain ⟨P, hP1, hP2⟩ :=
      (hF (F n).out).2
        ⟨n, Setoid.refl _⟩
          -- Porting note: fix hP2 because `Quotient.out (Quotient.mk' x) ≈ a` was not simplified
              -- to `x ≈ a` in hF

    replace hP2 := Setoid.trans (Setoid.symm (Quotient.mk_out P)) hP2
    exact (hp.is_equiv_invariant_of_fg fg _ _ hP2).1 hP1
  choose P hPK hP hFP using fun (N : K) (n : ℕ) => jep N N.2 (F (n + 1)).out (hF' _)
  let G : ℕ → K :=
    @Nat.rec (fun _ => K) ⟨(F 0).out, hF' 0⟩ fun n N =>
      ⟨P N n, hPK N n⟩
        -- Porting note: was
          -- let f : ∀ i j, i ≤ j → G i ↪[L] G j := DirectedSystem.natLeRec fun n => (hP _ n).some

  let f : ∀ (i j : ℕ), i ≤ j → (G i).val ↪[L] (G j).val :=
    by
    refine DirectedSystem.natLERec (G' := fun i => (G i).val) (L := L) ?_
    dsimp only [G]
    exact fun n => (hP _ n).some
  have : DirectedSystem (fun n ↦ (G n).val) fun i j h ↦ ↑(f i j h) := by dsimp [f, G]; infer_instance
  refine ⟨Bundled.of (@DirectLimit L _ _ (fun n ↦ (G n).val) _ f _ _), ?_, ?_⟩
  · exact DirectLimit.cg _ (fun n => (fg _ (G n).2).cg)
  · refine
      (age_directLimit (fun n ↦ (G n).val) f).trans
        (subset_antisymm (iUnion_subset fun n N hN => hp (G n).val (G n).2 hN) fun N KN => ?_)
    have : Quotient.out (Quotient.mk' N) ≈ N := Quotient.eq_mk_iff_out.mp rfl
    obtain ⟨n, ⟨e⟩⟩ := (hF N).1 ⟨N, KN, this⟩
    refine mem_iUnion_of_mem n ⟨fg _ KN, ⟨Embedding.comp ?_ e.symm.toEmbedding⟩⟩
    rcases n with - | n
    · dsimp [G]; exact Embedding.refl _ _
    · dsimp [G]; exact (hFP _ n).some

Похожие утверждения