overEquiv_symm_generate — Mathlib

English

The inverse of overEquiv sends generates of a presieve to a generated presieve under pullback.

Русский

Обратная overEquiv отправляет порожденные презепивы в порожденные презепивы при pullback.

LaTeX

$$(overEquiv Y).symm (.generate R) = .generate (Presieve.functorPullback (Over.forget X) R)$$

Lean4

theorem overEquiv_symm_generate {X : C} {Y : Over X} (R : Presieve Y.left) :
    (overEquiv Y).symm (.generate R) = .generate (Presieve.functorPullback (Over.forget X) R) :=
  by
  refine le_antisymm (fun Z g hg ↦ ?_) ?_
  · rw [overEquiv_symm_iff] at hg
    obtain ⟨W, p, q, hq, hpq⟩ := hg
    refine ⟨.mk (q ≫ Y.hom), Over.homMk p (by simp [reassoc_of% hpq]), Over.homMk q rfl, hq, ?_⟩
    ext
    exact hpq
  · rw [generate_le_iff]
    exact fun Z g hg ↦ le_generate _ _ hg

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