English
A simplification congruence for lifts: equality of f forms yields equality of lifts.
Русский
Упрощенное свойство равенств для подъемов: равенство f порождает равенство lift.
LaTeX
$$$ lift_f\; g \; H' = lift_{f'}\; g' \; H'' $ under appropriate equalities$$
Lean4
theorem lift_range (H' : Set.range g.base ⊆ Set.range f.base) :
Set.range (lift f g H').base = f.base ⁻¹' Set.range g.base :=
by
have := pullback_snd_isIso_of_range_subset f g H'
dsimp only [lift]
have : _ = (pullback.fst f g).base :=
PreservesPullback.iso_hom_fst (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _) f g
rw [LocallyRingedSpace.comp_base, ← this, ← Category.assoc, TopCat.coe_comp, Set.range_comp, Set.range_eq_univ.mpr,
Set.image_univ]
· rw [TopCat.pullback_fst_range]
ext
constructor
· rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩
· rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩
· rw [← TopCat.epi_iff_surjective,
show (inv (pullback.snd f g)).base = _ from
(LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _).map_inv _]
infer_instance
