English
If the base map is epi, the open immersion is an iso. (Alternative presentation).
Русский
Если основание эпиморфно, открытое вложение является изоморфизмом.
LaTeX
$$IsIso f [h' : Epi f.base]$$
Lean4
theorem pullbackConeOfLeftLift_fst : pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst = s.fst := by
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` did not pick up `NatTrans.ext`
refine PresheafedSpace.Hom.ext _ _ ?_ <| NatTrans.ext <| funext fun x => ?_
· change pullback.lift _ _ _ ≫ pullback.fst _ _ = _
simp
· induction x with
| op x => ?_
change ((_ ≫ _) ≫ _ ≫ _) ≫ _ = _
simp_rw [Category.assoc]
erw [← s.pt.presheaf.map_comp]
erw [s.snd.c.naturality_assoc]
have := congr_app s.condition (op (opensFunctor f |>.obj x))
dsimp only [comp_c_app, unop_op] at this
rw [← IsIso.comp_inv_eq] at this
replace this := reassoc_of% this
erw [← this, hf.invApp_app_assoc, s.fst.c.naturality_assoc]
simp [eqToHom_map]
-- this lemma is not a `simp` lemma, because it is an implementation detail
