over_forget_compatiblePreserving — Mathlib

English

The forgetful functor Over forget X is compatible-preserving with respect to the Grothendieck topology J and the over-topology J.over X, meaning compatible families of coverings are preserved under forgetful transport.

Русский

Забывающая функция Over forget X совместима с топологией Гротендийка и сверху—сверху Over, то есть сохраняет совместимые покрытия при переносе.

LaTeX

$$$\\forall X\\,\\mathrm{CompatiblePreserving}\\ J\\ (\\mathrm{Over.forget}\\ X)$$$

Lean4

theorem over_forget_compatiblePreserving (X : C) : CompatiblePreserving J (Over.forget X) where
  compatible
    {_ Z _ _ hx Y₁ Y₂ W f₁ f₂ g₁ g₂ hg₁ hg₂
      h} := by
    let W' : Over X := Over.mk (f₁ ≫ Y₁.hom)
    let g₁' : W' ⟶ Y₁ := Over.homMk f₁
    let g₂' : W' ⟶ Y₂ := Over.homMk f₂ (by simpa using h.symm =≫ Z.hom)
    exact hx g₁' g₂' hg₁ hg₂ (by ext; exact h)

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