Loogle!

Result

Found 237 declarations mentioning CategoryTheory.End. Of these, only the first 200 are shown.

• CategoryTheory.End 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (X : C) : Type v
• CategoryTheory.End.inhabited 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (X : C) : Inhabited (CategoryTheory.End X)
• CategoryTheory.End.mul 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (X : C) : Mul (CategoryTheory.End X)
• CategoryTheory.End.one 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (X : C) : One (CategoryTheory.End X)
• CategoryTheory.End.monoid 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} : Monoid (CategoryTheory.End X)
• CategoryTheory.End.group 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Groupoid C] (X : C) : Group (CategoryTheory.End X)
• CategoryTheory.End.asHom 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {X : C} (f : CategoryTheory.End X) : X ⟶ X
• CategoryTheory.End.of 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {X : C} (f : X ⟶ X) : CategoryTheory.End X
• CategoryTheory.End.mulActionRight 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} : MulAction (CategoryTheory.End Y) (X ⟶ Y)
• CategoryTheory.End.one_def 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {X : C} : 1 = CategoryTheory.CategoryStruct.id X
• CategoryTheory.isUnit_iff_isIso 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (f : CategoryTheory.End X) : IsUnit f ↔ CategoryTheory.IsIso f
• CategoryTheory.End.mulActionLeft 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} : MulAction (CategoryTheory.End X)ᵐᵒᵖ (X ⟶ Y)
• CategoryTheory.End.ext 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {X : C} {x y : CategoryTheory.End X} (h : x.asHom = y.asHom) : x = y
• CategoryTheory.End.mul_def 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {X : C} (xs ys : CategoryTheory.End X) : xs * ys = CategoryTheory.CategoryStruct.comp ys xs
• 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.Aut.toEnd 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : CategoryTheory.Aut X →* CategoryTheory.End X
• CategoryTheory.InducedCategory.endEquiv 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} {F : D → C} {X : CategoryTheory.InducedCategory C F} : CategoryTheory.End X ≃* CategoryTheory.End (F X)
• CategoryTheory.Aut.unitsEndEquivAut 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.End X)ˣ ≃* CategoryTheory.Aut X
• CategoryTheory.Functor.mapEnd 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] (f : CategoryTheory.Functor C D) : CategoryTheory.End X →* CategoryTheory.End (f.obj X)
• CategoryTheory.End.smul_right 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {r : CategoryTheory.End Y} {f : X ⟶ Y} : r • f = CategoryTheory.CategoryStruct.comp f r
• CategoryTheory.End.smul_left 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {r : (CategoryTheory.End X)ᵐᵒᵖ} {f : X ⟶ Y} : r • f = CategoryTheory.CategoryStruct.comp (MulOpposite.unop r) f
• 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.mapEnd_apply 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] (f : CategoryTheory.Functor C D) (a✝ : X ⟶ X) : (CategoryTheory.Functor.mapEnd X f) a✝ = f.map a✝
• CategoryTheory.InducedCategory.endEquiv_apply 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} {F : D → C} {X : CategoryTheory.InducedCategory C F} (f : X ⟶ X) : CategoryTheory.InducedCategory.endEquiv f = f.hom
• 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.InducedCategory.endEquiv_symm_apply_hom 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} {F : D → C} {X : CategoryTheory.InducedCategory C F} (f : F X ⟶ F X) : (CategoryTheory.InducedCategory.endEquiv.symm f).hom = f
• CategoryTheory.Aut.toEnd_apply 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (x : CategoryTheory.Aut X) : (CategoryTheory.Aut.toEnd X) x = ↑((CategoryTheory.Aut.unitsEndEquivAut X).symm x)
• CategoryTheory.Iso.conj 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) : CategoryTheory.End X ≃* CategoryTheory.End Y
• CategoryTheory.Iso.refl_conj 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (f : CategoryTheory.End X) : (CategoryTheory.Iso.refl X).conj f = f
• CategoryTheory.Iso.conj_id 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) : α.conj (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id Y
• CategoryTheory.Iso.conj_apply 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.End X) : α.conj f = CategoryTheory.CategoryStruct.comp α.inv (CategoryTheory.CategoryStruct.comp f α.hom)
• CategoryTheory.Iso.self_symm_conj 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.End Y) : α.conj (α.symm.conj f) = f
• CategoryTheory.Iso.symm_self_conj 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.End X) : α.symm.conj (α.conj f) = f
• CategoryTheory.Iso.conj_pow 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.End X) (n : ℕ) : α.conj (f ^ n) = α.conj f ^ n
• CategoryTheory.Iso.trans_conj 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (β : Y ≅ Z) (f : CategoryTheory.End X) : (α ≪≫ β).conj f = β.conj (α.conj f)
• CategoryTheory.Iso.conjAut_hom 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) : (α.conjAut f).hom = α.conj f.hom
• CategoryTheory.Iso.conj_comp 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f g : CategoryTheory.End X) : α.conj (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (α.conj f) (α.conj g)
• CategoryTheory.Functor.map_conj 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C D) {X Y : C} (α : X ≅ Y) (f : CategoryTheory.End X) : F.map (α.conj f) = (F.mapIso α).conj (F.map f)
• SemimoduleCat.Iso.conj_eq_conj 📋 Mathlib.Algebra.Category.ModuleCat.Semi
  {S : Type u} [CommSemiring S] {X X' : SemimoduleCat S} (i : X ≅ X') (f : CategoryTheory.End X) : i.conj f = { hom' := i.toLinearEquivₛ.conj (SemimoduleCat.Hom.hom f) }
• CategoryTheory.Preadditive.instAddCommGroupEnd 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) : AddCommGroup (CategoryTheory.End X)
• CategoryTheory.Preadditive.instRingEnd 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X : C} : Ring (CategoryTheory.End X)
• CategoryTheory.Preadditive.instSemiringEnd 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X : C} : Semiring (CategoryTheory.End X)
• CategoryTheory.Preadditive.moduleEndRight 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} : Module (CategoryTheory.End Y) (X ⟶ Y)
• CategoryTheory.Linear.instAlgebraEnd 📋 Mathlib.CategoryTheory.Linear.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommSemiring R] [CategoryTheory.Linear R C] (X : C) : Algebra R (CategoryTheory.End X)
• CategoryTheory.Linear.instModuleEnd 📋 Mathlib.CategoryTheory.Linear.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] (X : C) : Module R (CategoryTheory.End X)
• ModuleCat.mkOfSMul' 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {A : AddCommGrpCat} : (R →+* CategoryTheory.End A) → AddCommGrpCat
• ModuleCat.mkOfSMul 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {A : AddCommGrpCat} (φ : R →+* CategoryTheory.End A) : ModuleCat R
• ModuleCat.instAddCommGroupCarrierMkOfSMul' 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {A : AddCommGrpCat} (φ : R →+* CategoryTheory.End A) : AddCommGroup ↑(ModuleCat.mkOfSMul' φ)
• ModuleCat.instSMulCarrierMkOfSMul' 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {A : AddCommGrpCat} (φ : R →+* CategoryTheory.End A) : SMul R ↑(ModuleCat.mkOfSMul' φ)
• ModuleCat.instModuleCarrierMkOfSMul' 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {A : AddCommGrpCat} (φ : R →+* CategoryTheory.End A) : Module R ↑(ModuleCat.mkOfSMul' φ)
• ModuleCat.endRingEquiv 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] (M : ModuleCat R) : CategoryTheory.End M ≃+* (↑M →ₗ[R] ↑M)
• ModuleCat.mkOfSMul'_smul 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {A : AddCommGrpCat} (φ : R →+* CategoryTheory.End A) (r : R) (x : ↑(ModuleCat.mkOfSMul' φ)) : r • x = (CategoryTheory.ConcreteCategory.hom (have this := φ r; this)) x
• ModuleCat.smul 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] (M : ModuleCat R) : R →+* CategoryTheory.End ((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj M)
• ModuleCat.smulNatTrans 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  (R : Type u) [Ring R] : R →+* CategoryTheory.End (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
• ModuleCat.endRingEquiv_apply 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] (M : ModuleCat R) (f : M.Hom M) : M.endRingEquiv f = f.hom
• ModuleCat.endRingEquiv_symm_apply_hom 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] (M : ModuleCat R) (f : ↑M →ₗ[R] ↑M) : ModuleCat.Hom.hom (M.endRingEquiv.symm f) = f
• ModuleCat.mkOfSMul_smul 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {A : AddCommGrpCat} (φ : R →+* CategoryTheory.End A) (r : R) : (ModuleCat.mkOfSMul φ).smul r = φ r
• ModuleCat.Iso.conj_eq_conj 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {S : Type u} [CommRing S] {X X' : ModuleCat S} (i : X ≅ X') (f : CategoryTheory.End X) : i.conj f = { hom' := i.toLinearEquiv.conj (ModuleCat.Hom.hom f) }
• ModuleCat.smulNatTrans_apply_app 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  (R : Type u) [Ring R] (r : R) (M : ModuleCat R) : ((ModuleCat.smulNatTrans R) r).app M = M.smul r
• ModuleCat.smul_naturality 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {M N : ModuleCat R} (f : M ⟶ N) (r : R) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).map f) (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) ((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).map f)
• ModuleCat.homMk 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {M N : ModuleCat R} (φ : (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj M ⟶ (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj N) (hφ : ∀ (r : R), CategoryTheory.CategoryStruct.comp φ (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ) : M ⟶ N
• ModuleCat.forget₂_map_homMk 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {M N : ModuleCat R} (φ : (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj M ⟶ (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj N) (hφ : ∀ (r : R), CategoryTheory.CategoryStruct.comp φ (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ) : (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).map (ModuleCat.homMk φ hφ) = φ
• ModuleCat.isoMk 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {M N : ModuleCat R} (φ : (CategoryTheory.forget₂ (ModuleCat R) Ab).obj M ≅ (CategoryTheory.forget₂ (ModuleCat R) Ab).obj N) (hφ : ∀ (r : R), CategoryTheory.CategoryStruct.comp φ.hom (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ.hom) : M ≅ N
• ModuleCat.isoMk_hom 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {M N : ModuleCat R} (φ : (CategoryTheory.forget₂ (ModuleCat R) Ab).obj M ≅ (CategoryTheory.forget₂ (ModuleCat R) Ab).obj N) (hφ : ∀ (r : R), CategoryTheory.CategoryStruct.comp φ.hom (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ.hom) : (ModuleCat.isoMk φ hφ).hom = ModuleCat.homMk φ.hom hφ
• ModuleCat.isoMk_symm 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {M N : ModuleCat R} (φ : (CategoryTheory.forget₂ (ModuleCat R) Ab).obj M ≅ (CategoryTheory.forget₂ (ModuleCat R) Ab).obj N) (hφ : ∀ (r : R), CategoryTheory.CategoryStruct.comp φ.hom (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ.hom) : (ModuleCat.isoMk φ hφ).symm = ModuleCat.isoMk φ.symm ⋯
• ModuleCat.isoMk_inv 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {M N : ModuleCat R} (φ : (CategoryTheory.forget₂ (ModuleCat R) Ab).obj M ≅ (CategoryTheory.forget₂ (ModuleCat R) Ab).obj N) (hφ : ∀ (r : R), CategoryTheory.CategoryStruct.comp φ.hom (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ.hom) : (ModuleCat.isoMk φ hφ).inv = ModuleCat.homMk φ.inv ⋯
• ModuleCat.homMk_hom_apply 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {M N : ModuleCat R} (φ : (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj M ⟶ (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj N) (hφ : ∀ (r : R), CategoryTheory.CategoryStruct.comp φ (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ) (a : ↑((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj M)) : (ModuleCat.Hom.hom (ModuleCat.homMk φ hφ)) a = (CategoryTheory.ConcreteCategory.hom φ) a
• ModuleCat.HasColimit.coconePointSMul 📋 Mathlib.Algebra.Category.ModuleCat.Colimits
  {R : Type w} [Ring R] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (ModuleCat R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] : R →+* CategoryTheory.End (CategoryTheory.Limits.colimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)))
• ModuleCat.HasColimit.coconePointSMul_apply 📋 Mathlib.Algebra.Category.ModuleCat.Colimits
  {R : Type w} [Ring R] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (ModuleCat R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] (r : R) : (ModuleCat.HasColimit.coconePointSMul F) r = CategoryTheory.Limits.colimMap { app := fun j => (F.obj j).smul r, naturality := ⋯ }
• ModuleCat.smul_restrictScalars 📋 Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
  {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (r : R) (M : ModuleCat S) : ((ModuleCat.restrictScalars f).obj M).smul r = M.smul (f r)
• CategoryTheory.moduleEndLeft 📋 Mathlib.CategoryTheory.Preadditive.Opposite
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {X Y : C} : Module (CategoryTheory.End X)ᵐᵒᵖ (X ⟶ Y)
• CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite 📋 Mathlib.CategoryTheory.Preadditive.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (G : C) : (G ⟶ G) ≃ₗ[(CategoryTheory.End G)ᵐᵒᵖ] (CategoryTheory.End G)ᵐᵒᵖ
• CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_apply 📋 Mathlib.CategoryTheory.Preadditive.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (G : C) (f : G ⟶ G) : (CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite G) f = { unop' := f }
• CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_symm_apply 📋 Mathlib.CategoryTheory.Preadditive.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (G : C) (x✝ : (CategoryTheory.End G)ᵐᵒᵖ) : (CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite G).symm x✝ = match x✝ with | { unop' := f } => f
• CategoryTheory.preadditiveYonedaObj 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Y : C) : CategoryTheory.Functor Cᵒᵖ (ModuleCat (CategoryTheory.End Y))
• CategoryTheory.preadditiveCoyonedaObj 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) : CategoryTheory.Functor C (ModuleCat (CategoryTheory.End X)ᵐᵒᵖ)
• CategoryTheory.additive_yonedaObj 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) : (CategoryTheory.preadditiveYonedaObj X).Additive
• CategoryTheory.preadditiveYonedaObj_obj_carrier 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Y : C) (X : Cᵒᵖ) : ↑((CategoryTheory.preadditiveYonedaObj Y).obj X) = (Opposite.unop X ⟶ Y)
• CategoryTheory.additive_coyonedaObj 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) : (CategoryTheory.preadditiveCoyonedaObj X).Additive
• CategoryTheory.preadditiveCoyonedaObj_obj_carrier 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Y : C) : ↑((CategoryTheory.preadditiveCoyonedaObj X).obj Y) = (X ⟶ Y)
• CategoryTheory.preadditiveYonedaObj_map 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Y : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.preadditiveYonedaObj Y).map f = ModuleCat.ofHom { toFun := fun g => CategoryTheory.CategoryStruct.comp f.unop g, map_add' := ⋯, map_smul' := ⋯ }
• CategoryTheory.preadditiveYoneda_obj 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Y : C) : CategoryTheory.preadditiveYoneda.obj Y = (CategoryTheory.preadditiveYonedaObj Y).comp (CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End Y)) AddCommGrpCat)
• CategoryTheory.preadditiveCoyonedaObj_map 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.preadditiveCoyonedaObj X).map f = ModuleCat.ofHom { toFun := fun g => CategoryTheory.CategoryStruct.comp g f, map_add' := ⋯, map_smul' := ⋯ }
• CategoryTheory.preadditiveYonedaMap_app 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v, u₁} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] (X : C) (Y : Cᵒᵖ) : (CategoryTheory.preadditiveYonedaMap F X).app Y = AddCommGrpCat.ofHom F.mapAddHom
• CategoryTheory.preadditiveCoyoneda_obj 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : Cᵒᵖ) : CategoryTheory.preadditiveCoyoneda.obj X = (CategoryTheory.preadditiveCoyonedaObj (Opposite.unop X)).comp (CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End (Opposite.unop X))ᵐᵒᵖ) AddCommGrpCat)
• FGModuleCat.Iso.conj_eq_conj 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (R : Type u) [CommRing R] {V W : FGModuleCat R} (i : V ≅ W) (f : CategoryTheory.End V) : i.conj f = FGModuleCat.ofHom ((FGModuleCat.isoToLinearEquiv i).conj (ModuleCat.Hom.hom f.hom))
• FGModuleCat.Iso.conj_hom_eq_conj 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (R : Type u) [CommRing R] {V W : FGModuleCat R} (i : V ≅ W) (f : CategoryTheory.End V) : ModuleCat.Hom.hom (i.conj f).hom = (FGModuleCat.isoToLinearEquiv i).conj (ModuleCat.Hom.hom f.hom)
• PresheafOfModules.smul_map 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {U V : Cᵒᵖ} (f : U ⟶ V) (r : ↑(R.obj U)) : CategoryTheory.CategoryStruct.comp ((M.obj U).smul r) (M.presheaf.map f) = CategoryTheory.CategoryStruct.comp (M.presheaf.map f) ((M.obj V).smul ((CategoryTheory.ConcreteCategory.hom (R.map f)) r))
• PresheafOfModules.smul_map_assoc 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {U V : Cᵒᵖ} (f : U ⟶ V) (r : ↑(R.obj U)) {Z : AddCommGrpCat} (h : M.presheaf.obj V ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((M.obj U).smul r) (M.presheaf.map f)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (M.presheaf.map f) ((M.obj V).smul ((CategoryTheory.ConcreteCategory.hom (R.map f)) r))) h
• CategoryTheory.instNontrivialEndOfSimple 📋 Mathlib.CategoryTheory.Simple
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) [CategoryTheory.Simple X] : Nontrivial (CategoryTheory.End X)
• CategoryTheory.End.ext_iff 📋 Mathlib.Algebra.Category.ModuleCat.Tannaka
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {X : C} {x y : CategoryTheory.End X} : x = y ↔ x.asHom = y.asHom
• ringEquivEndForget₂ 📋 Mathlib.Algebra.Category.ModuleCat.Tannaka
  (R : Type u) [Ring R] : R ≃+* CategoryTheory.End (CategoryTheory.AdditiveFunctor.of (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))
