of_equivalence — Mathlib

English

For any 𝒢, IsSeparating 𝒢.op is equivalent to IsCoseparating 𝒢.

Русский

Для любых 𝒢 верно, что IsSeparating 𝒢.op эквивалентно IsCoseparating 𝒢.

LaTeX

$$$IsSeparating(𝒢.op) \iff IsCoseparating(𝒢)$$$

Lean4

theorem of_equivalence {𝒢 : Set C} (h : IsCoseparating 𝒢) {D : Type*} [Category D] (α : C ≌ D) :
    IsCoseparating (α.functor.obj '' 𝒢) := fun X Y f g H =>
  α.inverse.map_injective
    (h _ _
      (fun Z hZ h => by
        obtain ⟨h', rfl⟩ := (α.symm.toAdjunction.homEquiv _ _).symm.surjective h
        simp only [Adjunction.homEquiv_symm_apply, ← Category.assoc, ← Functor.map_comp, Equivalence.symm_functor,
          H (α.functor.obj Z) (Set.mem_image_of_mem _ hZ) h']))

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