Effective epimorphic families in CompHaus
#
Let π a : X a ⟶ B
be a family of morphisms in CompHaus
indexed by a finite type α
.
In this file, we show that the following are all equivalent:
- The family
π
is effective epimorphic. - The induced map
∐ X ⟶ B
is epimorphic. - The family
π
is jointly surjective. This is the main result of this file, which can be found inCompHaus.effectiveEpiFamily_tfae
As a consequence, we also show that CompHaus
is precoherent.
Projects #
def
CompHaus.EffectiveEpiFamily.relation
{α : Type}
[Fintype α]
{B : CompHaus}
{X : α → CompHaus}
(π : (a : α) → X a ⟶ B)
:
Setoid ↑(CompHaus.finiteCoproduct X).toTop
Implementation: This is a setoid on the explicit finite coproduct of X
whose quotient
will be isomorphic to B
provided that X a → B
is an effective epi family.
Instances For
def
CompHaus.EffectiveEpiFamily.ιFun
{α : Type}
[Fintype α]
{B : CompHaus}
{X : α → CompHaus}
(π : (a : α) → X a ⟶ B)
:
Quotient (CompHaus.EffectiveEpiFamily.relation π) → ↑B.toTop
Implementation: the map from the quotient of relation π
to B
, which will eventually
become the function underlying an isomorphism, provided that X a → B
is an effective epi family.
Instances For
theorem
CompHaus.EffectiveEpiFamily.π'_comp_ι_hom_assoc
{α : Type}
[Fintype α]
{B : CompHaus}
{X : α → CompHaus}
(π : (a : α) → X a ⟶ B)
(surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b)
(a : α)
{Z : CompHaus}
(h : B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CompHaus.EffectiveEpiFamily.π' π a)
(CategoryTheory.CategoryStruct.comp (CompHaus.EffectiveEpiFamily.ι (fun a => π a) surj).hom h) = CategoryTheory.CategoryStruct.comp (π a) h
theorem
CompHaus.EffectiveEpiFamily.π'_comp_ι_hom
{α : Type}
[Fintype α]
{B : CompHaus}
{X : α → CompHaus}
(π : (a : α) → X a ⟶ B)
(surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b)
(a : α)
:
CategoryTheory.CategoryStruct.comp (CompHaus.EffectiveEpiFamily.π' π a)
(CompHaus.EffectiveEpiFamily.ι (fun a => π a) surj).hom = π a
theorem
CompHaus.EffectiveEpiFamily.π_comp_ι_inv_assoc
{α : Type}
[Fintype α]
{B : CompHaus}
{X : α → CompHaus}
(π : (a : α) → X a ⟶ B)
(surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b)
(a : α)
{Z : CompHaus}
(h : (CompHaus.EffectiveEpiFamily.QB fun a => π a) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (π a)
(CategoryTheory.CategoryStruct.comp (CompHaus.EffectiveEpiFamily.ι (fun a => π a) surj).inv h) = CategoryTheory.CategoryStruct.comp (CompHaus.EffectiveEpiFamily.π' π a) h
theorem
CompHaus.EffectiveEpiFamily.π_comp_ι_inv
{α : Type}
[Fintype α]
{B : CompHaus}
{X : α → CompHaus}
(π : (a : α) → X a ⟶ B)
(surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b)
(a : α)
:
CategoryTheory.CategoryStruct.comp (π a) (CompHaus.EffectiveEpiFamily.ι (fun a => π a) surj).inv = CompHaus.EffectiveEpiFamily.π' π a
noncomputable def
CompHaus.EffectiveEpiFamily.struct
{α : Type}
[Fintype α]
{B : CompHaus}
{X : α → CompHaus}
(π : (a : α) → X a ⟶ B)
(surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b)
:
Implementation: The family X
is an effective epi, provided that π
are jointly surjective.
The theorem CompHaus.effectiveEpiFamily_tfae
should be used instead.
Instances For
theorem
CompHaus.effectiveEpiFamily_tfae
{α : Type}
[Fintype α]
{B : CompHaus}
(X : α → CompHaus)
(π : (a : α) → X a ⟶ B)
:
List.TFAE
[CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π),
∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b]