• TopModuleCat.endRingEquiv 📋 Mathlib.Algebra.Category.ModuleCat.Topology.Basic
  {R : Type u} [Ring R] [TopologicalSpace R] (M : TopModuleCat R) : CategoryTheory.End M ≃+* (↑M.toModuleCat →L[R] ↑M.toModuleCat)
• TopModuleCat.endRingEquiv_apply 📋 Mathlib.Algebra.Category.ModuleCat.Topology.Basic
  {R : Type u} [Ring R] [TopologicalSpace R] (M : TopModuleCat R) (f : M.Hom M) : M.endRingEquiv f = f.hom
• TopModuleCat.endRingEquiv_symm_apply 📋 Mathlib.Algebra.Category.ModuleCat.Topology.Basic
  {R : Type u} [Ring R] [TopologicalSpace R] (M : TopModuleCat R) (f : ↑M.toModuleCat →L[R] ↑M.toModuleCat) : M.endRingEquiv.symm f = TopModuleCat.ofHom f
• AlgebraicGeometry.Scheme.Modules.smul 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X : AlgebraicGeometry.Scheme} {M : X.Modules} {U : X.Opens} : ↑(X.presheaf.obj (Opposite.op U)) →+* CategoryTheory.End (M.presheaf.obj (Opposite.op U))
• AlgebraicGeometry.Scheme.Modules.map_comp_smul 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X : AlgebraicGeometry.Scheme} {M : X.Modules} {U V : X.Opens} (i : U ⟶ V) (r : ↑(X.presheaf.obj (Opposite.op V))) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul r) (M.presheaf.map i.op) = CategoryTheory.CategoryStruct.comp (M.presheaf.map i.op) (AlgebraicGeometry.Scheme.Modules.smul ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) r))
• AlgebraicGeometry.Scheme.Modules.map_comp_smul_assoc 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X : AlgebraicGeometry.Scheme} {M : X.Modules} {U V : X.Opens} (i : U ⟶ V) (r : ↑(X.presheaf.obj (Opposite.op V))) {Z : Ab} (h : M.presheaf.obj (Opposite.op U) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul r) (CategoryTheory.CategoryStruct.comp (M.presheaf.map i.op) h) = CategoryTheory.CategoryStruct.comp (M.presheaf.map i.op) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) r)) h)
• AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_inv 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules) (U : X.Opens) (r : ↑(Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)))) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul r) (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv (AlgebraicGeometry.Scheme.Modules.smul ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).hom) r))
• AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_hom 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules) (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul r) (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).hom = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).hom (AlgebraicGeometry.Scheme.Modules.smul ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).inv) r))
• AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_hom_assoc 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules) (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))) {Z : Ab} (h : M.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul r) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).hom h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).inv) r)) h)
• AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_inv_assoc 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules) (U : X.Opens) (r : ↑(Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)))) {Z : Ab} (h : (M.restrict f).presheaf.obj (Opposite.op U) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul r) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).hom) r)) h)
• AlgebraicGeometry.Scheme.Modules.smul_apply 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X : AlgebraicGeometry.Scheme} {M : X.Modules} {U : X.Opens} (r : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑(M.presheaf.obj (Opposite.op U))) : (AddCommGrpCat.Hom.hom (AlgebraicGeometry.Scheme.Modules.smul r)) x = r • x
• CategoryTheory.SingleObj.functor 📋 Mathlib.CategoryTheory.SingleObj
  {M : Type u} [Monoid M] {C : Type v} [CategoryTheory.Category.{w, v} C] {X : C} (f : M →* CategoryTheory.End X) : CategoryTheory.Functor (CategoryTheory.SingleObj M) C
