English
Under suitable open cover restrictions, the diagonal map yields a pullback in the restricted setting.
Русский
При надлежащих ограничениях диагональная карта задаёт пулбэк в ограниченной конфигурации.
LaTeX
$$$$ \text{HasPullback}( \text{diagonal}, \text{restrictions}) $$$$
Lean4
/-- The restriction of the diagonal `X ⟶ X ×ₛ X` to `𝒱 i j ×[𝒰 i] 𝒱 i j` is the diagonal
`𝒱 i j ⟶ 𝒱 i j ×[𝒰 i] 𝒱 i j`. -/
noncomputable def diagonalRestrictIsoDiagonal (i j) :
Arrow.mk (pullback.diagonal f ∣_ ((diagonalCover f 𝒰 𝒱).f ⟨i, j, j⟩).opensRange) ≅
Arrow.mk (pullback.diagonal ((𝒱 i).f j ≫ pullback.snd _ _)) :=
by
refine (morphismRestrictOpensRange _ _).trans ?_
refine Arrow.isoMk ?_ (Iso.refl _) ?_
·
exact
pullback.congrHom rfl (diagonalCover_map _ _ _ _) ≪≫
pullbackDiagonalMapIso _ _ _ _ ≪≫ (asIso (pullback.diagonal _)).symm
have H :
pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫ pullback.snd _ _ =
pullback.snd _ _ ≫ pullback.fst _ _ :=
by
rw [← cancel_mono ((𝒱 i).f _)]
apply pullback.hom_ext
· trans
pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
(diagonalCover f 𝒰 𝒱).f _ ≫ pullback.snd _ _
· simp [diagonalCover_map]
symm
trans
pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
(diagonalCover f 𝒰 𝒱).f _ ≫ pullback.fst _ _
· simp [diagonalCover_map]
· rw [← pullback.condition_assoc, ← pullback.condition_assoc]
simp
· simp [pullback.condition, Cover.pullbackHom]
dsimp [Cover.pullbackHom] at H ⊢
apply pullback.hom_ext
· simp only [Category.assoc, pullback.diagonal_fst, Category.comp_id]
simp only [← Category.assoc, IsIso.comp_inv_eq]
apply pullback.hom_ext <;> simp [H]
· simp only [Category.assoc, pullback.diagonal_snd, Category.comp_id]
simp only [← Category.assoc, IsIso.comp_inv_eq]
apply pullback.hom_ext <;> simp [H]
