Loogle!

Result

Found 254 declarations mentioning CategoryTheory.Functor.FullyFaithful. Of these, only the first 200 are shown.

• CategoryTheory.Functor.FullyFaithful.id 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.Functor.id C).FullyFaithful
• CategoryTheory.Functor.FullyFaithful 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Type (max (max u₁ v₁) v₂)
• CategoryTheory.Functor.FullyFaithful.instSubsingleton 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} : Subsingleton F.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.faithful 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) : F.Faithful
• CategoryTheory.Functor.FullyFaithful.full 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) : F.Full
• CategoryTheory.Functor.FullyFaithful.ofFullyFaithful 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] : F.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.ofIso 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {G : CategoryTheory.Functor C D} (e : F ≅ G) : G.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.preimageIso 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (e : F.obj X ≅ F.obj Y) : X ≅ Y
• CategoryTheory.Functor.FullyFaithful.isoEquiv 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} : (X ≅ Y) ≃ (F.obj X ≅ F.obj Y)
• CategoryTheory.Functor.FullyFaithful.comp 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {G : CategoryTheory.Functor D E} (hG : G.FullyFaithful) : (F.comp G).FullyFaithful
• CategoryTheory.Functor.FullyFaithful.ofCompFaithful 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [G.Faithful] (hFG : (F.comp G).FullyFaithful) : F.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.preimage 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (self : F.FullyFaithful) {X Y : C} (f : F.obj X ⟶ F.obj Y) : X ⟶ Y
• CategoryTheory.Functor.FullyFaithful.homEquiv 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} : (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y)
• CategoryTheory.Functor.FullyFaithful.preimage_id 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X : C} : hF.preimage (CategoryTheory.CategoryStruct.id (F.obj X)) = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Functor.FullyFaithful.preimage_map 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (self : F.FullyFaithful) {X Y : C} (f : X ⟶ Y) : self.preimage (F.map f) = f
• CategoryTheory.Functor.FullyFaithful.map_bijective 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X Y : C) : Function.Bijective F.map
• CategoryTheory.Functor.FullyFaithful.map_surjective 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} : Function.Surjective F.map
• CategoryTheory.Functor.FullyFaithful.isIso_of_isIso_map 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso (F.map f)] : CategoryTheory.IsIso f
• CategoryTheory.Functor.FullyFaithful.nonempty_iff_map_bijective 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Nonempty F.FullyFaithful ↔ ∀ (X Y : C), Function.Bijective F.map
• CategoryTheory.Functor.FullyFaithful.map_preimage 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (self : F.FullyFaithful) {X Y : C} (f : F.obj X ⟶ F.obj Y) : F.map (self.preimage f) = f
• CategoryTheory.Functor.FullyFaithful.preimageIso_hom 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (e : F.obj X ≅ F.obj Y) : (hF.preimageIso e).hom = hF.preimage e.hom
• CategoryTheory.Functor.FullyFaithful.preimageIso_inv 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (e : F.obj X ≅ F.obj Y) : (hF.preimageIso e).inv = hF.preimage e.inv
• CategoryTheory.Functor.FullyFaithful.map_injective 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} {f g : X ⟶ Y} (h : F.map f = F.map g) : f = g
• CategoryTheory.Functor.FullyFaithful.preimage_comp 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) : hF.preimage (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hF.preimage f) (hF.preimage g)
• CategoryTheory.Functor.FullyFaithful.comp_preimage 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {G : CategoryTheory.Functor D E} (hG : G.FullyFaithful) {X✝ Y✝ : C} (f : (F.comp G).obj X✝ ⟶ (F.comp G).obj Y✝) : (hF.comp hG).preimage f = hF.preimage (hG.preimage f)
• CategoryTheory.Functor.FullyFaithful.mk 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (preimage : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)) (map_preimage : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage f) = f := by cat_disch) (preimage_map : ∀ {X Y : C} (f : X ⟶ Y), preimage (F.map f) = f := by cat_disch) : F.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.preimage_comp_assoc 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (hF.preimage (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (hF.preimage f) (CategoryTheory.CategoryStruct.comp (hF.preimage g) h)
• CategoryTheory.Functor.FullyFaithful.isoEquiv_apply 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (i : X ≅ Y) : hF.isoEquiv i = F.mapIso i
• CategoryTheory.Functor.FullyFaithful.isoEquiv_symm_apply 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (e : F.obj X ≅ F.obj Y) : hF.isoEquiv.symm e = hF.preimageIso e
• CategoryTheory.Functor.FullyFaithful.homEquiv_apply 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (a✝ : X ⟶ Y) : hF.homEquiv a✝ = F.map a✝
• CategoryTheory.Functor.FullyFaithful.homEquiv_symm_apply 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (f : F.obj X ⟶ F.obj Y) : hF.homEquiv.symm f = hF.preimage f
• CategoryTheory.fullyFaithfulInducedFunctor 📋 Mathlib.CategoryTheory.InducedCategory
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : C → D) : (CategoryTheory.inducedFunctor F).FullyFaithful
• CategoryTheory.ObjectProperty.fullyFaithfulι 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.ι.FullyFaithful
• CategoryTheory.ObjectProperty.fullyFaithfulιOfLE 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') : (CategoryTheory.ObjectProperty.ιOfLE h).FullyFaithful
• CategoryTheory.Functor.FullyFaithful.whiskeringRight 📋 Mathlib.CategoryTheory.Whiskering
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} (hF : F.FullyFaithful) (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] : ((CategoryTheory.Functor.whiskeringRight C D E).obj F).FullyFaithful
• CategoryTheory.Functor.FullyFaithful.whiskeringRight_preimage_app 📋 Mathlib.CategoryTheory.Whiskering
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} (hF : F.FullyFaithful) (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {X✝ Y✝ : CategoryTheory.Functor C D} (f : ((CategoryTheory.Functor.whiskeringRight C D E).obj F).obj X✝ ⟶ ((CategoryTheory.Functor.whiskeringRight C D E).obj F).obj Y✝) (X : C) : ((hF.whiskeringRight C).preimage f).app X = hF.preimage (f.app X)
• CategoryTheory.Functor.FullyFaithful.reflectsIsomorphisms 📋 Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) : F.ReflectsIsomorphisms
• CategoryTheory.Equivalence.fullyFaithfulFunctor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ E) : e.functor.FullyFaithful
• CategoryTheory.Equivalence.fullyFaithfulInverse 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ E) : e.inverse.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.op 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) : F.op.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.leftOp 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} (hF : F.FullyFaithful) : F.leftOp.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.rightOp 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} (hF : F.FullyFaithful) : F.rightOp.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.unop 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (hF : F.FullyFaithful) : F.unop.FullyFaithful
• CategoryTheory.Groupoid.ofFullyFaithfulToGroupoid 📋 Mathlib.CategoryTheory.Groupoid
  {C : Type u_1} [𝒞 : CategoryTheory.Category.{u_2, u_1} C] {D : Type u} [CategoryTheory.Groupoid D] (F : CategoryTheory.Functor C D) (h : F.FullyFaithful) : CategoryTheory.Groupoid C
