Lean4
/-- An effective epi family precomposed by a family of split epis is effective epimorphic.
This version takes an explicit section to the split epis, and is mainly used to define
`effectiveEpiStructCompOfEffectiveEpiSplitEpi`,
which takes a `IsSplitEpi` instance instead.
-/
noncomputable def effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi' {α : Type*} {B : C} {X Y : α → C}
(f : (a : α) → X a ⟶ B) (g : (a : α) → Y a ⟶ X a) (i : (a : α) → X a ⟶ Y a) (hi : ∀ a, i a ≫ g a = 𝟙 _)
[EffectiveEpiFamily _ f] : EffectiveEpiFamilyStruct _ (fun a ↦ g a ≫ f a)
where
desc e
w :=
EffectiveEpiFamily.desc _ f (fun a ↦ i a ≫ e a) fun a₁ a₂ g₁ g₂ _ ↦
(by
simp only [← Category.assoc]
apply w _ _ (g₁ ≫ i a₁) (g₂ ≫ i a₂)
simp only [Category.assoc]
simp only [← Category.assoc, hi]
simpa)
fac e w
a := by
simp only [Category.assoc, EffectiveEpiFamily.fac]
rw [← Category.id_comp (e a), ← Category.assoc, ← Category.assoc]
apply w
simp only [Category.comp_id, Category.id_comp, ← Category.assoc]
aesop
uniq _ _ _
hm := by
apply EffectiveEpiFamily.uniq _ f
intro a
rw [← hm a, ← Category.assoc, ← Category.assoc, hi, Category.id_comp]
