English
If S Semiconjugates to T via φ, then a dynamical cover of T on φ''F with V preimage corresponds to a dynamical cover of S on F with a larger entourage; i.e., there exists s with IsDynCoverOf S F ((map φ φ)⁻¹' (V○V)) n s and s.card ≤ t.card.
Русский
Если S и T связаны через полином φ, то покрытие DynCover по T на φ''F с V-преобразованием соответствует DynCover по S на F с более крупной окрестностью; существует s такое, что IsDynCoverOf S F ((map φ φ)⁻¹'(V○V)) n s и card s ≤ card t.
LaTeX
$$$\exists s:\ Finset X,\IsDynCoverOf S F ((map φ φ)^{-1}'(V\circ V))\ n\ s\wedge s.card\le t.card$$$
Lean4
theorem preimage (h : Semiconj φ S T) {F : Set X} {V : Set (Y × Y)} (V_symm : IsSymmetricRel V) {n : ℕ} {t : Finset Y}
(h' : IsDynCoverOf T (φ '' F) V n t) :
∃ s : Finset X, IsDynCoverOf S F ((map φ φ) ⁻¹' (V ○ V)) n s ∧ s.card ≤ t.card := by
classical
rcases isEmpty_or_nonempty X with _ | _
·
exact
⟨∅, eq_empty_of_isEmpty F ▸ ⟨isDynCoverOf_empty, Finset.card_empty ▸ zero_le t.card⟩⟩
-- If `t` is a dynamical cover of `φ '' F`, then we want to choose one preimage by `φ` for each
-- element of `t`. This is complicated by the fact that `t` may not be a subset of `φ '' F`,
-- and may not even be in the range of `φ`. Hence, we first modify `t` to make it a subset
-- of `φ '' F`. This requires taking larger entourages.
obtain ⟨s, s_cover, s_card, s_inter⟩ := h'.nonempty_inter
choose! g gs_cover using fun (x : Y) (h : x ∈ s) ↦ nonempty_def.1 (s_inter x h)
choose! f f_section using fun (y : Y) (a : y ∈ φ '' F) ↦ a
refine ⟨s.image (f ∘ g), ?_, Finset.card_image_le.trans s_card⟩
simp only [IsDynCoverOf, Finset.mem_coe, image_subset_iff, preimage_iUnion₂] at s_cover ⊢
apply s_cover.trans
rw [← h.preimage_dynEntourage (V ○ V) n, Finset.set_biUnion_finset_image]
refine iUnion₂_mono fun i i_s ↦ ?_
rw [comp_apply, ball_preimage, (f_section (g i) (gs_cover i i_s).2).2]
refine preimage_mono fun x x_i ↦ mem_ball_dynEntourage_comp T n V_symm x (g i) ⟨i, ?_⟩
replace gs_cover := (gs_cover i i_s).1
rw [mem_ball_symmetry (V_symm.dynEntourage T n)] at x_i gs_cover
exact ⟨x_i, gs_cover⟩
