congr_apply — Mathlib

English

Pull back a Meq witness along a morphism f: Y → X to a refined cover given by the pullback square.

Русский

Вытягиваем свидетеля Meq вдоль морфизма f: Y → X к уточнённому покрытию через диаграмму вытяжки.

LaTeX

$$$\text{pullback}(x,f): \mathrm{Meq}(P, (J.pullback f).obj S)$$$

Lean4

theorem congr_apply {X} {P : Cᵒᵖ ⥤ D} {S : J.Cover X} (x : Meq P S) {Y} {f g : Y ⟶ X} (h : f = g) (hf : S f) :
    x ⟨_, _, hf⟩ = x ⟨_, g, by simpa only [← h] using hf⟩ :=
  by
  subst h
  rfl

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