image_comp — Mathlib

English

If a set s of β → M is definable over A in the language L, then its image under precomposition with a map f: α → β, viewed as a subset of α → M, is also definable over A.

Русский

Если множество s ⊆ β → M определяется над A в языке L, то образ подстановки через f: α → β, как множество α → M, также определимо над A.

LaTeX

$$$A\text{Definable}_L s \Rightarrow A\text{Definable}_L\left(\left(\lambda g: \beta \to M,\ g\circ f\right) '' s\right).$$$

Lean4

/-- Shows that definability is closed under finite projections. -/
theorem image_comp {s : Set (β → M)} (h : A.Definable L s) (f : α → β) [Finite α] [Finite β] :
    A.Definable L ((fun g : β → M => g ∘ f) '' s) := by
  classical
  cases nonempty_fintype α
  cases nonempty_fintype β
  have h :=
    (((h.image_comp_equiv (Equiv.Set.sumCompl (range f))).image_comp_equiv
              (Equiv.sumCongr (_root_.Equiv.refl _) (Fintype.equivFin _).symm)).image_comp_sumInl_fin
          _).preimage_comp
      (rangeSplitting f)
  have h' : A.Definable L {x : α → M | ∀ a, x a = x (rangeSplitting f (rangeFactorization f a))} :=
    by
    have h' : ∀ a, A.Definable L {x : α → M | x a = x (rangeSplitting f (rangeFactorization f a))} :=
      by
      refine fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext ?_⟩
      simp
    refine (congr rfl (ext ?_)).mp (definable_biInter_finset h' Finset.univ)
    simp
  refine (congr rfl (ext fun x => ?_)).mp (h.inter h')
  simp only [mem_inter_iff, mem_preimage, mem_image, exists_exists_and_eq_and, mem_setOf_eq]
  constructor
  · rintro ⟨⟨y, ys, hy⟩, hx⟩
    refine ⟨y, ys, ?_⟩
    ext a
    rw [hx a, ← Function.comp_apply (f := x), ← hy]
    simp
  · rintro ⟨y, ys, rfl⟩
    refine ⟨⟨y, ys, ?_⟩, fun a => ?_⟩
    · ext
      simp [Set.apply_rangeSplitting f]
    · rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f, rangeFactorization_coe]

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