English
Reindexing an effective epi family along an equivalence preserves effectiveness: from P for (X∘e, π∘e) deduce an effective epi family for (X, π).
Русский
Перепозиционирование эффективного эпипеременного семейства по эквиварианту сохраняет свойство: если есть эффективное семейство для (X∘e, π∘e), то оно даёт эффективное семейство для (X,π).
LaTeX
$$$\operatorname{EffectiveEpiFamily}(X\circ e)(\pi\circ e) \Rightarrow \operatorname{EffectiveEpiFamily} X\pi$$$
Lean4
/-- Reindex the indexing type of an effective epi family struct.
-/
def reindex {B : C} {α α' : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) (e : α' ≃ α)
(P : EffectiveEpiFamilyStruct (fun a => X (e a)) (fun a => π (e a))) : EffectiveEpiFamilyStruct X π
where
desc := fun f h => P.desc (fun _ => f _) (fun _ _ => h _ _)
fac _ _
a := by
obtain ⟨a, rfl⟩ := e.surjective a
apply P.fac
uniq _ _ _ hm := P.uniq _ _ _ fun _ => hm _