• CategoryTheory.fullyFaithfulULiftFunctor 📋 Mathlib.CategoryTheory.Types.Basic
  : CategoryTheory.uliftFunctor.{v, u}.FullyFaithful
• AddCommMonCat.fullyFaithfulForgetToAddMonCat 📋 Mathlib.Algebra.Category.MonCat.Basic
  : (CategoryTheory.forget₂ AddCommMonCat AddMonCat).FullyFaithful
• CommMonCat.fullyFaithfulForgetToMonCat 📋 Mathlib.Algebra.Category.MonCat.Basic
  : (CategoryTheory.forget₂ CommMonCat MonCat).FullyFaithful
• CategoryTheory.Functor.FullyFaithful.mulEquivEnd 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) : CategoryTheory.End X ≃* CategoryTheory.End (f.obj X)
• CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) : CategoryTheory.Aut X ≃* CategoryTheory.Aut (f.obj X)
• CategoryTheory.Functor.FullyFaithful.mulEquivEnd_apply 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (a✝ : X ⟶ X) : (hf.mulEquivEnd X) a✝ = f.map a✝
• CategoryTheory.Functor.FullyFaithful.mulEquivEnd_symm_apply 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (f✝ : f.obj X ⟶ f.obj X) : (hf.mulEquivEnd X).symm f✝ = hf.preimage f✝
• CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_hom 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (i : X ≅ X) : ((hf.autMulEquivOfFullyFaithful X) i).hom = f.map i.hom
• CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_inv 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (i : X ≅ X) : ((hf.autMulEquivOfFullyFaithful X) i).inv = f.map i.inv
• CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_hom 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (e : f.obj X ≅ f.obj X) : ((hf.autMulEquivOfFullyFaithful X).symm e).hom = hf.preimage e.hom
• CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_inv 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (e : f.obj X ≅ f.obj X) : ((hf.autMulEquivOfFullyFaithful X).symm e).inv = hf.preimage e.inv
• AddGrpCat.fullyFaihtfulForget₂ToAddMonCat 📋 Mathlib.Algebra.Category.Grp.Basic
  : (CategoryTheory.forget₂ AddGrpCat AddMonCat).FullyFaithful
• GrpCat.fullyFaithfulForget₂ToMonCat 📋 Mathlib.Algebra.Category.Grp.Basic
  : (CategoryTheory.forget₂ GrpCat MonCat).FullyFaithful
• AddCommGrpCat.fullyFaihtfulForget₂ToAddGrp 📋 Mathlib.Algebra.Category.Grp.Basic
  : (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).FullyFaithful
• CommGrpCat.fullyFaithfulForget₂ToGrp 📋 Mathlib.Algebra.Category.Grp.Basic
  : (CategoryTheory.forget₂ CommGrpCat GrpCat).FullyFaithful
• CommSemiRingCat.fullyFaithfulForget₂ToSemiRingCat 📋 Mathlib.Algebra.Category.Ring.Basic
  : (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat).FullyFaithful
• RingCat.fullyFaithfulForget₂ToSemiRingCat 📋 Mathlib.Algebra.Category.Ring.Basic
  : (CategoryTheory.forget₂ RingCat SemiRingCat).FullyFaithful
• CommRingCat.fullyFaithfulForget₂ToRingCat 📋 Mathlib.Algebra.Category.Ring.Basic
  : (CategoryTheory.forget₂ CommRingCat RingCat).FullyFaithful
