Theorems · Definition · category theory

CategoryTheory.Functor.FullyFaithful.leftOp

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C Dᵒᵖ} → F.FullyFaithful → F.leftOp.FullyFaithful

The opposite of a fully faithful functor is fully faithful.

Defined in: Mathlib.CategoryTheory.Opposites
Cited by: 0 results in Mathlib
Foundations: Depth 14 from the axioms · uses propext
Assumes: CategoryTheory.Category CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homproof · cited by 32,603
CategoryTheory.Functor.objproof · cited by 19,642
CategoryTheory.Functorstatement and proof · cited by 16,252
Oppositestatement and proof · cited by 8,081
Quiver.Hom.opproof · cited by 1,948
CategoryTheory.Functor.leftOpstatement and proof · cited by 187
CategoryTheory.Functor.FullyFaithfulstatement and proof · cited by 87
CategoryTheory.Functor.FullyFaithful.preimageproof · cited by 64

Cited by2

Results whose statement or proof uses this declaration.

AlgebraicGeometry.hopfSpec.fullyFaithfulproof · cited by 0
AlgebraicGeometry.bialgSpec.fullyFaithfulproof · cited by 0