English
Same range-description phenomenon for the general pullback map, expressing the image as a meet of two preimages.
Русский
Повторное описание образа общего отображения пределa как пересечение двух прообразов.
LaTeX
$$$ \operatorname{range}( \mathrm{pullback.map} f_1 f_2 g_1 g_2 i_1 i_2 i_3 eq_1 eq_2 ) = (\mathrm{pullback.fst} g_1 g_2)^{-1}(\operatorname{range} i_1) \cap (\mathrm{pullback.snd} g_1 g_2)^{-1}(\operatorname{range} i_2) $$$
Lean4
/-- If the map `S ⟶ T` is mono, then there is a description of the image of `W ×ₛ X ⟶ Y ×ₜ Z`. -/
theorem range_pullback_map {W X Y Z S T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) (i₁ : W ⟶ Y)
(i₂ : X ⟶ Z) (i₃ : S ⟶ T) [H₃ : Mono i₃] (eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁) (eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) :
Set.range (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) =
(pullback.fst g₁ g₂) ⁻¹' Set.range i₁ ∩ (pullback.snd g₁ g₂) ⁻¹' Set.range i₂ :=
by
ext
constructor
· rintro ⟨y, rfl⟩
simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_range]
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply]
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
exact ⟨exists_apply_eq_apply _ _, exists_apply_eq_apply _ _⟩
rintro ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩⟩
have : f₁ x₁ = f₂ x₂ := by
apply (TopCat.mono_iff_injective _).mp H₃
rw [← ConcreteCategory.comp_apply, eq₁, ← ConcreteCategory.comp_apply, eq₂, ConcreteCategory.comp_apply,
ConcreteCategory.comp_apply, hx₁, hx₂, ← ConcreteCategory.comp_apply, pullback.condition,
ConcreteCategory.comp_apply]
use (pullbackIsoProdSubtype f₁ f₂).inv ⟨⟨x₁, x₂⟩, this⟩
apply Concrete.limit_ext
rintro (_ | _ | _) <;> rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply]
· simp [hx₁, ← limit.w _ WalkingCospan.Hom.inl]
· simp [hx₁]
· simp [hx₂]