• CategoryTheory.SingleObj.toEnd 📋 Mathlib.CategoryTheory.SingleObj
  (M : Type u) [Monoid M] : M ≃* CategoryTheory.End (CategoryTheory.SingleObj.star M)
• CategoryTheory.SingleObj.functor_obj 📋 Mathlib.CategoryTheory.SingleObj
  {M : Type u} [Monoid M] {C : Type v} [CategoryTheory.Category.{w, v} C] {X : C} (f : M →* CategoryTheory.End X) (x✝ : CategoryTheory.SingleObj M) : (CategoryTheory.SingleObj.functor f).obj x✝ = X
• CategoryTheory.SingleObj.functor_map 📋 Mathlib.CategoryTheory.SingleObj
  {M : Type u} [Monoid M] {C : Type v} [CategoryTheory.Category.{w, v} C] {X : C} (f : M →* CategoryTheory.End X) {X✝ Y✝ : CategoryTheory.SingleObj M} (a : X✝ ⟶ Y✝) : (CategoryTheory.SingleObj.functor f).map a = f a
• CategoryTheory.SingleObj.toEnd_def 📋 Mathlib.CategoryTheory.SingleObj
  (M : Type u) [Monoid M] (x : M) : (CategoryTheory.SingleObj.toEnd M) x = x
