English
For a finite index family X and π, the three statements—EffectiveEpiFamily, Epi(desc π), and pointwise surjectivity—are equivalent.
Русский
Для конечного семейства X и отображения π три утверждения—EffectiveEpiFamily, Epi(desc π), и точечная сюръективность—эквивалентны.
LaTeX
$$$\mathrm{TFAE}\;[\mathrm{EffectiveEpiFamily}~X~\pi, \mathrm{Epi}(\Sigma\text{.desc }\pi), \forall b:\,B, \exists a, x.\;\pi_a(x)=b]$$$
Lean4
theorem effectiveEpiFamily_tfae {α : Type} [Finite α] {B : CompHaus.{u}} (X : α → CompHaus.{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
| _ => inferInstance
tfae_have 3 → 2
| e => by
rw [epi_iff_surjective]
intro b
obtain ⟨t, x, h⟩ := e b
refine ⟨Sigma.ι X t x, ?_⟩
change (Sigma.ι X t ≫ Sigma.desc π) x = _
simpa using h
tfae_have 2 → 3
| e => by
rw [epi_iff_surjective] at e
let i : ∐ X ≅ finiteCoproduct X := (colimit.isColimit _).coconePointUniqueUpToIso (finiteCoproduct.isColimit _)
intro b
obtain ⟨t, rfl⟩ := e b
let q := i.hom t
refine ⟨q.1, q.2, ?_⟩
have : t = i.inv (i.hom t) := show t = (i.hom ≫ i.inv) t by simp only [i.hom_inv_id]; rfl
rw [this]
change _ = (i.inv ≫ Sigma.desc π) (i.hom t)
suffices i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π by rw [this]; rfl
rw [Iso.inv_comp_eq]
apply colimit.hom_ext
rintro ⟨a⟩
simp only [i, Discrete.functor_obj, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app,
colimit.comp_coconePointUniqueUpToIso_hom_assoc]
ext; rfl
tfae_finish
