whiskerEquiv — Mathlib

English

Two products which differ by an index equivalence and up to isomorphism in the factors are isomorphic.

Русский

Две произведения, индексы которых связаны эквивалентностью и которые различаются на изоморфизмах факторов, изоморфны.

LaTeX

$$$\\prod^{\\scaleto{\\text{(f)}}{4pt}} f \\cong \\prod^{\\scaleto{\\text{(g)}}{4pt}} g$ given $e : J \\simeq K$ and $w : \\forall j, g(e j) \\cong f j$.$$

Lean4

/-- Two products which differ by an equivalence in the indexing type,
and up to isomorphism in the factors, are isomorphic.
-/
@[simps]
def whiskerEquiv {J K : Type*} {f : J → C} {g : K → C} (e : J ≃ K) (w : ∀ j, g (e j) ≅ f j) [HasProduct f]
    [HasProduct g] : ∏ᶜ f ≅ ∏ᶜ g
    where
  hom := Pi.map' e.symm fun k => (w (e.symm k)).inv ≫ eqToHom (by simp)
  inv := Pi.map' e fun j => (w j).hom

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