of_equivalence — Mathlib

English

A simp lemma about how the separating property behaves with equivalences and composition of maps.

Русский

Лемма упрощения о поведении разделяющего свойства при эквивалентностях и композициях морфизмов.

LaTeX

$$$(IsSeparating\text{ with Equivalence})$$$

Lean4

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

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