• CategoryTheory.Coyoneda.fullyFaithful 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.coyoneda.FullyFaithful
• CategoryTheory.Coyoneda.ULiftCoyoneda.fullyFaithful 📋 Mathlib.CategoryTheory.Yoneda
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.FullyFaithful
• CategoryTheory.ULiftYoneda.fullyFaithful 📋 Mathlib.CategoryTheory.Yoneda
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.uliftYoneda.{w, v₁, u₁}.FullyFaithful
• CategoryTheory.Yoneda.fullyFaithful 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.yoneda.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.homNatIso' 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) : F.comp (CategoryTheory.uliftCoyoneda.{v₁, v₂, u₂}.obj (Opposite.op (F.obj X))) ≅ CategoryTheory.uliftCoyoneda.{v₂, v₁, u₁}.obj (Opposite.op X)
• CategoryTheory.Functor.FullyFaithful.homNatIso 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) : F.op.comp (CategoryTheory.uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)) ≅ CategoryTheory.uliftYoneda.{v₂, v₁, u₁}.obj X
• CategoryTheory.Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) : F.op.comp (CategoryTheory.uliftCoyoneda.{v₁, v₂, u₂}.comp ((CategoryTheory.Functor.whiskeringLeft C D (Type (max v₁ v₂))).obj F)) ≅ CategoryTheory.uliftCoyoneda.{v₂, v₁, u₁}
• CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) : F.comp (CategoryTheory.uliftYoneda.{v₁, v₂, u₂}.comp ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op)) ≅ CategoryTheory.uliftYoneda.{v₂, v₁, u₁}
• CategoryTheory.Functor.FullyFaithful.homNatIso'_hom_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X X✝ : C) : (hF.homNatIso' X).hom.app X✝ = (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom
• CategoryTheory.Functor.FullyFaithful.homNatIso'_inv_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X X✝ : C) : (hF.homNatIso' X).inv.app X✝ = (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.inv
• CategoryTheory.Functor.FullyFaithful.homNatIso_hom_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) : (hF.homNatIso X).hom.app X✝ = (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom
• CategoryTheory.Functor.FullyFaithful.homNatIso_inv_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) : (hF.homNatIso X).inv.app X✝ = (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.inv
• CategoryTheory.Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft_hom_app_app_hom_apply_down 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : Cᵒᵖ) (X✝ : C) (x : (F.comp (CategoryTheory.uliftCoyoneda.{v₁, v₂, u₂}.obj (Opposite.op (F.obj (Opposite.unop X))))).obj X✝) : ((CategoryTheory.ConcreteCategory.hom ((hF.compUliftCoyonedaCompWhiskeringLeft.hom.app X).app X✝)) x).down = hF.preimage x.down
• CategoryTheory.Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft_inv_app_app_hom_apply_down 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : Cᵒᵖ) (X✝ : C) (x : (CategoryTheory.uliftCoyoneda.{v₂, v₁, u₁}.obj (Opposite.op (Opposite.unop X))).obj X✝) : ((CategoryTheory.ConcreteCategory.hom ((hF.compUliftCoyonedaCompWhiskeringLeft.inv.app X).app X✝)) x).down = F.map x.down
• CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft_hom_app_app_hom_apply_down 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (x : (F.op.comp (CategoryTheory.uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X))).obj X✝) : ((CategoryTheory.ConcreteCategory.hom ((hF.compUliftYonedaCompWhiskeringLeft.hom.app X).app X✝)) x).down = hF.preimage x.down
• CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft_inv_app_app_hom_apply_down 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (x : (CategoryTheory.uliftYoneda.{v₂, v₁, u₁}.obj X).obj X✝) : ((CategoryTheory.ConcreteCategory.hom ((hF.compUliftYonedaCompWhiskeringLeft.inv.app X).app X✝)) x).down = F.map x.down
• CategoryTheory.Functor.FullyFaithful.over 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor T D) (h : F.FullyFaithful) : (CategoryTheory.Over.post F).FullyFaithful
• CategoryTheory.Functor.FullyFaithful.under 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor T D) (h : F.FullyFaithful) : (CategoryTheory.Under.post F).FullyFaithful
• CategoryTheory.Functor.FullyFaithful.hasZeroMorphisms 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms C] {F : CategoryTheory.Functor D C} (hF : F.FullyFaithful) : CategoryTheory.Limits.HasZeroMorphisms D
• CategoryTheory.Functor.FullyFaithful.hasZeroMorphisms_def 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms C] {F : CategoryTheory.Functor D C} (hF : F.FullyFaithful) (X Y : D) : 0 = hF.preimage 0
• CategoryTheory.Functor.FullyFaithful.preservesZeroMorphisms 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (hF : F.FullyFaithful) : F.PreservesZeroMorphisms
• CategoryTheory.LeftExactFunctor.fullyFaithful 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.LeftExactFunctor.forget C D).FullyFaithful
• CategoryTheory.RightExactFunctor.fullyFaithful 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.RightExactFunctor.forget C D).FullyFaithful
• CategoryTheory.Functor.fullyFaithfulCurry 📋 Mathlib.CategoryTheory.Functor.Currying
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] : CategoryTheory.Functor.curry.FullyFaithful
• CategoryTheory.Functor.fullyFaithfulUncurry 📋 Mathlib.CategoryTheory.Functor.Currying
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] : CategoryTheory.Functor.uncurry.FullyFaithful
• CategoryTheory.fullyFaithfulShrinkCoyoneda 📋 Mathlib.CategoryTheory.ShrinkYoneda
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] : CategoryTheory.shrinkCoyoneda.{w, v, u}.FullyFaithful
• CategoryTheory.fullyFaithfulShrinkYoneda 📋 Mathlib.CategoryTheory.ShrinkYoneda
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] : CategoryTheory.shrinkYoneda.{w, v, u}.FullyFaithful
• CategoryTheory.Adjunction.fullyFaithfulLOfIsIsoUnit 📋 Mathlib.CategoryTheory.Adjunction.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [CategoryTheory.IsIso h.unit] : L.FullyFaithful
• CategoryTheory.Adjunction.fullyFaithfulROfIsIsoCounit 📋 Mathlib.CategoryTheory.Adjunction.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [CategoryTheory.IsIso h.counit] : R.FullyFaithful
• CategoryTheory.LaxBraidedFunctor.fullyFaithfulForget 📋 Mathlib.CategoryTheory.Monoidal.Braided.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] : CategoryTheory.LaxBraidedFunctor.forget.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.addMonObj 📋 Mathlib.CategoryTheory.Monoidal.Mon
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.AddMonObj (F.obj X)] : CategoryTheory.AddMonObj X
• CategoryTheory.Functor.FullyFaithful.monObj 📋 Mathlib.CategoryTheory.Monoidal.Mon
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.MonObj (F.obj X)] : CategoryTheory.MonObj X
• CategoryTheory.Functor.FullyFaithful.mapAddMon 📋 Mathlib.CategoryTheory.Monoidal.Mon
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) : F.mapAddMon.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.mapMon 📋 Mathlib.CategoryTheory.Monoidal.Mon
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) : F.mapMon.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.isAddMonHom_preimage 📋 Mathlib.CategoryTheory.Monoidal.Mon
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) {X Y : C} [CategoryTheory.AddMonObj X] [CategoryTheory.AddMonObj Y] (f : F.obj X ⟶ F.obj Y) [CategoryTheory.IsAddMonHom f] : CategoryTheory.IsAddMonHom (hF.preimage f)
• CategoryTheory.Functor.FullyFaithful.isMonHom_preimage 📋 Mathlib.CategoryTheory.Monoidal.Mon
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) {X Y : C} [CategoryTheory.MonObj X] [CategoryTheory.MonObj Y] (f : F.obj X ⟶ F.obj Y) [CategoryTheory.IsMonHom f] : CategoryTheory.IsMonHom (hF.preimage f)
• CategoryTheory.Functor.FullyFaithful.addMonObj_zero 📋 Mathlib.CategoryTheory.Monoidal.Mon
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.AddMonObj (F.obj X)] : CategoryTheory.AddMonObj.zero = hF.preimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) CategoryTheory.AddMonObj.zero)
• CategoryTheory.Functor.FullyFaithful.monObj_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.MonObj (F.obj X)] : CategoryTheory.MonObj.one = hF.preimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) CategoryTheory.MonObj.one)
• CategoryTheory.Functor.FullyFaithful.addMonObj_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.AddMonObj (F.obj X)] : CategoryTheory.AddMonObj.add = hF.preimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X) CategoryTheory.AddMonObj.add)
• CategoryTheory.Functor.FullyFaithful.monObj_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.MonObj (F.obj X)] : CategoryTheory.MonObj.mul = hF.preimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X) CategoryTheory.MonObj.mul)
• CategoryTheory.Functor.FullyFaithful.mapAddMon_preimage_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) {X Y : CategoryTheory.AddMon C} (f : F.mapAddMon.obj X ⟶ F.mapAddMon.obj Y) : (hF.mapAddMon.preimage f).hom = hF.preimage f.hom
• CategoryTheory.Functor.FullyFaithful.mapMon_preimage_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) {X Y : CategoryTheory.Mon C} (f : F.mapMon.obj X ⟶ F.mapMon.obj Y) : (hF.mapMon.preimage f).hom = hF.preimage f.hom
• CommAlgCat.fullyFaithfulUliftFunctor 📋 Mathlib.Algebra.Category.CommAlgCat.Basic
  (R : Type u) [CommRing R] : (CommAlgCat.uliftFunctor R).FullyFaithful
