English
The induced construction yields a category equivalent to the target category.
Русский
Индукционная конструкция даёт категорию, эквивалентную целевой категории.
LaTeX
$$$\\operatorname{InducedCategory} D e \\simeq D$$$
Lean4
/-- If `T ≃ D` is a bijection and `D` is a category, then
`InducedCategory D e` is equivalent to `D`. -/
@[simps]
def induced {T : Type*} (e : T ≃ D) : InducedCategory D e ≌ D
where
functor := inducedFunctor e
inverse :=
{ obj := e.symm
map {X Y}
f :=
show e (e.symm X) ⟶ e (e.symm Y) from eqToHom (e.apply_symm_apply X) ≫ f ≫ eqToHom (e.apply_symm_apply Y).symm
map_comp {X Y Z} f
g := by
dsimp
rw [Category.assoc]
erw [Category.assoc]
rw [Category.assoc, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp] }
unitIso :=
NatIso.ofComponents (fun _ ↦ eqToIso (by simp))
(fun {X Y} f ↦ by
dsimp
erw [eqToHom_trans_assoc _ (by simp), eqToHom_refl, Category.id_comp]
rfl)
counitIso := NatIso.ofComponents (fun _ ↦ eqToIso (by simp))
functor_unitIso_comp X := eqToHom_trans (by simp) (by simp)
