English
The IsBase for comap is equivalent to certain image-based and injectivity conditions.
Русский
IsBase для comap эквивалентно условиям, зависящим от образа и инъективности.
LaTeX
$$(N.comap f).IsBase B \iff N.IsBasis (f '' B) (f '' (f^{-1}' N.E)) ∧ B.InjOn f ∧ B ⊆ f^{-1}' N.E$$
Lean4
@[simp]
theorem comap_isBasis_iff {I X : Set α} : (N.comap f).IsBasis I X ↔ N.IsBasis (f '' I) (f '' X) ∧ I.InjOn f ∧ I ⊆ X :=
by
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· obtain ⟨hI, hinj⟩ := comap_indep_iff.1 h.indep
refine ⟨hI.isBasis_of_forall_insert (image_mono h.subset) fun e he ↦ ?_, hinj, h.subset⟩
simp only [mem_diff, mem_image, not_exists, not_and] at he
obtain ⟨⟨e, heX, rfl⟩, he⟩ := he
have heI : e ∉ I := fun heI ↦ (he e heI rfl)
replace h := h.insert_dep ⟨heX, heI⟩
simp only [comap_dep_iff, image_insert_eq, or_iff_not_imp_right, injOn_insert heI, hinj, mem_image, not_exists,
not_and, true_and, not_forall, not_not] at h
exact h (fun _ ↦ he)
refine Indep.isBasis_of_forall_insert ?_ h.2.2 fun e ⟨heX, heI⟩ ↦ ?_
· simp [comap_indep_iff, h.1.indep, h.2]
have hIE : insert e I ⊆ (N.comap f).E :=
by
simp_rw [comap_ground_eq, ← image_subset_iff]
exact (image_mono (insert_subset heX h.2.2)).trans h.1.subset_ground
suffices N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e by
simpa [← not_indep_iff hIE, injOn_insert heI, h.2.1, image_insert_eq]
exact h.1.mem_of_insert_indep (mem_image_of_mem f heX)