• CategoryTheory.MorphismProperty.Comma.forgetFullyFaithful 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
  {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2} [CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [CategoryTheory.Category.{v_3, u_3} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (P : CategoryTheory.MorphismProperty T) : (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤).FullyFaithful
• CategoryTheory.MorphismProperty.Comma.fullyFaithfulChangeProp 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
  {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2} [CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [CategoryTheory.Category.{v_3, u_3} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {P P' : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} (hP : P ≤ P') [Q.IsMultiplicative] [W.IsMultiplicative] : (CategoryTheory.MorphismProperty.Comma.changeProp L R hP ⋯ ⋯).FullyFaithful
• FGAlgCat.fullyFaithfulUliftFunctor 📋 Mathlib.Algebra.Category.CommAlgCat.FiniteType
  (R : Type u) [CommRing R] : (FGAlgCat.uliftFunctor R).FullyFaithful
• CategoryTheory.yonedaAddMonFullyFaithful 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.yonedaAddMon.FullyFaithful
• CategoryTheory.yonedaMonFullyFaithful 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.yonedaMon.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.homAddEquiv 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Category.{w, u_2} D] [CategoryTheory.CartesianMonoidalCategory D] {M X : C} [CategoryTheory.AddMonObj M] (F : CategoryTheory.Functor C D) [F.Monoidal] (hF : F.FullyFaithful) : (X ⟶ M) ≃+ (F.obj X ⟶ F.obj M)
• CategoryTheory.Functor.FullyFaithful.homMulEquiv 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Category.{w, u_2} D] [CategoryTheory.CartesianMonoidalCategory D] {M X : C} [CategoryTheory.MonObj M] (F : CategoryTheory.Functor C D) [F.Monoidal] (hF : F.FullyFaithful) : (X ⟶ M) ≃* (F.obj X ⟶ F.obj M)
• CategoryTheory.Functor.FullyFaithful.homAddEquiv_apply 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Category.{w, u_2} D] [CategoryTheory.CartesianMonoidalCategory D] {M X : C} [CategoryTheory.AddMonObj M] (F : CategoryTheory.Functor C D) [F.Monoidal] (hF : F.FullyFaithful) (a✝ : X ⟶ M) : (CategoryTheory.Functor.FullyFaithful.homAddEquiv F hF) a✝ = F.map a✝
• CategoryTheory.Functor.FullyFaithful.homMulEquiv_apply 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Category.{w, u_2} D] [CategoryTheory.CartesianMonoidalCategory D] {M X : C} [CategoryTheory.MonObj M] (F : CategoryTheory.Functor C D) [F.Monoidal] (hF : F.FullyFaithful) (a✝ : X ⟶ M) : (CategoryTheory.Functor.FullyFaithful.homMulEquiv F hF) a✝ = F.map a✝
• CategoryTheory.Functor.FullyFaithful.homAddEquiv_symm_apply 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Category.{w, u_2} D] [CategoryTheory.CartesianMonoidalCategory D] {M X : C} [CategoryTheory.AddMonObj M] (F : CategoryTheory.Functor C D) [F.Monoidal] (hF : F.FullyFaithful) (f : F.obj X ⟶ F.obj M) : (CategoryTheory.Functor.FullyFaithful.homAddEquiv F hF).symm f = hF.preimage f
• CategoryTheory.Functor.FullyFaithful.homMulEquiv_symm_apply 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Category.{w, u_2} D] [CategoryTheory.CartesianMonoidalCategory D] {M X : C} [CategoryTheory.MonObj M] (F : CategoryTheory.Functor C D) [F.Monoidal] (hF : F.FullyFaithful) (f : F.obj X ⟶ F.obj M) : (CategoryTheory.Functor.FullyFaithful.homMulEquiv F hF).symm f = hF.preimage f
• CategoryTheory.AddGrp.fullyFaithfulForget₂Mon 📋 Mathlib.CategoryTheory.Monoidal.Grp
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : (CategoryTheory.AddGrp.forget₂Mon C).FullyFaithful
• CategoryTheory.Grp.fullyFaithfulForget₂Mon 📋 Mathlib.CategoryTheory.Monoidal.Grp
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : (CategoryTheory.Grp.forget₂Mon C).FullyFaithful
• CategoryTheory.Functor.FullyFaithful.addGrpObj 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.AddGrpObj (F.obj X)] : CategoryTheory.AddGrpObj X
• CategoryTheory.Functor.FullyFaithful.grpObj 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.GrpObj (F.obj X)] : CategoryTheory.GrpObj X
• CategoryTheory.Functor.FullyFaithful.mapAddGrp 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) : F.mapAddGrp.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.mapGrp 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) : F.mapGrp.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.addGrpObj_neg 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.AddGrpObj (F.obj X)] : CategoryTheory.AddGrpObj.neg = hF.preimage CategoryTheory.AddGrpObj.neg
• CategoryTheory.Functor.FullyFaithful.grpObj_inv 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.GrpObj (F.obj X)] : CategoryTheory.GrpObj.inv = hF.preimage CategoryTheory.GrpObj.inv
• CategoryTheory.Functor.FullyFaithful.addGrpObj_zero 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.AddGrpObj (F.obj X)] : CategoryTheory.AddMonObj.zero = hF.preimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) CategoryTheory.AddMonObj.zero)
• CategoryTheory.Functor.FullyFaithful.grpObj_one 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.GrpObj (F.obj X)] : CategoryTheory.MonObj.one = hF.preimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) CategoryTheory.MonObj.one)
• CategoryTheory.Functor.FullyFaithful.addGrpObj_add 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.AddGrpObj (F.obj X)] : CategoryTheory.AddMonObj.add = hF.preimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X) CategoryTheory.AddMonObj.add)
• CategoryTheory.Functor.FullyFaithful.grpObj_mul 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.GrpObj (F.obj X)] : CategoryTheory.MonObj.mul = hF.preimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X) CategoryTheory.MonObj.mul)
• FGModuleCat.fullyFaithfulULift 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (R : Type u) [Ring R] : (FGModuleCat.ulift R).FullyFaithful
• CategoryTheory.Functor.fullyFaithfulOfCoreflective 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (j : CategoryTheory.Functor C D) [CategoryTheory.Coreflective j] : j.FullyFaithful
• CategoryTheory.Functor.fullyFaithfulOfReflective 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (i : CategoryTheory.Functor D C) [CategoryTheory.Reflective i] : i.FullyFaithful
• CategoryTheory.Adjunction.restrictFullyFaithful 📋 Mathlib.CategoryTheory.Adjunction.Restrict
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u₃} [CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] {iC : CategoryTheory.Functor C C'} {iD : CategoryTheory.Functor D D'} {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) : L ⊣ R
• CategoryTheory.Adjunction.map_restrictFullyFaithful_counit_app 📋 Mathlib.CategoryTheory.Adjunction.Restrict
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u₃} [CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] {iC : CategoryTheory.Functor C C'} {iD : CategoryTheory.Functor D D'} {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) (X : D) : iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X) = CategoryTheory.CategoryStruct.comp (comm1.inv.app (R.obj X)) (CategoryTheory.CategoryStruct.comp (L'.map (comm2.inv.app X)) (adj.counit.app (iD.obj X)))
• CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app 📋 Mathlib.CategoryTheory.Adjunction.Restrict
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u₃} [CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] {iC : CategoryTheory.Functor C C'} {iD : CategoryTheory.Functor D D'} {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) (X : C) : iC.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).unit.app X) = CategoryTheory.CategoryStruct.comp (adj.unit.app (iC.obj X)) (CategoryTheory.CategoryStruct.comp (R'.map (comm1.hom.app X)) (comm2.hom.app (L.obj X)))
• CategoryTheory.Adjunction.map_restrictFullyFaithful_counit_app_assoc 📋 Mathlib.CategoryTheory.Adjunction.Restrict
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u₃} [CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] {iC : CategoryTheory.Functor C C'} {iD : CategoryTheory.Functor D D'} {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) (X : D) {Z : D'} (h : iD.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X)) h = CategoryTheory.CategoryStruct.comp (comm1.inv.app (R.obj X)) (CategoryTheory.CategoryStruct.comp (L'.map (comm2.inv.app X)) (CategoryTheory.CategoryStruct.comp (adj.counit.app (iD.obj X)) h))
• CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app_assoc 📋 Mathlib.CategoryTheory.Adjunction.Restrict
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u₃} [CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] {iC : CategoryTheory.Functor C C'} {iD : CategoryTheory.Functor D D'} {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) (X : C) {Z : C'} (h : iC.obj (R.obj (L.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (iC.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).unit.app X)) h = CategoryTheory.CategoryStruct.comp (adj.unit.app (iC.obj X)) (CategoryTheory.CategoryStruct.comp (R'.map (comm1.hom.app X)) (CategoryTheory.CategoryStruct.comp (comm2.hom.app (L.obj X)) h))
• CategoryTheory.Adjunction.restrictFullyFaithful_homEquiv_apply 📋 Mathlib.CategoryTheory.Adjunction.Restrict
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u₃} [CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] {iC : CategoryTheory.Functor C C'} {iD : CategoryTheory.Functor D D'} {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) {X : C} {Y : D} (f : L.obj X ⟶ Y) : ((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y) f = hiC.preimage (CategoryTheory.CategoryStruct.comp (adj.unit.app (iC.obj X)) (CategoryTheory.CategoryStruct.comp (R'.map (comm1.hom.app X)) (CategoryTheory.CategoryStruct.comp (R'.map (iD.map f)) (comm2.hom.app Y))))
• CategoryTheory.MonoOver.fullyFaithfulForget 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.MonoOver.forget X).FullyFaithful
• CategoryTheory.Preadditive.ofFullyFaithful 📋 Mathlib.CategoryTheory.Preadditive.Transfer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) : CategoryTheory.Preadditive C
• CategoryTheory.Functor.FullyFaithful.additive_ofFullyFaithful 📋 Mathlib.CategoryTheory.Preadditive.Transfer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) : F.Additive
• CategoryTheory.CommMon.fullyFaithfulForget₂Mon 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.CommMon.forget₂Mon C).FullyFaithful
• CategoryTheory.Functor.FullyFaithful.mapCommMon 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} [F.Braided] (hF : F.FullyFaithful) : F.mapCommMon.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.mapCommMon_preimage 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} [F.Braided] (hF : F.FullyFaithful) {X✝ Y✝ : CategoryTheory.CommMon C} (f : F.mapCommMon.obj X✝ ⟶ F.mapCommMon.obj Y✝) : hF.mapCommMon.preimage f = CategoryTheory.CommMon.homMk (hF.mapMon.preimage f.hom)
• CategoryTheory.CommGrp.fullyFaithfulForget₂Grp 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.CommGrp.forget₂Grp C).FullyFaithful
• CategoryTheory.CommGrp.fullyFaithfulForget₂CommMon 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.CommGrp.forget₂CommMon C).FullyFaithful
• CategoryTheory.Functor.FullyFaithful.mapCommGrp 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} [F.Braided] (hF : F.FullyFaithful) : F.mapCommGrp.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.mapCommGrp_preimage 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} [F.Braided] (hF : F.FullyFaithful) {X✝ Y✝ : CategoryTheory.CommGrp C} (f : F.mapCommGrp.obj X✝ ⟶ F.mapCommGrp.obj Y✝) : hF.mapCommGrp.preimage f = CategoryTheory.InducedCategory.homMk (CategoryTheory.Grp.homMk' (hF.mapMon.preimage f.hom.hom))
• AddCommGrpCat.uliftFunctorFullyFaithful 📋 Mathlib.Algebra.Category.Grp.Ulift
  : AddCommGrpCat.uliftFunctor.FullyFaithful
• AddGrpCat.uliftFunctorFullyFaithful 📋 Mathlib.Algebra.Category.Grp.Ulift
  : AddGrpCat.uliftFunctor.FullyFaithful
• CommGrpCat.uliftFunctorFullyFaithful 📋 Mathlib.Algebra.Category.Grp.Ulift
  : CommGrpCat.uliftFunctor.FullyFaithful
• GrpCat.uliftFunctorFullyFaithful 📋 Mathlib.Algebra.Category.Grp.Ulift
  : GrpCat.uliftFunctor.FullyFaithful
• CategoryTheory.Adjunction.fullyFaithfulLOfCompIsoId 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R) (i : L.comp R ≅ CategoryTheory.Functor.id C) : L.FullyFaithful
• CategoryTheory.Adjunction.fullyFaithfulROfCompIsoId 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R) (j : R.comp L ≅ CategoryTheory.Functor.id D) : R.FullyFaithful
• CategoryTheory.Functor.FullyFaithful.hasShift 📋 Mathlib.CategoryTheory.Shift.Basic
  {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_1, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) : CategoryTheory.HasShift C A
