English
The comapEquiv construction provides a canonical equivalence between graded objects indexed by β and those indexed by γ, whenever there is an equivalence e between β and γ. It uses comap with e.symm and e to transport grading along the equivalence.
Русский
Конструкция comapEquiv устанавливает каноническое эквивалентное соответствие между градуированными объектами по индексу β и по индексу γ при наличии эквивалента e между β и γ. Она переносит градацию по эквивалентности через comap с e.symm и e.
LaTeX
$$$\text{comapEquiv}\, C\, e : GradedObject β C \\cong GradedObject γ C$$$
Lean4
/-- The equivalence between β-graded objects and γ-graded objects,
given an equivalence between β and γ.
-/
@[simps]
def comapEquiv {β γ : Type w} (e : β ≃ γ) : GradedObject β C ≌ GradedObject γ C
where
functor := comap C (e.symm : γ → β)
inverse := comap C (e : β → γ)
counitIso := (Pi.comapComp (fun _ => C) _ _).trans (comapEq C (by ext; simp))
unitIso := (comapEq C (by ext; simp)).trans (Pi.comapComp _ _ _).symm
