precoherentEffectiveEpiFamilyCompEffectiveEpis

English

If Y π is an EffectiveEpiFamily and you have arrows f a: Z a → Y a that are each epi, then Z π_n composed with π gives an EffectiveEpiFamily.

Русский

Если Y π образует EffectiveEpiFamily и существуют стрелки f_a: Z_a → Y_a каждая из которых эпиморфна, то композиция π_n с π образует EffectiveEpiFamily.

LaTeX

$$$\text{EffectiveEpiFamily } Z \pi_n \Rightarrow \text{EffectiveEpiFamily} (Z) (π_n) \circ π$$$

Lean4

instance precoherentEffectiveEpiFamilyCompEffectiveEpis {α : Type} [Finite α] {Y Z : α → C} (π : (a : α) → (Y a ⟶ X))
    [EffectiveEpiFamily Y π] (f : (a : α) → Z a ⟶ Y a) [h : ∀ a, EffectiveEpi (f a)] :
    EffectiveEpiFamily _ fun a ↦ f a ≫ π a :=
  by
  simp_rw [effectiveEpi_iff_effectiveEpiFamily] at h
  exact
    EffectiveEpiFamily.reindex (e := Equiv.sigmaPUnit α) _ _
      (EffectiveEpiFamily.transitive_of_finite (β := fun _ ↦ Unit) _ inferInstance _ h)

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