t_id — Mathlib

English

On a fixed index i in the open cover, the corresponding t-map equals the identity on the pullback fiber up to compatible identifications in the category of schemes.

Русский

На фиксированном индексе i в открытом покрытии соответствующая карта t равна единице на волокне pullback, с учётом совместимых идентификаций в схеме.

LaTeX

$$$t 𝒰 f g i i = 1$ (up to equality in the scheme-structure)$$

Lean4

theorem t_id (i : 𝒰.I₀) : t 𝒰 f g i i = 𝟙 _ :=
  by
  apply pullback.hom_ext <;> rw [Category.id_comp]
  · apply pullback.hom_ext
    · rw [← cancel_mono (𝒰.f i)]; simp only [pullback.condition, Category.assoc, t_fst_fst]
    · simp only [Category.assoc, t_fst_snd]
  · rw [← cancel_mono (𝒰.f i)]; simp only [pullback.condition, t_snd, Category.assoc]

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