• Units.toAut_hom 📋 Mathlib.CategoryTheory.SingleObj
  (M : Type u) [Monoid M] (x : Mˣ) : ((Units.toAut M) x).hom = (CategoryTheory.SingleObj.toEnd M) ↑x
• Units.toAut_inv 📋 Mathlib.CategoryTheory.SingleObj
  (M : Type u) [Monoid M] (x : Mˣ) : ((Units.toAut M) x).inv = (CategoryTheory.SingleObj.toEnd M) ↑x⁻¹
• CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (P : C) : CategoryTheory.Projective P ↔ (CategoryTheory.preadditiveCoyonedaObj P).PreservesEpimorphisms
• CategoryTheory.preservesLimits_preadditiveYonedaObj 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) : CategoryTheory.Limits.PreservesLimits (CategoryTheory.preadditiveYonedaObj X)
• CategoryTheory.preservesLimits_preadditiveCoyonedaObj 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) : CategoryTheory.Limits.PreservesLimits (CategoryTheory.preadditiveCoyonedaObj X)
• CategoryTheory.preservesFiniteColimits_preadditiveCoyonedaObj_of_projective 📋 Mathlib.CategoryTheory.Abelian.Projective.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : C) [hP : CategoryTheory.Projective P] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveCoyonedaObj P)
• CategoryTheory.projective_of_preservesFiniteColimits_preadditiveCoyonedaObj 📋 Mathlib.CategoryTheory.Abelian.Projective.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : C) [hP : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveCoyonedaObj P)] : CategoryTheory.Projective P
• CategoryTheory.preservesHomology_preadditiveCoyonedaObj_of_projective 📋 Mathlib.CategoryTheory.Abelian.Projective.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : C) [hP : CategoryTheory.Projective P] : (CategoryTheory.preadditiveCoyonedaObj P).PreservesHomology
• CategoryTheory.isCoseparator_iff_faithful_preadditiveYonedaObj 📋 Mathlib.CategoryTheory.Generator.Preadditive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (G : C) : CategoryTheory.IsCoseparator G ↔ (CategoryTheory.preadditiveYonedaObj G).Faithful
• CategoryTheory.isSeparator_iff_faithful_preadditiveCoyonedaObj 📋 Mathlib.CategoryTheory.Generator.Preadditive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (G : C) : CategoryTheory.IsSeparator G ↔ (CategoryTheory.preadditiveCoyonedaObj G).Faithful
• CategoryTheory.Abelian.full_comp_preadditiveCoyonedaObj 📋 Mathlib.CategoryTheory.Abelian.Yoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor D C) [F.Full] {G : C} [CategoryTheory.Projective G] (hG : CategoryTheory.IsSeparator G) (hG₂ : ∀ (X : D), ∃ p, CategoryTheory.Epi p) : (F.comp (CategoryTheory.preadditiveCoyonedaObj G)).Full
• CategoryTheory.Abelian.preadditiveCoyonedaObj_map_surjective 📋 Mathlib.CategoryTheory.Abelian.Yoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {G : C} [CategoryTheory.Projective G] (hG : CategoryTheory.IsSeparator G) {X : C} (p : G ⟶ X) [CategoryTheory.Epi p] {Y : C} : Function.Surjective (CategoryTheory.preadditiveCoyonedaObj G).map
• CategoryTheory.IsGrothendieckAbelian.tensorObj 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] (G : C) : CategoryTheory.Functor (ModuleCat (CategoryTheory.End G)ᵐᵒᵖ) C
• CategoryTheory.IsGrothendieckAbelian.instIsLeftAdjointModuleCatMulOppositeEndTensorObj 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G : C} : (CategoryTheory.IsGrothendieckAbelian.tensorObj G).IsLeftAdjoint
• CategoryTheory.IsGrothendieckAbelian.instIsRightAdjointModuleCatMulOppositeEndPreadditiveCoyonedaObj 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G : C} : (CategoryTheory.preadditiveCoyonedaObj G).IsRightAdjoint
• CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesFiniteLimits 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] (G : C) (hG : CategoryTheory.IsSeparator G) : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.IsGrothendieckAbelian.tensorObj G)
• CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.full 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] (G : C) (hG : CategoryTheory.IsSeparator G) : (CategoryTheory.preadditiveCoyonedaObj G).Full
• CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesInjectiveObjects 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] (G : C) (hG : CategoryTheory.IsSeparator G) : (CategoryTheory.preadditiveCoyonedaObj G).PreservesInjectiveObjects
• CategoryTheory.IsGrothendieckAbelian.tensorObjPreadditiveCoyonedaObjAdjunction 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] (G : C) : CategoryTheory.IsGrothendieckAbelian.tensorObj G ⊣ CategoryTheory.preadditiveCoyonedaObj G
• CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G A : C} {M : ModuleCat (CategoryTheory.End G)ᵐᵒᵖ} (g : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ A)) : (∐ fun x => G) ⟶ A
• CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.exists_d_comp_eq_d 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G : C} (hG : CategoryTheory.IsSeparator G) {A : C} (B : C) [CategoryTheory.Injective B] {M : ModuleCat (CategoryTheory.End G)ᵐᵒᵖ} (g : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ A)) (hg : CategoryTheory.Mono g) (f : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ B)) : ∃ l, CategoryTheory.CategoryStruct.comp (CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d g) l = CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d f
• CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G A : C} {M : ModuleCat (CategoryTheory.End G)ᵐᵒᵖ} (g : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ A)) (m : ↑M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => G) m) (CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d g) = (ModuleCat.Hom.hom g) m
• CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d_assoc 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G A : C} {M : ModuleCat (CategoryTheory.End G)ᵐᵒᵖ} (g : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ A)) (m : ↑M) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => G) m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d g) h) = CategoryTheory.CategoryStruct.comp ((ModuleCat.Hom.hom g) m) h
• CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.kernel_ι_d_comp_d 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G : C} (hG : CategoryTheory.IsSeparator G) {A B : C} {M : ModuleCat (CategoryTheory.End G)ᵐᵒᵖ} (g : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ A)) (hg : CategoryTheory.Mono g) (f : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ B)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d g)) (CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d f) = 0
• CategoryTheory.Injective.injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (J : C) : CategoryTheory.Injective J ↔ (CategoryTheory.preadditiveYonedaObj J).PreservesEpimorphisms
• CategoryTheory.injective_of_preservesFiniteColimits_preadditiveYonedaObj 📋 Mathlib.CategoryTheory.Abelian.Injective.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (J : C) [hP : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveYonedaObj J)] : CategoryTheory.Injective J
• CategoryTheory.preservesFiniteColimits_preadditiveYonedaObj_of_injective 📋 Mathlib.CategoryTheory.Abelian.Injective.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (J : C) [hP : CategoryTheory.Injective J] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveYonedaObj J)
• CategoryTheory.preservesHomology_preadditiveYonedaObj_of_injective 📋 Mathlib.CategoryTheory.Abelian.Injective.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (J : C) [hJ : CategoryTheory.Injective J] : (CategoryTheory.preadditiveYonedaObj J).PreservesHomology
• CategoryTheory.ActionCategory.stabilizerIsoEnd 📋 Mathlib.CategoryTheory.Action
  (M : Type u_1) [Monoid M] {X : Type u} [MulAction M X] (x : X) : ↥(MulAction.stabilizerSubmonoid M x) ≃* CategoryTheory.End ⟨(), x⟩
