mapBifunctorMapMapIso — Mathlib

English

There is a canonical isomorphism between mapBifunctorMapObj with X1,Y1 and X2,Y2 induced by isomorphisms X1 ≅ X2 and Y1 ≅ Y2.

Русский

Существует канонический изоморфизм между mapBifunctorMapObj F p X1 Y1 и mapBifunctorMapObj F p X2 Y2, индуцированный изоморфизмами X1 ≅ X2 и Y1 ≅ Y2.

LaTeX

$$$mapBifunctorMapObj F p X_1 Y_1 \cong mapBifunctorMapObj F p X_2 Y_2$$$

Lean4

/-- The isomorphism `mapBifunctorMapObj F p X₁ Y₁ ≅ mapBifunctorMapObj F p X₂ Y₂`
induced by isomorphisms `X₁ ≅ X₂` and `Y₁ ≅ Y₂`. -/
@[simps]
noncomputable def mapBifunctorMapMapIso (e : X₁ ≅ X₂) (e' : Y₁ ≅ Y₂) :
    mapBifunctorMapObj F p X₁ Y₁ ≅ mapBifunctorMapObj F p X₂ Y₂
    where
  hom := mapBifunctorMapMap F p e.hom e'.hom
  inv := mapBifunctorMapMap F p e.inv e'.inv
  hom_inv_id := by ext; simp
  inv_hom_id := by ext; simp

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