diagonalCover_map — Mathlib

English

Restriction of the diagonal map to a certain open subcover is isomorphic to a restricted diagonal map on the restricted pullback.

Русский

Ограничение диагонального отображения на открытое подпокрытие изоморфно ограниченному диагональному отображению на ограниченном пулбэке.

LaTeX

$$$$ \text{diagonalRestrictIsoDiagonal}(i,j) : \text{Arrow.mk}(...) \cong \text{Arrow.mk}(...) $$$$

Lean4

theorem diagonalCover_map (I) :
    (diagonalCover f 𝒰 𝒱).f I =
      pullback.map _ _ _ _ ((𝒱 I.fst).f _ ≫ pullback.fst _ _) ((𝒱 I.fst).f _ ≫ pullback.fst _ _) (𝒰.f _) (by simp)
        (by simp) :=
  by
  cases I
  ext1 <;> simp [diagonalCover, Cover.pullbackHom]

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