ι_jointly_surjective — Mathlib

English

The principal equality of opensImagePreimageMap_app holds: the two composed paths agree via a witness from opensImagePreimageMap_app'.

Русский

Главное равенство opensImagePreimageMap_app: две составные траектории совпадают по свидетельству из opensImagePreimageMap_app'.

LaTeX

$$$D.opensImagePreimageMap i j U ≫ (D.f j k).c.app _ = ((π_1 j,i,k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫ (π_2⁻¹ j,i,k) (unop _) ≫ (D.V (j,k)).presheaf.map (eqToHom (opensImagePreimageMap_app' D i j k U).choose)$$$

Lean4

theorem ι_jointly_surjective (x : 𝖣.glued) : ∃ (i : D.J) (y : D.U i), (𝖣.ι i).base y = x :=
  𝖣.ι_jointly_surjective
    ((LocallyRingedSpace.forgetToSheafedSpace.{u} ⋙ SheafedSpace.forget CommRingCat.{u}) ⋙ forget TopCat.{u}) x

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