Lean4
/-- Equivalences preserve effective epimorphic families -/
def effectiveEpiFamilyStructOfEquivalence :
EffectiveEpiFamilyStruct (fun a ↦ e.functor.obj (X a)) (fun a ↦ e.functor.map (π a))
where
desc ε
h :=
(e.toAdjunction.homEquiv _ _).symm
(EffectiveEpiFamily.desc X π (fun a ↦ e.unit.app _ ≫ e.inverse.map (ε a))
(effectiveEpiFamilyStructOfEquivalence_aux e X π ε h))
fac ε h
a := by
simp only [Functor.comp_obj, Adjunction.homEquiv_counit, Equivalence.toAdjunction_counit]
have :=
congrArg ((fun f ↦ f ≫ e.counit.app _) ∘ e.functor.map)
(EffectiveEpiFamily.fac X π (fun a ↦ e.unit.app _ ≫ e.inverse.map (ε a))
(effectiveEpiFamilyStructOfEquivalence_aux e X π ε h) a)
simp only [Functor.id_obj, Functor.comp_obj, Function.comp_apply, Functor.map_comp, Category.assoc,
Equivalence.fun_inv_map, Iso.inv_hom_id_app, Category.comp_id] at this
simp [this]
uniq ε h m
hm := by
simp only [Functor.comp_obj, Adjunction.homEquiv_counit, Equivalence.toAdjunction_counit]
have :=
EffectiveEpiFamily.uniq X π (fun a ↦ e.unit.app _ ≫ e.inverse.map (ε a))
(effectiveEpiFamilyStructOfEquivalence_aux e X π ε h)
specialize this (e.unit.app _ ≫ e.inverse.map m) fun a ↦ ?_
· rw [← congrArg e.inverse.map (hm a)]
simp
· simp [← this]