• CategoryTheory.ActionCategory.stabilizerIsoEnd_apply 📋 Mathlib.CategoryTheory.Action
  (M : Type u_1) [Monoid M] {X : Type u} [MulAction M X] (x : X) (f : ↥(MulAction.stabilizerSubmonoid M x)) : (CategoryTheory.ActionCategory.stabilizerIsoEnd M x) f = f
• CategoryTheory.ActionCategory.stabilizerIsoEnd_symm_apply 📋 Mathlib.CategoryTheory.Action
  (M : Type u_1) [Monoid M] {X : Type u} [MulAction M X] (x : X) (f : CategoryTheory.End ⟨(), x⟩) : (CategoryTheory.ActionCategory.stabilizerIsoEnd M x).symm f = f
• CategoryTheory.ActionCategory.endMulEquivSubgroup 📋 Mathlib.CategoryTheory.Action
  {G : Type u_2} [Group G] (H : Subgroup G) : CategoryTheory.End ((CategoryTheory.ActionCategory.objEquiv G (G ⧸ H)) ↑1) ≃* ↥H
• Action.mk 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (V✝ : V) (ρ : G →* CategoryTheory.End V✝) : Action V G
• Action.ρ 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (self : Action V G) : G →* CategoryTheory.End self.V
• Action.trivial_ρ 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] (X : V) : (Action.trivial G X).ρ = 1
• Action.ρ_one 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (A : Action V G) : A.ρ 1 = CategoryTheory.CategoryStruct.id A.V
• Action.res_obj_ρ 📋 Mathlib.CategoryTheory.Action.Basic
  (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G →* H) (M : Action V H) : ((Action.res V f).obj M).ρ = M.ρ.comp f