• CategoryTheory.Functor.FullyFaithful.hasShift.zero 📋 Mathlib.CategoryTheory.Shift.Basic
  {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_1, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) : s 0 ≅ CategoryTheory.Functor.id C
• CategoryTheory.Functor.FullyFaithful.hasShift.add 📋 Mathlib.CategoryTheory.Shift.Basic
  {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_1, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (a b : A) : s (a + b) ≅ (s a).comp (s b)
• CategoryTheory.Functor.FullyFaithful.hasShift.map_zero_inv_app 📋 Mathlib.CategoryTheory.Shift.Basic
  {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_1, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (X : C) : F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.zero hF s i).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero D A).inv.app (F.obj X)) ((i 0).inv.app X)
• CategoryTheory.Functor.FullyFaithful.hasShift.map_zero_hom_app 📋 Mathlib.CategoryTheory.Shift.Basic
  {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_1, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (X : C) : F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.zero hF s i).hom.app X) = CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) ((CategoryTheory.shiftFunctorZero D A).hom.app (F.obj X))
• CategoryTheory.Functor.FullyFaithful.hasShift.map_add_hom_app 📋 Mathlib.CategoryTheory.Shift.Basic
  {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_1, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (a b : A) (X : C) : F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.add hF s i a b).hom.app X) = CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((i a).inv.app X)) ((i b).inv.app ((s a).obj X))))
