English
For a finite index set α, a family X: α → Profinite and maps π a: X(a) → B yields an equivalence with EffectiveEpiFamily X π when surjectivity on fibers holds.
Русский
Для конечной индексации α семейство X и отображения π образуют эквивалентность с EffectiveEpiFamily, если каждая волокна подпадает под сигнатуру surjectivity.
LaTeX
$$$\\mathrm{effectiveEpiFamily\\_tfae}\\;\\alpha\\;X\\;\\pi$$$
Lean4
theorem effectiveEpiFamily_tfae {α : Type} [Finite α] {B : Profinite.{u}} (X : α → Profinite.{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 ↦ profiniteToCompHaus.obj (X a))
(fun a ↦ profiniteToCompHaus.map (π a))).out
2 0 :)]
exact ⟨fun h ↦ profiniteToCompHaus.finite_effectiveEpiFamily_of_map _ _ h, fun _ ↦ inferInstance⟩
tfae_finish
