π — Mathlib · SciLib

English

There is a canonical equivalence between lift-structures of α and lift-structures of its image under the arrowHomEquiv relative to the parametrized adjunction.

Русский

Существует каноническое эквивалентное соответствие между структурами подъёма для α и структурами подъёма его образа через arrowHomEquiv в контексте параметризованного сопряжения.

LaTeX

$$$\\text{liftStructEquiv}(\\alpha) : \\mathrm{Arrow.LiftStruct}(\\alpha) \\simeq \\mathrm{Arrow.LiftStruct}(\\text{adj₂.arrowHomEquiv}(\\alpha))$$$

Lean4

/-- The projection `(G.obj (op Y₁)).obj X₃ ⟶ sq.pt` when
`sq : G.PullbackObjObj f₁ f₃`. -/
noncomputable def π : (G.obj (op Y₁)).obj X₃ ⟶ sq.pt :=
  sq.isPullback.lift ((G.map f₁.op).app X₃) ((G.obj (op Y₁)).map f₃) (by simp)

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