pullbackRestrictIsoRestrict_inv_fst

English

In the pullback-restriction isomorphism, the inverse followed by the pullback projection fst recovers the restriction map to the open set U.

Русский

В изоморфизме pullbackRestrictIsoRestrict, обратная связь и проекция fst восстанавливают ограничение к U.

LaTeX

$$(pullbackRestrictIsoRestrict f U).inv ≫ pullback.fst f U.ι = (f ⁻¹ᵁ U).ι$$

Lean4

@[simp, reassoc]
theorem pullbackRestrictIsoRestrict_inv_fst {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) :
    (pullbackRestrictIsoRestrict f U).inv ≫ pullback.fst f _ = (f ⁻¹ᵁ U).ι := by delta pullbackRestrictIsoRestrict; simp

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