English
For finite α and Stonean X, the following are equivalent: EffectiveEpiFamily X π, Epi (Sigma.desc π), and a surjectivity condition for all b ∈ B.
Русский
Для конечного множества α и Stonean X эквивалентны: EffectiveEpiFamily X π, Epi (Sigma.desc π) и условие сюръективности для каждого b в B.
LaTeX
$$$\text{TFAE}[\text{EffectiveEpiFamily }X\,π, \text{Epi }(\Sigma.desc\ π), \forall b:\,B, \exists a,x:\, π a x = b]$$$
Lean4
theorem effectiveEpiFamily_tfae {α : Type} [Finite α] {B : Stonean.{u}} (X : α → Stonean.{u})
(π : (a : α) → (X a ⟶ B)) :
TFAE [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ b : B, ∃ (a : α) (x : X a), π a x = b] :=
by
tfae_have 2 → 1
| _ => by simpa [← effectiveEpi_desc_iff_effectiveEpiFamily, (effectiveEpi_tfae (Sigma.desc π)).out 0 1]
tfae_have 1 → 2 := fun _ ↦ inferInstance
tfae_have 3 ↔ 1 :=
by
erw [((CompHaus.effectiveEpiFamily_tfae (fun a ↦ Stonean.toCompHaus.obj (X a))
(fun a ↦ Stonean.toCompHaus.map (π a))).out
2 0 :)]
exact ⟨fun h ↦ Stonean.toCompHaus.finite_effectiveEpiFamily_of_map _ _ h, fun _ ↦ inferInstance⟩
tfae_finish
