pullback_snd_isIso_of_range_subset

English

If the range of g.base is contained in the range of f.base, then the pullback snd is an isomorphism.

Русский

Если образ g.base содержится в образе f.base, то pullback snd является изоморфизмом.

LaTeX

$$$(\mathrm{range}\,g.base) \subseteq (\mathrm{range}\,f.base) \Rightarrow \mathrm{pullback.snd}(f,g) \cong _Id$$$

Lean4

theorem pullback_snd_isIso_of_range_subset (H' : Set.range g.base ⊆ Set.range f.base) : IsIso (pullback.snd f g) :=
  by
  apply (config := { allowSynthFailures := true })
    Functor.ReflectsIsomorphisms.reflects (F := LocallyRingedSpace.forgetToSheafedSpace)
  apply (config := { allowSynthFailures := true })
    Functor.ReflectsIsomorphisms.reflects (F := SheafedSpace.forgetToPresheafedSpace)
  erw [←
    PreservesPullback.iso_hom_snd (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g]
    -- Porting note: was `inferInstance`

  exact IsIso.comp_isIso' inferInstance <| PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset _ _ H'

Похожие утверждения