arrowHomEquiv — Mathlib

English

The π projection is defined as the isPullback-lift with the indicated maps; it is the canonical arrow from the Y-side pullback object to the pushout object.

Русский

Проекция π определяется как инстанция Lift от IsPullback c указанными маппингами; это каноническое отображение из вытягиваемого объекта наPushout-объект.

LaTeX

$$$\\pi = sq.isPullback.lift ( (G.map f_1.op).app X_3 ) ( (G.obj (op Y_1)).map f_3 ) (by simp)$$$

Lean4

/-- Given a parametrized adjunction `F ⊣₂ G` between bifunctors, and structures
`sq₁₂ : F.PushoutObjObj f₁ f₂` and `sq₁₃ : G.PullbackObjObj f₁ f₃`, there are
as many commutative squares with left map `sq₁₂.ι` and right map `f₃`
as commutative squares with left map `f₂` and right map `sq₁₃.π`. -/
@[simps! apply_left symm_apply_right]
noncomputable def arrowHomEquiv : (Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) ≃ (Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π)
    where
  toFun
    α :=
    Arrow.homMk (adj₂.homEquiv (sq₁₂.inl ≫ α.left))
      (sq₁₃.isPullback.lift (adj₂.homEquiv (sq₁₂.inr ≫ α.left)) (adj₂.homEquiv α.right)
        (by simp [← adj₂.homEquiv_naturality_one, ← adj₂.homEquiv_naturality_three]))
      (by
        apply sq₁₃.isPullback.hom_ext
        · simp [← adj₂.homEquiv_naturality_two, ← adj₂.homEquiv_naturality_one, sq₁₂.isPushout.w_assoc]
        · simp [← adj₂.homEquiv_naturality_two, ← adj₂.homEquiv_naturality_three])
  invFun
    β :=
    Arrow.homMk
      (sq₁₂.isPushout.desc (adj₂.homEquiv.symm β.left) (adj₂.homEquiv.symm (β.right ≫ sq₁₃.fst))
        (by
          have := Arrow.w β =≫ sq₁₃.fst
          dsimp at this
          simp only [Category.assoc, sq₁₃.π_fst] at this
          simp only [← adj₂.homEquiv_symm_naturality_one, ← adj₂.homEquiv_symm_naturality_two, Arrow.mk_left,
            Arrow.mk_right, this]))
      (adj₂.homEquiv.symm (β.right ≫ sq₁₃.snd))
      (by
        apply sq₁₂.isPushout.hom_ext
        · have := Arrow.w β =≫ sq₁₃.snd
          dsimp at this
          simp only [Category.assoc, sq₁₃.π_snd] at this
          simp [← adj₂.homEquiv_symm_naturality_two, ← adj₂.homEquiv_symm_naturality_three, this]
        · simp [← adj₂.homEquiv_symm_naturality_one, ← adj₂.homEquiv_symm_naturality_three, sq₁₃.isPullback.w])
  left_inv
    α := by
    ext
    · apply sq₁₂.isPushout.hom_ext <;> simp
    · simp
  right_inv
    β := by
    ext
    · simp
    · apply sq₁₃.isPullback.hom_ext <;> simp

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