Theorems · Definition · category theory

CategoryTheory.Equivalence.congrFullSubcategory

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {P : CategoryTheory.ObjectProperty C} →
          {Q : CategoryTheory.ObjectProperty D} →
            (e : C ≌ D) →
              [Q.IsClosedUnderIsomorphisms] → Q.inverseImage e.functor = P → (P.FullSubcategory ≌ Q.FullSubcategory)

The equivalence of categories between two fullsubcategories P and Q of categories C and D that is induced by an equivalence e : C ≌ D when Q.inverseImage e.functor = P and Q respects isomorphisms.

Defined in

Mathlib.CategoryTheory.ObjectProperty.Equivalence

Cited by

4 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms