English
If i3 is mono and f1,i1,f2,i2,g1,g2 satisfy compatibility eqs, then the image of pullback.map equals the intersection of two preimages: over fst with range i1 and over snd with range i2.
Русский
Пусть i3 моно, а сопряжённые условия eq1, eq2 выполняются; тогда образ map-предела равен пересечению двух прообразов: fst^{-1}(range i1) ∩ snd^{-1}(range i2).
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
/-- The pullback along an embedding is (isomorphic to) the preimage. -/
noncomputable def pullbackHomeoPreimage {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
(f : X → Z) (hf : Continuous f) (g : Y → Z) (hg : IsEmbedding g) :
{ p : X × Y // f p.1 = g p.2 } ≃ₜ f ⁻¹' Set.range g
where
toFun := fun x ↦ ⟨x.1.1, _, x.2.symm⟩
invFun := fun x ↦ ⟨⟨x.1, Exists.choose x.2⟩, (Exists.choose_spec x.2).symm⟩
left_inv := by
intro x
ext <;> dsimp
apply hg.injective
convert x.prop
exact Exists.choose_spec (p := fun y ↦ g y = f (↑x : X × Y).1) _
continuous_toFun := by fun_prop
continuous_invFun := by
apply Continuous.subtype_mk
refine continuous_subtype_val.prodMk <| hg.isInducing.continuous_iff.mpr ?_
convert hf.comp continuous_subtype_val
ext x
exact Exists.choose_spec x.2