• Action.FunctorCategoryEquivalence.functor_obj_map 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (M : Action V G) {X✝ Y✝ : CategoryTheory.SingleObj G} (g : X✝ ⟶ Y✝) : (Action.FunctorCategoryEquivalence.functor.obj M).map g = M.ρ g
• Action.FunctorCategoryEquivalence.inverse_obj_ρ_apply 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (F : CategoryTheory.Functor (CategoryTheory.SingleObj G) V) (g : G) : (Action.FunctorCategoryEquivalence.inverse.obj F).ρ g = F.map g
• Action.res_map_hom 📋 Mathlib.CategoryTheory.Action.Basic
  (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G →* H) {X✝ Y✝ : Action V H} (p : X✝ ⟶ Y✝) : ((Action.res V f).map p).hom = p.hom
• Action.Hom.comm 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (self : M.Hom N) (g : G) : CategoryTheory.CategoryStruct.comp (M.ρ g) self.hom = CategoryTheory.CategoryStruct.comp self.hom (N.ρ g)
• Action.Hom.mk 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (hom : M.V ⟶ N.V) (comm : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) hom = CategoryTheory.CategoryStruct.comp hom (N.ρ g) := by cat_disch) : M.Hom N
• Action.isIso_hom_mk 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M.V ⟶ N.V) [CategoryTheory.IsIso f] (w : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f = CategoryTheory.CategoryStruct.comp f (N.ρ g)) : CategoryTheory.IsIso { hom := f, comm := w }
• Action.Hom.comm_assoc 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (self : M.Hom N) (g : G) {Z : V} (h : N.V ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.ρ g) (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp (N.ρ g) h)
• Action.mkIso 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M.V ≅ N.V) (comm : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g) := by cat_disch) : M ≅ N
• CategoryTheory.Functor.mapAction_obj_ρ_apply 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {W : Type u_2} [CategoryTheory.Category.{v_2, u_2} W] (F : CategoryTheory.Functor V W) (G : Type u_3) [Monoid G] (M : Action V G) (g : G) : ((F.mapAction G).obj M).ρ g = F.map (M.ρ g)
• Action.ρAut_apply_hom 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Group G] (A : Action V G) (g : G) : (A.ρAut g).hom = A.ρ g
• Action.mkIso_hom_hom 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M.V ≅ N.V) (comm : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g) := by cat_disch) : (Action.mkIso f comm).hom.hom = f.hom
• Action.mkIso_inv_hom 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M.V ≅ N.V) (comm : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g) := by cat_disch) : (Action.mkIso f comm).inv.hom = f.inv
• Action.ρAut_apply_inv 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Group G] (A : Action V G) (g : G) : (A.ρAut g).inv = A.ρ g⁻¹
• Action.FunctorCategoryEquivalence.functor_map_app 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {X✝ Y✝ : Action V G} (f : X✝ ⟶ Y✝) (x✝ : CategoryTheory.SingleObj G) : (Action.FunctorCategoryEquivalence.functor.map f).app x✝ = f.hom
• Action.FunctorCategoryEquivalence.inverse_map_hom 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.SingleObj G) V} (f : X✝ ⟶ Y✝) : (Action.FunctorCategoryEquivalence.inverse.map f).hom = f.app PUnit.unit
• Action.Iso.conj_ρ 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M ≅ N) (g : G) : N.ρ g = ((Action.forget V G).mapIso f).conj (M.ρ g)
• CategoryTheory.Functor.mapAction_map_hom 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {W : Type u_2} [CategoryTheory.Category.{v_2, u_2} W] (F : CategoryTheory.Functor V W) (G : Type u_3) [Monoid G] {X✝ Y✝ : Action V G} (f : X✝ ⟶ Y✝) : ((F.mapAction G).map f).hom = F.map f.hom
• TypeCat.instCoeFunEndForall 📋 Mathlib.CategoryTheory.Action.Concrete
  (X : Type u) : CoeFun (CategoryTheory.End X) fun x => X → X