• CategoryTheory.Functor.FullyFaithful.hasShift.map_add_inv_app 📋 Mathlib.CategoryTheory.Shift.Basic
  {C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_1, u_2} D] [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (a b : A) (X : C) : F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.add hF s i a b).inv.app X) = CategoryTheory.CategoryStruct.comp ((i b).hom.app ((s a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).inv.app (F.obj X)) ((i (a + b)).inv.app X)))
• CategoryTheory.Functor.CommShift.ofHasShiftOfFullyFaithful 📋 Mathlib.CategoryTheory.Shift.CommShift
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) : F.CommShift A
• CategoryTheory.Functor.shiftFunctorIso_ofHasShiftOfFullyFaithful 📋 Mathlib.CategoryTheory.Shift.CommShift
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C) (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (a : A) : CategoryTheory.Functor.commShiftIso F a = i a
• CategoryTheory.Localization.fullyFaithfulWhiskeringLeft 📋 Mathlib.CategoryTheory.Localization.Predicate
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (E : Type u_4) [CategoryTheory.Category.{v_4, u_4} E] : ((CategoryTheory.Functor.whiskeringLeft C D E).obj L).FullyFaithful
• CategoryTheory.LocalizerMorphism.fullyFaithfulLocalizedFunctor 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
  {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.IsLocalizedFullyFaithful] : (Φ.localizedFunctor L₁ L₂).FullyFaithful
• CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.mk 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
  {C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} (nonempty_fullyFaithful : Nonempty (Φ.localizedFunctor W₁.Q W₂.Q).FullyFaithful) : Φ.IsLocalizedFullyFaithful
• CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.nonempty_fullyFaithful 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
  {C₁ : Type u₁} {C₂ : Type u₂} {inst✝ : CategoryTheory.Category.{v₁, u₁} C₁} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} C₂} {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} [self : Φ.IsLocalizedFullyFaithful] : Nonempty (Φ.localizedFunctor W₁.Q W₂.Q).FullyFaithful
