instEffectiveEpiFamilyObjMapOfIsEquivalence

English

If e: C ≌ D is an equivalence, then EffectiveEpiFamily is preserved under F.obj and F.map along e for any F equivalence.

Русский

Если e: C ≌ D — эквивалентность, то семейство эпиморфий сохраняется через отображение F_obj и отображение F_map через эквивалентность.

LaTeX

$$$e : C \simeq D \Rightarrow (\text{If } X,\pi \text{ is effective epi family in C, then } F.obj(X) , F.map(\pi) \text{ is in D})$$$

Lean4

instance (F : C ⥤ D) [F.IsEquivalence] : EffectiveEpiFamily (fun a ↦ F.obj (X a)) (fun a ↦ F.map (π a)) :=
  ⟨⟨effectiveEpiFamilyStructOfEquivalence F.asEquivalence _ _⟩⟩

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