effectiveEpi_desc_iff_effectiveEpiFamily

English

For finite α, EffectiveEpi (Sigma.desc π) is equivalent to EffectiveEpiFamily X π.

Русский

Для конечного α эффективная эпиморфия Sigma.desc π эквивалентна EffectiveEpiFamily X π.

LaTeX

$$$[\text{Finite }\alpha] \Rightarrow \operatorname{EffectiveEpi}(\Sigma.\mathrm{desc}\,\pi) \iff \operatorname{EffectiveEpiFamily} X\pi$$$

Lean4

theorem effectiveEpi_desc_iff_effectiveEpiFamily {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) :
    EffectiveEpi (Sigma.desc π) ↔ EffectiveEpiFamily X π := by
  exact
    ⟨fun h ↦
      ⟨⟨@effectiveEpiFamilyStructOfEffectiveEpiDesc _ _ _ _ X π _ h _ _
            (fun g ↦ (FinitaryPreExtensive.isIso_sigmaDesc_fst (fun a ↦ Sigma.ι X a) g inferInstance).epi_of_iso)⟩⟩,
      fun _ ↦ inferInstance⟩

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