• CategoryTheory.LocalizerMorphism.fullyFaithful 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
  {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor D₁ D₂) [h : Φ.IsLocalizedFullyFaithful] [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] : G.FullyFaithful
• CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.mk' 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
  {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor D₁ D₂) [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] (hG : G.FullyFaithful) : Φ.IsLocalizedFullyFaithful
• CategoryTheory.LocalizerMorphism.nonempty_fullyFaithful_iff 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
  {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor D₁ D₂) [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] {D₁' : Type u₄'} {D₂' : Type u₅'} [CategoryTheory.Category.{v₄', u₄'} D₁'] [CategoryTheory.Category.{v₅', u₅'} D₂'] (L₁' : CategoryTheory.Functor C₁ D₁') (L₂' : CategoryTheory.Functor C₂ D₂') [L₁'.IsLocalization W₁] [L₂'.IsLocalization W₂] (G' : CategoryTheory.Functor D₁' D₂') [CategoryTheory.CatCommSq Φ.functor L₁' L₂' G'] : Nonempty G.FullyFaithful ↔ Nonempty G'.FullyFaithful
• ComplexShape.Embedding.fullyFaithfulExtendFunctor 📋 Mathlib.Algebra.Homology.Embedding.Extend
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] : (e.extendFunctor C).FullyFaithful
• CategoryTheory.fullyFaithfulSheafToPresheaf 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] : (CategoryTheory.sheafToPresheaf J A).FullyFaithful
• CategoryTheory.fullyFaithfulSheafCompose 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) {F : CategoryTheory.Functor A B} [J.HasSheafCompose F] (hF : F.FullyFaithful) : (CategoryTheory.sheafCompose J F).FullyFaithful
• CategoryTheory.fullyFaithfulSheafComposeCompSheafToPresheaf 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) {F : CategoryTheory.Functor A B} [J.HasSheafCompose F] (hF : F.FullyFaithful) : ((CategoryTheory.sheafCompose J F).comp (CategoryTheory.sheafToPresheaf J B)).FullyFaithful
• SheafOfModules.fullyFaithfulForget 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : (SheafOfModules.forget R).FullyFaithful
• CategoryTheory.GrothendieckTopology.fullyFaithfulUliftYoneda 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : (CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).FullyFaithful
• CategoryTheory.GrothendieckTopology.yonedaFullyFaithful 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : J.yoneda.FullyFaithful
• ModuleCat.fullyFaithfulUliftFunctor 📋 Mathlib.Algebra.Category.ModuleCat.Ulift
  (R : Type u) [Ring R] : (ModuleCat.uliftFunctor.{u_2, u_1, u} R).FullyFaithful