• TypeCat.endEquiv 📋 Mathlib.CategoryTheory.Action.Concrete
  (X : Type u) : Function.End X ≃* CategoryTheory.End X
• TypeCat.endEquiv_apply 📋 Mathlib.CategoryTheory.Action.Concrete
  (X : Type u) (f : Function.End X) : (TypeCat.endEquiv X) f = TypeCat.ofHom f
• Action.ofMulAction_ρ 📋 Mathlib.CategoryTheory.Action.Concrete
  (G : Type u_1) (H : Type u) [Monoid G] [MulAction G H] : (Action.ofMulAction G H).ρ = (TypeCat.endEquiv H).toMonoidHom.comp MulAction.toEndHom
• TypeCat.endEquiv_symm_apply 📋 Mathlib.CategoryTheory.Action.Concrete
  (X : Type u) (f : CategoryTheory.End X) (a : X) : (TypeCat.endEquiv X).symm f a = (CategoryTheory.ConcreteCategory.hom f) a
• Action.ofMulAction_apply 📋 Mathlib.CategoryTheory.Action.Concrete
  {G : Type u_1} {H : Type u_2} [Monoid G] [MulAction G H] (g : G) (x : H) : (CategoryTheory.ConcreteCategory.hom ((Action.ofMulAction G H).ρ g)) x = g • x
• Action.FintypeCat.toEndHom 📋 Mathlib.CategoryTheory.Action.Concrete
  {G : Type u_1} [Group G] (N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] : G →* CategoryTheory.End (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)))
• Action.FintypeCat.ofMulAction_apply 📋 Mathlib.CategoryTheory.Action.Concrete
  {G : Type u_1} {H : FintypeCat} [Monoid G] [MulAction G H.obj] (g : G) (x : H.obj) : (CategoryTheory.ConcreteCategory.hom ((Action.FintypeCat.ofMulAction G H).ρ g)) x = g • x
• Action.ρ_inv_self_apply 📋 Mathlib.CategoryTheory.Action.Concrete
  {G : Type u} [Group G] {A : Action (Type u) G} (g : G) (x : A.V) : (CategoryTheory.ConcreteCategory.hom (A.ρ g⁻¹)) ((CategoryTheory.ConcreteCategory.hom (A.ρ g)) x) = x
• Action.ρ_self_inv_apply 📋 Mathlib.CategoryTheory.Action.Concrete
  {G : Type u} [Group G] {A : Action (Type u) G} (g : G) (x : A.V) : (CategoryTheory.ConcreteCategory.hom (A.ρ g)) ((CategoryTheory.ConcreteCategory.hom (A.ρ g⁻¹)) x) = x
• Action.FintypeCat.quotientToEndHom 📋 Mathlib.CategoryTheory.Action.Concrete
  {G : Type u_1} [Group G] (H N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] : ↥H ⧸ N.subgroupOf H →* CategoryTheory.End (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)))
• Action.FintypeCat.toEndHom_trivial_of_mem 📋 Mathlib.CategoryTheory.Action.Concrete
  {G : Type u_1} [Group G] {N : Subgroup G} [Fintype (G ⧸ N)] [N.Normal] {n : G} (hn : n ∈ N) : (Action.FintypeCat.toEndHom N) n = CategoryTheory.CategoryStruct.id (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)))
• Action.FintypeCat.toEndHom_apply 📋 Mathlib.CategoryTheory.Action.Concrete
  {G : Type u_1} [Group G] (N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] (g h : G) : (CategoryTheory.ConcreteCategory.hom ((Action.FintypeCat.toEndHom N) g).hom) ⟦h⟧ = ⟦h * g⁻¹⟧
• Action.FintypeCat.quotientToEndHom_mk 📋 Mathlib.CategoryTheory.Action.Concrete
  {G : Type u_1} [Group G] (H N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] (x : ↥H) (g : G) : (CategoryTheory.ConcreteCategory.hom ((Action.FintypeCat.quotientToEndHom H N) ⟦x⟧).hom) ⟦g⟧ = ⟦g * ↑x⁻¹⟧
