English
The topology on the pullback is the infimum (i.e., the meet) of the induced topologies from the two projections to X and Y.
Русский
Топология на пределе равна наименьшему из топологий, индуцируемых двумя проекциям на X и Y.
LaTeX
$$$ (pullback f g).str = \operatorname{induced} (pullback.fst f g) X.str \; \inf \; \operatorname{induced} (pullback.snd f g) Y.str $$$
Lean4
theorem pullback_topology {X Y Z : TopCat.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) :
(pullback f g).str = induced (pullback.fst f g) X.str ⊓ induced (pullback.snd f g) Y.str :=
by
let homeo := homeoOfIso (pullbackIsoProdSubtype f g)
refine homeo.isInducing.eq_induced.trans ?_
change induced homeo (induced _ ((induced Prod.fst X.str) ⊓ (induced Prod.snd Y.str))) = _
simp only [induced_compose, induced_inf]
rfl
