πTruncGE_naturality — Mathlib

English

For all maps φ: K → L, the naturality square for πTruncGE commutes with the truncGE maps, i.e., K.πTruncGE e ; truncGEMap φ e = φ ; L.πTruncGE e.

Русский

Для любых отображений φ: K → L диаграмма естественности для πTruncGE через truncGEMap φ e коммутирует: K.πTruncGE e ; truncGEMap φ e = φ ; L.πTruncGE e.

LaTeX

$$$K.\pi_{\mathrm{TruncGE}}(e) \;\circ\; \mathrm{truncGEMap}(\phi,e) = \phi \circ L.\pi_{\mathrm{TruncGE}}(e)$$$

Lean4

@[reassoc (attr := simp)]
theorem πTruncGE_naturality : K.πTruncGE e ≫ truncGEMap φ e = φ ≫ L.πTruncGE e :=
  by
  apply (e.homEquiv _ _).injective
  ext1
  dsimp [truncGEMap, πTruncGE]
  rw [e.homRestrict_comp_extendMap, e.homRestrict_liftExtend, e.homRestrict_precomp, e.homRestrict_liftExtend,
    restrictionToTruncGE'_naturality]

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