• Action.isContinuous_def 📋 Mathlib.CategoryTheory.Action.Continuous
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {FV : V → V → Type u_2} {CV : V → Type u_3} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_4} [Monoid G] [TopologicalSpace G] (X : Action V G) : X.IsContinuous ↔ Continuous fun p => (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ V TopCat).map (X.ρ p.1))) p.2
• Action.tensorUnitIso 📋 Mathlib.CategoryTheory.Action.Monoidal
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.MonoidalCategory V] {X : V} (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ≅ X) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V G) ≅ { V := X, ρ := 1 }
• Action.tensorUnit_ρ 📋 Mathlib.CategoryTheory.Action.Monoidal
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.MonoidalCategory V] {g : G} : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V G)).ρ g = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)
• Action.tensor_ρ 📋 Mathlib.CategoryTheory.Action.Monoidal
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.MonoidalCategory V] {X Y : Action V G} {g : G} : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ρ g = CategoryTheory.MonoidalCategoryStruct.tensorHom (X.ρ g) (Y.ρ g)
• Action.leftDual_ρ 📋 Mathlib.CategoryTheory.Action.Monoidal
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_3} [Group H] (X : Action V H) [CategoryTheory.LeftRigidCategory V] (h : H) : (ᘁX).ρ h = ᘁX.ρ h⁻¹
• Action.rightDual_ρ 📋 Mathlib.CategoryTheory.Action.Monoidal
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_3} [Group H] (X : Action V H) [CategoryTheory.RightRigidCategory V] (h : H) : Xᘁ.ρ h = X.ρ h⁻¹ᘁ
• Action.leftRegularTensorIso_hom_hom 📋 Mathlib.CategoryTheory.Action.Monoidal
  (G : Type u) [Group G] (X : Action (Type u) G) : (Action.leftRegularTensorIso G X).hom.hom = { toFun := fun g => (g.1, (CategoryTheory.ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2), invFun := fun g => (g.1, (CategoryTheory.ConcreteCategory.hom (X.ρ g.1)) g.2), left_inv := ⋯, right_inv := ⋯ }.toIso.hom
• Action.leftRegularTensorIso_inv_hom 📋 Mathlib.CategoryTheory.Action.Monoidal
  (G : Type u) [Group G] (X : Action (Type u) G) : (Action.leftRegularTensorIso G X).inv.hom = { toFun := fun g => (g.1, (CategoryTheory.ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2), invFun := fun g => (g.1, (CategoryTheory.ConcreteCategory.hom (X.ρ g.1)) g.2), left_inv := ⋯, right_inv := ⋯ }.toIso.inv
• CategoryTheory.PreGaloisCategory.endEquivAutGalois 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.End F ≃ CategoryTheory.PreGaloisCategory.AutGalois F
• CategoryTheory.PreGaloisCategory.FibreFunctor.end_isIso 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.End F) : CategoryTheory.IsIso f
• CategoryTheory.PreGaloisCategory.FibreFunctor.end_isUnit 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.End F) : IsUnit f
• CategoryTheory.PreGaloisCategory.endMulEquivAutGalois 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.End F ≃* (CategoryTheory.PreGaloisCategory.AutGalois F)ᵐᵒᵖ
• CategoryTheory.PreGaloisCategory.endEquivSectionsFibers 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.End F ≃ ↑((CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).comp (F.comp FintypeCat.incl)).sections
• CategoryTheory.PreGaloisCategory.endEquivAutGalois_mul 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f g : CategoryTheory.End F) : (CategoryTheory.PreGaloisCategory.endEquivAutGalois F) (CategoryTheory.CategoryStruct.comp g f) = (CategoryTheory.PreGaloisCategory.endEquivAutGalois F) g * (CategoryTheory.PreGaloisCategory.endEquivAutGalois F) f
• CategoryTheory.PreGaloisCategory.endEquivAutGalois_π 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.End F) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : (CategoryTheory.ConcreteCategory.hom (F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F A) ((CategoryTheory.PreGaloisCategory.endEquivAutGalois F) f)).hom)) A.pt = (CategoryTheory.ConcreteCategory.hom (f.app A.obj)) A.pt
• CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.End F) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : (CategoryTheory.ConcreteCategory.hom (F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F A) (MulOpposite.unop ((CategoryTheory.PreGaloisCategory.endMulEquivAutGalois F) f))).hom)) A.pt = (CategoryTheory.ConcreteCategory.hom (f.app A.obj)) A.pt
• CategoryTheory.PreGaloisCategory.endEquivSectionsFibers_π 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.End F) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : ↑((CategoryTheory.PreGaloisCategory.endEquivSectionsFibers F) f) A = (CategoryTheory.ConcreteCategory.hom (f.app A.obj)) A.pt
• CategoryTheory.HomOrthogonal.matrixDecomposition 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} : ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃ ((i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i)))
• CategoryTheory.HomOrthogonal.equiv_of_iso 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [∀ (i : ι), InvariantBasisNumber (CategoryTheory.End (s i))] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} (i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)) : ∃ e, ∀ (a : α), g (e a) = f a
• CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} : ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃+ ((i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i)))
• CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {R : Type u_2} [Semiring R] [CategoryTheory.Linear R C] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} : ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃ₗ[R] (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i))
• CategoryTheory.HomOrthogonal.matrixDecomposition_apply 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} (z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) (i : ι) (j : ↑(g ⁻¹' {i})) (k : ↑(f ⁻¹' {i})) : o.matrixDecomposition z i j k = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.components z ↑k ↑j) (CategoryTheory.eqToHom ⋯))
• CategoryTheory.HomOrthogonal.matrixDecomposition_id 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (o : CategoryTheory.HomOrthogonal s) {α : Type} [Finite α] {f : α → ι} (i : ι) : o.matrixDecomposition (CategoryTheory.CategoryStruct.id (⨁ fun a => s (f a))) i = 1
• CategoryTheory.HomOrthogonal.matrixDecomposition_symm_apply 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} (z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i))) : o.matrixDecomposition.symm z = CategoryTheory.Limits.biproduct.matrix fun j k => if h : f j = g k then CategoryTheory.CategoryStruct.comp (z (f j) ⟨k, ⋯⟩ ⟨j, ⋯⟩) (CategoryTheory.eqToHom ⋯) else 0

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