• SimplexCategory.Truncated.inclusion.fullyFaithful 📋 Mathlib.AlgebraicTopology.SimplexCategory.Defs
  (n : ℕ) : (SimplexCategory.Truncated.inclusion n).op.FullyFaithful
• CategoryTheory.SimplicialObject.Truncated.cosk.fullyFaithful 📋 Mathlib.AlgebraicTopology.SimplicialObject.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (n : ℕ) [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F] : (CategoryTheory.SimplicialObject.Truncated.cosk n).FullyFaithful
• CategoryTheory.SimplicialObject.Truncated.sk.fullyFaithful 📋 Mathlib.AlgebraicTopology.SimplicialObject.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (n : ℕ) [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F] : (CategoryTheory.SimplicialObject.Truncated.sk n).FullyFaithful
• CategoryTheory.Idempotents.fullyFaithfulToKaroubi 📋 Mathlib.CategoryTheory.Idempotents.Karoubi
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] : (CategoryTheory.Idempotents.toKaroubi C).FullyFaithful
• SSet.Truncated.cosk.fullyFaithful 📋 Mathlib.AlgebraicTopology.SimplicialSet.Basic
  (n : ℕ) : (SSet.Truncated.cosk n).FullyFaithful
• SSet.Truncated.sk.fullyFaithful 📋 Mathlib.AlgebraicTopology.SimplicialSet.Basic
  (n : ℕ) : (SSet.Truncated.sk n).FullyFaithful
• SSet.stdSimplex.fullyFaithful 📋 Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
  : CategoryTheory.Functor.FullyFaithful SSet.stdSimplex
• CochainComplex.Plus.fullyFaithfulι 📋 Mathlib.Algebra.Homology.CochainComplexPlus
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (CochainComplex.Plus.ι C).FullyFaithful
• HomotopyCategory.Plus.fullyFaithfulι 📋 Mathlib.Algebra.Homology.HomotopyCategory.Plus
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] : (HomotopyCategory.Plus.ι C).FullyFaithful
• CategoryTheory.ObjectProperty.IsVerdierLeftLocalizing.fullyFaithful 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} D₁] [CategoryTheory.Category.{v_4, u_4} D₂] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierLeftLocalizing B] {L₁ : CategoryTheory.Functor A.FullSubcategory D₁} {L₂ : CategoryTheory.Functor C D₂} {F : CategoryTheory.Functor D₁ D₂} [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW] (e : L₁.comp F ≅ A.ι.comp L₂) : F.FullyFaithful
• CategoryTheory.ObjectProperty.IsVerdierRightLocalizing.fullyFaithful 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
  {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} D₁] [CategoryTheory.Category.{v_4, u_4} D₂] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierRightLocalizing B] {L₁ : CategoryTheory.Functor A.FullSubcategory D₁} {L₂ : CategoryTheory.Functor C D₂} {F : CategoryTheory.Functor D₁ D₂} [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW] (e : L₁.comp F ≅ A.ι.comp L₂) : F.FullyFaithful
• CategoryTheory.Idempotents.whiskeringLeftObjToKaroubiFullyFaithful 📋 Mathlib.CategoryTheory.Idempotents.FunctorExtension
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] : ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) D).obj (CategoryTheory.Idempotents.toKaroubi C)).FullyFaithful
• AlgebraicGeometry.SheafedSpace.fullyFaithfulForgetToPresheafedSpace 📋 Mathlib.Geometry.RingedSpace.SheafedSpace
  {C : Type u} [CategoryTheory.Category.{v, u} C] : AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.FullyFaithful
• AlgebraicGeometry.Scheme.fullyFaithfulForgetToLocallyRingedSpace 📋 Mathlib.AlgebraicGeometry.Scheme
  : AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.FullyFaithful
• AlgebraicGeometry.Spec.fullyFaithful 📋 Mathlib.AlgebraicGeometry.GammaSpecAdjunction
  : AlgebraicGeometry.Scheme.Spec.FullyFaithful
• AlgebraicGeometry.Spec.fullyFaithfulToLocallyRingedSpace 📋 Mathlib.AlgebraicGeometry.GammaSpecAdjunction
  : AlgebraicGeometry.Spec.toLocallyRingedSpace.FullyFaithful
• TopCat.uliftFunctorFullyFaithful 📋 Mathlib.Topology.Category.TopCat.ULift
  : TopCat.uliftFunctor.FullyFaithful
• AlgebraicGeometry.Scheme.Etale.forgetFullyFaithful 📋 Mathlib.AlgebraicGeometry.Morphisms.Etale
  (X : AlgebraicGeometry.Scheme) : (AlgebraicGeometry.Scheme.Etale.forget X).FullyFaithful
• CategoryTheory.yonedaAddGrpFullyFaithful 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.yonedaAddGrp.FullyFaithful
• CategoryTheory.yonedaGrpFullyFaithful 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.yonedaGrp.FullyFaithful
• AlgebraicGeometry.algSpec.fullyFaithful 📋 Mathlib.AlgebraicGeometry.Group.Affine
  {R : CommRingCat} : (AlgebraicGeometry.algSpec R).FullyFaithful
• AlgebraicGeometry.hopfSpec.fullyFaithful 📋 Mathlib.AlgebraicGeometry.Group.Affine
  {R : CommRingCat} : (AlgebraicGeometry.hopfSpec R).FullyFaithful
• AlgebraicGeometry.bialgSpec.fullyFaithful 📋 Mathlib.AlgebraicGeometry.Group.Affine
  {R : CommRingCat} : (AlgebraicGeometry.bialgSpec R).FullyFaithful

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c