Loogle!

Result

Found 216 declarations mentioning Action.V. Of these, only the first 200 are shown.

• Action.V 📋 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) : V
• Action.trivial_V 📋 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).V = X
• Action.forget_obj 📋 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) : (Action.forget V G).obj M = M.V
• Action.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} (self : M.Hom N) : M.V ⟶ N.V
• Action.hom_injective 📋 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} : Function.Injective Action.Hom.hom
• Action.Hom.id_hom 📋 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) : (Action.Hom.id M).hom = CategoryTheory.CategoryStruct.id M.V
• 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.instFunLikeHomSubtypeV 📋 Mathlib.CategoryTheory.Action.Basic
  (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] {FV : V → V → Type u_3} {CV : V → Type u_4} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] (M N : Action V G) : FunLike (Action.HomSubtype V G M N) (CV M.V) (CV N.V)
• Action.FunctorCategoryEquivalence.functor_obj_obj 📋 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✝ : CategoryTheory.SingleObj G) : (Action.FunctorCategoryEquivalence.functor.obj M).obj x✝ = M.V
• Action.FunctorCategoryEquivalence.inverse_obj_V 📋 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) : (Action.FunctorCategoryEquivalence.inverse.obj F).V = F.obj PUnit.unit
• Action.instIsIsoHomHom 📋 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) : CategoryTheory.IsIso f.hom.hom
• Action.instIsIsoHomInv 📋 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) : CategoryTheory.IsIso f.inv.hom
• Action.id_hom 📋 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) : (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.V
• Action.instConcreteCategoryHomSubtypeV 📋 Mathlib.CategoryTheory.Action.Basic
  (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] {FV : V → V → Type u_3} {CV : V → Type u_4} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] : CategoryTheory.ConcreteCategory (Action V G) (Action.HomSubtype V G)
• CategoryTheory.Functor.mapAction_obj_V 📋 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) : ((F.mapAction G).obj M).V = F.obj M.V
• Action.res_obj_V 📋 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).V = M.V
• Action.Hom.ext 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} V} {G : Type u_2} {inst✝¹ : Monoid G} {M N : Action V G} {x y : M.Hom N} (hom : x.hom = y.hom) : x = y
• Action.Hom.ext_iff 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} V} {G : Type u_2} {inst✝¹ : Monoid G} {M N : Action V G} {x y : M.Hom N} : x = y ↔ x.hom = y.hom
• Action.isIso_of_hom_isIso 📋 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) [CategoryTheory.IsIso f.hom] : CategoryTheory.IsIso f
• Action.hasForgetToV 📋 Mathlib.CategoryTheory.Action.Basic
  (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] {FV : V → V → Type u_3} {CV : V → Type u_4} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] : CategoryTheory.HasForget₂ (Action V G) V
• Action.forget_map 📋 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✝) : (Action.forget V G).map f = f.hom
• Action.ρAut 📋 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 →* CategoryTheory.Aut A.V
• Action.Hom.comp_hom 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N K : Action V G} (p : M.Hom N) (q : N.Hom K) : (p.comp q).hom = CategoryTheory.CategoryStruct.comp p.hom q.hom
• Action.hom_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 ≅ N) : CategoryTheory.CategoryStruct.comp f.hom.hom f.inv.hom = CategoryTheory.CategoryStruct.id M.V
• Action.inv_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 ≅ N) : CategoryTheory.CategoryStruct.comp f.inv.hom f.hom.hom = CategoryTheory.CategoryStruct.id N.V
• Action.hom_ext 📋 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} (φ₁ φ₂ : M ⟶ N) (h : φ₁.hom = φ₂.hom) : φ₁ = φ₂
• Action.hom_ext_iff 📋 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} {φ₁ φ₂ : M ⟶ N} : φ₁ = φ₂ ↔ φ₁.hom = φ₂.hom
• Action.hom_inv_hom_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} (f : M ≅ N) {Z : V} (h : M.V ⟶ Z) : CategoryTheory.CategoryStruct.comp f.hom.hom (CategoryTheory.CategoryStruct.comp f.inv.hom h) = h
• Action.inv_hom_hom_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} (f : M ≅ N) {Z : V} (h : N.V ⟶ Z) : CategoryTheory.CategoryStruct.comp f.inv.hom (CategoryTheory.CategoryStruct.comp f.hom.hom h) = h
• Action.comp_hom 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N K : Action V G} (f : M ⟶ N) (g : N ⟶ K) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
• 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.comp_hom_assoc 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N K : Action V G} (f : M ⟶ N) (g : N ⟶ K) {Z : V} (h : K.V ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
• 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.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.resId_hom_app_hom 📋 Mathlib.CategoryTheory.Action.Basic
  (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} [Monoid G] (X : Action V G) : ((Action.resId V).hom.app X).hom = CategoryTheory.CategoryStruct.id X.V
• Action.resId_inv_app_hom 📋 Mathlib.CategoryTheory.Action.Basic
  (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} [Monoid G] (X : Action V G) : ((Action.resId V).inv.app X).hom = CategoryTheory.CategoryStruct.id X.V
• 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.FunctorCategoryEquivalence.unitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (X : Action V G) : (Action.FunctorCategoryEquivalence.unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.V
• Action.FunctorCategoryEquivalence.unitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (X : Action V G) : (Action.FunctorCategoryEquivalence.unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.V
• 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
• CategoryTheory.Functor.mapActionCongr_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] (G : Type u_3) [Monoid G] {F F' : CategoryTheory.Functor V W} (e : F ≅ F') : (CategoryTheory.Functor.mapActionCongr G e).hom = { app := fun X => (Action.mkIso (e.app X.V) ⋯).hom, naturality := ⋯ }
• Action.resCongr_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 f' : G →* H} (h : f = f') : (Action.resCongr V h).hom = { app := fun X => (Action.mkIso (CategoryTheory.Iso.refl X.V) ⋯).hom, naturality := ⋯ }
• CategoryTheory.Functor.mapActionCongr_inv 📋 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] (G : Type u_3) [Monoid G] {F F' : CategoryTheory.Functor V W} (e : F ≅ F') : (CategoryTheory.Functor.mapActionCongr G e).inv = { app := fun X => (Action.mkIso (e.app X.V) ⋯).inv, naturality := ⋯ }
• Action.resComp_hom_app_hom 📋 Mathlib.CategoryTheory.Action.Basic
  (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} {K : Type u_5} [Monoid G] [Monoid H] [Monoid K] (f : G →* H) (g : H →* K) (X : Action V K) : ((Action.resComp V f g).hom.app X).hom = CategoryTheory.CategoryStruct.id X.V
• Action.resComp_inv_app_hom 📋 Mathlib.CategoryTheory.Action.Basic
  (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} {K : Type u_5} [Monoid G] [Monoid H] [Monoid K] (f : G →* H) (g : H →* K) (X : Action V K) : ((Action.resComp V f g).inv.app X).hom = CategoryTheory.CategoryStruct.id X.V
• Action.resCongr_inv 📋 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 f' : G →* H} (h : f = f') : (Action.resCongr V h).inv = { app := fun X => (Action.mkIso (CategoryTheory.Iso.refl X.V) ⋯).inv, naturality := ⋯ }
• 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
• Action.ofMulAction_V 📋 Mathlib.CategoryTheory.Action.Concrete
  (G : Type u_1) (H : Type u) [Monoid G] [MulAction G H] : (Action.ofMulAction G H).V = H
• Action.instMulActionObjFiniteVFintypeCat 📋 Mathlib.CategoryTheory.Action.Concrete
  {G : Type u_3} [Monoid G] (X : Action FintypeCat G) : MulAction G X.V.obj
• Action.instMulAction 📋 Mathlib.CategoryTheory.Action.Concrete
  {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {FV : V → V → Type u_1} {CV : V → Type u_2} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] {G : Type u_3} [Monoid G] (X : Action V G) : MulAction G (CategoryTheory.ToType X)
• 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.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.quotientToQuotientOfLE_hom_mk 📋 Mathlib.CategoryTheory.Action.Concrete
  {G : Type u_1} [Group G] (H N : Subgroup G) [Fintype (G ⧸ N)] [Fintype (G ⧸ H)] (h : N ≤ H) (x : G) : (CategoryTheory.ConcreteCategory.hom (Action.FintypeCat.quotientToQuotientOfLE H N h).hom) ⟦x⟧ = ⟦x⟧
• 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.instHasForget₂HomSubtypeVTopCatContinuousMapCarrier 📋 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] : CategoryTheory.HasForget₂ (Action V G) TopCat
• Action.instMulActionCarrierObjTopCatForget₂ContinuousMap 📋 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] (X : Action V G) : MulAction G ↑((CategoryTheory.forget₂ (Action V G) TopCat).obj X)
• ContAction.instHasForget₂HomSubtypeObjActionIsContinuousV 📋 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] : CategoryTheory.HasForget₂ (ContAction V G) V
• ContAction.instHasForget₂HomSubtypeObjActionIsContinuousVTopCatContinuousMapCarrier 📋 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] : CategoryTheory.HasForget₂ (ContAction V G) TopCat
• instConcreteCategoryDiscreteContActionHomSubtypeObjActionIsContinuousContActionIsDiscreteV 📋 Mathlib.CategoryTheory.Action.Continuous
  (V : Type u_3) [CategoryTheory.Category.{u_2, u_3} V] {FV : V → V → Type u_5} {CV : V → Type u_1} [(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] : CategoryTheory.ConcreteCategory (DiscreteContAction V G) fun X Y => Action.HomSubtype V G X.obj.obj Y.obj.obj
• DiscreteContAction.instHasForget₂HomSubtypeObjActionIsContinuousContActionIsDiscreteVTopCatContinuousMapCarrier 📋 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] : CategoryTheory.HasForget₂ (DiscreteContAction V G) TopCat
• DiscreteContAction.instHasForget₂HomSubtypeObjActionIsContinuousContActionIsDiscreteV 📋 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] : CategoryTheory.HasForget₂ (DiscreteContAction V G) (ContAction V G)
• DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap 📋 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 : DiscreteContAction V G) : DiscreteTopology ↑((CategoryTheory.forget₂ (DiscreteContAction V G) TopCat).obj 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
• ContAction.resCongr_hom 📋 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] {H : Type u_5} [Monoid H] [TopologicalSpace H] (f f' : G →ₜ* H) (h : f = f') : (ContAction.resCongr V f f' h).hom = { app := fun X => CategoryTheory.ObjectProperty.homMk (Action.mkIso (CategoryTheory.Iso.refl X.obj.V) ⋯).hom, naturality := ⋯ }
• ContAction.resCongr_inv 📋 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] {H : Type u_5} [Monoid H] [TopologicalSpace H] (f f' : G →ₜ* H) (h : f = f') : (ContAction.resCongr V f f' h).inv = { app := fun X => CategoryTheory.ObjectProperty.homMk (Action.mkIso (CategoryTheory.Iso.refl X.obj.V) ⋯).inv, naturality := ⋯ }
• CategoryTheory.Functor.mapContActionCongr_hom 📋 Mathlib.CategoryTheory.Action.Continuous
  {V : Type u_5} {W : Type u_6} [CategoryTheory.Category.{v_2, u_5} V] {FV : V → V → Type u_7} {CV : V → Type u_8} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] [CategoryTheory.HasForget₂ V TopCat] [CategoryTheory.Category.{v_3, u_6} W] {FW : W → W → Type u_9} {CW : W → Type u_10} [(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] [CategoryTheory.ConcreteCategory W FW] [CategoryTheory.HasForget₂ W TopCat] (G : Type u_11) [Monoid G] [TopologicalSpace G] {F F' : CategoryTheory.Functor V W} (e : F ≅ F') (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) (H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous) : (CategoryTheory.Functor.mapContActionCongr G e H H').hom = { app := fun X => CategoryTheory.ObjectProperty.homMk (Action.mkIso (e.app X.obj.V) ⋯).hom, naturality := ⋯ }
• CategoryTheory.Functor.mapContActionCongr_inv 📋 Mathlib.CategoryTheory.Action.Continuous
  {V : Type u_5} {W : Type u_6} [CategoryTheory.Category.{v_2, u_5} V] {FV : V → V → Type u_7} {CV : V → Type u_8} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] [CategoryTheory.HasForget₂ V TopCat] [CategoryTheory.Category.{v_3, u_6} W] {FW : W → W → Type u_9} {CW : W → Type u_10} [(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] [CategoryTheory.ConcreteCategory W FW] [CategoryTheory.HasForget₂ W TopCat] (G : Type u_11) [Monoid G] [TopologicalSpace G] {F F' : CategoryTheory.Functor V W} (e : F ≅ F') (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) (H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous) : (CategoryTheory.Functor.mapContActionCongr G e H H').inv = { app := fun X => CategoryTheory.ObjectProperty.homMk (Action.mkIso (e.app X.obj.V) ⋯).inv, naturality := ⋯ }
• Action.forget₂_additive 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Preadditive V] {FV : V → V → Type u_3} {CV : V → Type u_4} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] : (CategoryTheory.forget₂ (Action V G) V).Additive
• Action.forget₂_preservesZeroMorphisms 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Limits.HasZeroMorphisms V] {FV : V → V → Type u_3} {CV : V → Type u_4} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] : (CategoryTheory.forget₂ (Action V G) V).PreservesZeroMorphisms
• Action.forget₂_linear 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Preadditive V] {R : Type u_3} [Semiring R] [CategoryTheory.Linear R V] {FV : V → V → Type u_4} {CV : V → Type u_5} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] : CategoryTheory.Functor.Linear R (CategoryTheory.forget₂ (Action V G) V)
• Action.zero_hom 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : Action V G} : Action.Hom.hom 0 = 0
• Action.sum_hom 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Preadditive V] {X Y : Action V G} {ι : Type u_3} (f : ι → (X ⟶ Y)) (s : Finset ι) : (s.sum f).hom = ∑ i ∈ s, (f i).hom
• Action.neg_hom 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Preadditive V] {X Y : Action V G} (f : X ⟶ Y) : (-f).hom = -f.hom
• Action.zsmul_hom 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Preadditive V] {X Y : Action V G} (n : ℤ) (f : X ⟶ Y) : (n • f).hom = n • f.hom
• Action.nsmul_hom 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Preadditive V] {X Y : Action V G} (n : ℕ) (f : X ⟶ Y) : (n • f).hom = n • f.hom
• Action.sub_hom 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Preadditive V] {X Y : Action V G} (f g : X ⟶ Y) : (f - g).hom = f.hom - g.hom
• Action.add_hom 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Preadditive V] {X Y : Action V G} (f g : X ⟶ Y) : (f + g).hom = f.hom + g.hom
• Action.smul_hom 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Preadditive V] {R : Type u_3} [Semiring R] [CategoryTheory.Linear R V] {X Y : Action V G} (r : R) (f : X ⟶ Y) : (r • f).hom = r • f.hom
• Action.tensorUnit_V 📋 Mathlib.CategoryTheory.Action.Monoidal
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.MonoidalCategory V] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V G)).V = CategoryTheory.MonoidalCategoryStruct.tensorUnit V
• Action.tensorObj_V 📋 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) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V = CategoryTheory.MonoidalCategoryStruct.tensorObj X.V Y.V
• Action.leftDual_v 📋 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] : (ᘁX).V = ᘁX.V
• Action.rightDual_v 📋 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] : Xᘁ.V = X.Vᘁ
• Action.leftRegularTensorIso 📋 Mathlib.CategoryTheory.Action.Monoidal
  (G : Type u) [Group G] (X : Action (Type u) G) : CategoryTheory.MonoidalCategoryStruct.tensorObj (Action.leftRegular G) X ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (Action.leftRegular G) (Action.trivial G X.V)
• CategoryTheory.Functor.mapAction_ε_hom 📋 Mathlib.CategoryTheory.Action.Monoidal
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {W : Type u_3} [CategoryTheory.Category.{v_2, u_3} W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] : (CategoryTheory.Functor.LaxMonoidal.ε (F.mapAction G)).hom = CategoryTheory.Functor.LaxMonoidal.ε F
• CategoryTheory.Functor.mapAction_η_hom 📋 Mathlib.CategoryTheory.Action.Monoidal
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {W : Type u_3} [CategoryTheory.Category.{v_2, u_3} W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.OplaxMonoidal] : (CategoryTheory.Functor.OplaxMonoidal.η (F.mapAction G)).hom = CategoryTheory.Functor.OplaxMonoidal.η F
• Action.β_hom_hom 📋 Mathlib.CategoryTheory.Action.Monoidal
  (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {X Y : Action V G} : (β_ X Y).hom.hom = (β_ X.V Y.V).hom
• Action.β_inv_hom 📋 Mathlib.CategoryTheory.Action.Monoidal
  (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {X Y : Action V G} : (β_ X Y).inv.hom = (β_ X.V Y.V).inv
• Action.diagonalSuccIsoTensorDiagonal_hom_hom 📋 Mathlib.CategoryTheory.Action.Monoidal
  (G : Type u) [Monoid G] (n : ℕ) : (Action.diagonalSuccIsoTensorDiagonal G n).hom.hom = (Fin.consEquiv fun a => G).symm.toIso.hom
• Action.diagonalSuccIsoTensorDiagonal_inv_hom 📋 Mathlib.CategoryTheory.Action.Monoidal
  (G : Type u) [Monoid G] (n : ℕ) : (Action.diagonalSuccIsoTensorDiagonal G n).inv.hom = (Fin.consEquiv fun a => G).symm.toIso.inv
• CategoryTheory.Functor.mapAction_δ_hom 📋 Mathlib.CategoryTheory.Action.Monoidal
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {W : Type u_3} [CategoryTheory.Category.{v_2, u_3} W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.OplaxMonoidal] (X Y : Action V G) : (CategoryTheory.Functor.OplaxMonoidal.δ (F.mapAction G) X Y).hom = CategoryTheory.Functor.OplaxMonoidal.δ F X.V Y.V
• CategoryTheory.Functor.mapAction_μ_hom 📋 Mathlib.CategoryTheory.Action.Monoidal
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {W : Type u_3} [CategoryTheory.Category.{v_2, u_3} W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (X Y : Action V G) : (CategoryTheory.Functor.LaxMonoidal.μ (F.mapAction G) X Y).hom = CategoryTheory.Functor.LaxMonoidal.μ F X.V Y.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.diagonalSuccIsoTensorTrivial_inv_hom_apply 📋 Mathlib.CategoryTheory.Action.Monoidal
  {G : Type u} [Group G] {n : ℕ} (g : G) (f : Fin n → G) : (CategoryTheory.ConcreteCategory.hom (Action.diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f
• Action.whiskerLeft_hom 📋 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 : Action V G) {Y₁ Y₂ : Action V G} (f : Y₁ ⟶ Y₂) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.V f.hom
• Action.whiskerRight_hom 📋 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₁ X₂ : Action V G} (f : X₁ ⟶ X₂) (Y : Action V G) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Y.V
• Action.diagonalSuccIsoTensorTrivial_hom_hom_apply 📋 Mathlib.CategoryTheory.Action.Monoidal
  {G : Type u} [Group G] {n : ℕ} (f : Fin (n + 1) → G) : (CategoryTheory.ConcreteCategory.hom (Action.diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)
• Action.tensorHom_hom 📋 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₁ X₂ Y₂ : Action V G} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom = CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
• Action.leftUnitor_hom_hom 📋 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 : Action V G) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.V).hom
• Action.leftUnitor_inv_hom 📋 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 : Action V G) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.V).inv
• Action.rightUnitor_hom_hom 📋 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 : Action V G) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.V).hom
• Action.rightUnitor_inv_hom 📋 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 : Action V G) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.V).inv
• 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
• Action.associator_hom_hom 📋 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 Z : Action V G) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom = (CategoryTheory.MonoidalCategoryStruct.associator X.V Y.V Z.V).hom
• Action.associator_inv_hom 📋 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 Z : Action V G) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom = (CategoryTheory.MonoidalCategoryStruct.associator X.V Y.V Z.V).inv
• CategoryTheory.FintypeCat.Action.pretransitive_of_isConnected 📋 Mathlib.CategoryTheory.Galois.Examples
  (G : Type u) [Group G] (X : Action FintypeCat G) [CategoryTheory.PreGaloisCategory.IsConnected X] : MulAction.IsPretransitive G X.V.obj
• CategoryTheory.FintypeCat.Action.isConnected_iff_transitive 📋 Mathlib.CategoryTheory.Galois.Examples
  (G : Type u) [Group G] (X : Action FintypeCat G) [Nonempty X.V.obj] : CategoryTheory.PreGaloisCategory.IsConnected X ↔ MulAction.IsPretransitive G X.V.obj
• CategoryTheory.FintypeCat.isoQuotientStabilizerOfIsConnected 📋 Mathlib.CategoryTheory.Galois.Examples
  {G : Type u} [Group G] (X : Action FintypeCat G) [CategoryTheory.PreGaloisCategory.IsConnected X] (x : X.V.obj) [Fintype (G ⧸ MulAction.stabilizer G x)] : X ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))
• CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeFunObjFiniteV 📋 Mathlib.CategoryTheory.Galois.Examples
  (G : Type u) [Group G] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget (Action FintypeCat G))
• CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeFunObjFiniteV 📋 Mathlib.CategoryTheory.Galois.Examples
  (G : Type u) [Group G] : CategoryTheory.PreGaloisCategory.FiberFunctor (CategoryTheory.forget₂ (Action FintypeCat G) FintypeCat)
• CategoryTheory.PreGaloisCategory.instMulActionAutObjFiniteVFintypeCatFunctorObjActionFunctorToAction 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) : MulAction (CategoryTheory.Aut X) ((CategoryTheory.PreGaloisCategory.functorToAction F).obj X).V.obj
• CategoryTheory.PreGaloisCategory.instIsPretransitiveAutObjFiniteVFintypeCatFunctorObjActionFunctorToActionOfIsGalois 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X] : MulAction.IsPretransitive (CategoryTheory.Aut X) ((CategoryTheory.PreGaloisCategory.functorToAction F).obj X).V.obj
• CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) : (CategoryTheory.PreGaloisCategory.functorToAction F).comp (CategoryTheory.forget₂ (Action FintypeCat (CategoryTheory.Aut F)) FintypeCat) = F
• CategoryTheory.PreGaloisCategory.functorToAction_map 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) {X Y : C} (f : X ⟶ Y) : ((CategoryTheory.PreGaloisCategory.functorToAction F).map f).hom = F.map f
• CategoryTheory.PreGaloisCategory.has_decomp_quotients 📋 Mathlib.CategoryTheory.Galois.EssSurj
  {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (X : Action FintypeCat G) [TopologicalSpace X.V.obj] [DiscreteTopology X.V.obj] [ContinuousSMul G X.V.obj] : ∃ ι, ∃ (x : Finite ι), ∃ f, Nonempty ((∐ fun i => Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ X)
• CategoryTheory.PreGaloisCategory.exists_lift_of_continuous 📋 Mathlib.CategoryTheory.Galois.EssSurj
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : Action FintypeCat (CategoryTheory.Aut F)) [TopologicalSpace X.V.obj] [DiscreteTopology X.V.obj] [ContinuousSMul (CategoryTheory.Aut F) X.V.obj] : ∃ A, Nonempty ((CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅ X)
• Representation.linearize 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] (X : Action (Type w) G) : Representation k G (MonoidAlgebra k X.V)
• Representation.linearizeDiagonalEquiv 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] (n : ℕ) : (Representation.linearize k G (Action.diagonal G n)).Equiv (Representation.diagonal k G n)
• Representation.linearizeOfMulActionIso 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] (H : Type w) [MulAction G H] : (Representation.linearize k G (Action.ofMulAction G H)).Equiv (Representation.ofMulAction k G H)
• Representation.linearizeTrivialIso 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] (X : Type w) : (Representation.linearize k G (Action.trivial G X)).Equiv (Representation.trivial k G (MonoidAlgebra k X))
• Representation.linearizeMap 📋 Mathlib.RepresentationTheory.Action
  {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X Y : Action (Type w) G} (f : X ⟶ Y) : (Representation.linearize k G X).IntertwiningMap (Representation.linearize k G Y)
• Representation.LinearizeMonoidal.ε 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (Representation.trivial k G k).IntertwiningMap (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type w) G)))
• Representation.LinearizeMonoidal.η 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G))).IntertwiningMap (Representation.trivial k G k)
• Representation.LinearizeMonoidal.η_toLinearMap 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (Representation.LinearizeMonoidal.η k G).toLinearMap = ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{u + 1})
• Representation.LinearizeMonoidal.η_ε 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (Representation.LinearizeMonoidal.η k G).comp (Representation.LinearizeMonoidal.ε k G) = Representation.IntertwiningMap.id (Representation.trivial k G k)
• Representation.linearizeMap_toLinearMap 📋 Mathlib.RepresentationTheory.Action
  {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X Y : Action (Type w) G} (f : X ⟶ Y) : (Representation.linearizeMap f).toLinearMap = MonoidAlgebra.mapDomainLinearMap k k ⇑(CategoryTheory.ConcreteCategory.hom f.hom)
• Representation.LinearizeMonoidal.ε_toLinearMap 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (Representation.LinearizeMonoidal.ε k G).toLinearMap = ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{w + 1}).symm
• Representation.linearizeMap_single 📋 Mathlib.RepresentationTheory.Action
  {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X Y : Action (Type w) G} (f : X ⟶ Y) (x : X.V) (r : k) : (Representation.linearizeMap f) (MonoidAlgebra.single x r) = MonoidAlgebra.single ((CategoryTheory.ConcreteCategory.hom f.hom) x) r
• Representation.linearizeTrivialIso_apply 📋 Mathlib.RepresentationTheory.Action
  {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X : Type w} (f : MonoidAlgebra k (Action.trivial G X).V) : (Representation.linearizeTrivialIso k G X) f = f
• Representation.linearizeTrivialIso_symm_apply 📋 Mathlib.RepresentationTheory.Action
  {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X : Type w} (f : MonoidAlgebra k X) : (Representation.linearizeTrivialIso k G X).symm f = f
• Representation.LinearizeMonoidal.ε_one 📋 Mathlib.RepresentationTheory.Action
  {k : Type u} {G : Type v} [Monoid G] [Semiring k] : (Representation.LinearizeMonoidal.ε k G) 1 = MonoidAlgebra.single PUnit.unit 1
• Representation.LinearizeMonoidal.η_single 📋 Mathlib.RepresentationTheory.Action
  {k : Type u} {G : Type v} [Monoid G] [Semiring k] (x : PUnit.{u + 1}) : (Representation.LinearizeMonoidal.η k G) (MonoidAlgebra.single x 1) = 1
• Representation.LinearizeMonoidal.δ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).IntertwiningMap ((Representation.linearize k G X).tprod (Representation.linearize k G Y))
• Representation.LinearizeMonoidal.μ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : ((Representation.linearize k G X).tprod (Representation.linearize k G Y)).IntertwiningMap (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
• Representation.linearizeTrivial_def 📋 Mathlib.RepresentationTheory.Action
  {k : Type u} {G : Type v} [Monoid G] [Semiring k] (X : Type w) (g : G) : (Representation.linearize k G (Action.trivial G X)) g = LinearMap.id
• Representation.LinearizeMonoidal.ε_η 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (Representation.LinearizeMonoidal.ε k G).comp (Representation.LinearizeMonoidal.η k G) = Representation.IntertwiningMap.id (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G)))
• Representation.linearize_single 📋 Mathlib.RepresentationTheory.Action
  {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X : Action (Type w) G} (g : G) (x : X.V) : ((Representation.linearize k G X) g) (MonoidAlgebra.single x 1) = MonoidAlgebra.single ((CategoryTheory.ConcreteCategory.hom (X.ρ g)) x) 1
• Representation.linearize_apply 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] (X : Action (Type w) G) (g : G) : (Representation.linearize k G X) g = MonoidAlgebra.mapDomainLinearMap k k ⇑(CategoryTheory.ConcreteCategory.hom (X.ρ g))
• Representation.LinearizeMonoidal.μ_toLinearMap 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : (Representation.LinearizeMonoidal.μ X Y).toLinearMap = ↑(MonoidAlgebra.tensorEquiv k)
• Representation.LinearizeMonoidal.μ_δ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : (Representation.LinearizeMonoidal.μ X Y).comp (Representation.LinearizeMonoidal.δ X Y) = Representation.IntertwiningMap.id (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
• Action.tensor_ρ_apply 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} (g : G) (xy : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ρ g)) xy = ((CategoryTheory.ConcreteCategory.hom (X.ρ g)) xy.1, (CategoryTheory.ConcreteCategory.hom (Y.ρ g)) xy.2)
• Representation.LinearizeMonoidal.μ_apply_single_single 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (x : X.V) (y : Y.V) (r s : k) : (Representation.LinearizeMonoidal.μ X Y) (MonoidAlgebra.single x r ⊗ₜ[k] MonoidAlgebra.single y s) = MonoidAlgebra.single (x, y) (r * s)
• Representation.LinearizeMonoidal.δ_apply_single 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (xy : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V) : (Representation.LinearizeMonoidal.δ X Y) (MonoidAlgebra.single xy 1) = MonoidAlgebra.single xy.1 1 ⊗ₜ[k] MonoidAlgebra.single xy.2 1
• Representation.LinearizeMonoidal.coeff_μ_tmul 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (l1 : MonoidAlgebra k X.V) (l2 : MonoidAlgebra k Y.V) (xy : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V) : ((Representation.LinearizeMonoidal.μ X Y) (l1 ⊗ₜ[k] l2)).coeff xy = l1.coeff xy.1 * l2.coeff xy.2
• Representation.LinearizeMonoidal.δ_μ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : (Representation.LinearizeMonoidal.δ X Y).comp (Representation.LinearizeMonoidal.μ X Y) = Representation.IntertwiningMap.id ((Representation.linearize k G X).tprod (Representation.linearize k G Y))
• Representation.LinearizeMonoidal.lTensor_comp_δ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} (Z : Action (Type w) G) {k : Type u} [CommSemiring k] (f : X ⟶ Y) : (Representation.IntertwiningMap.lTensor (Representation.linearize k G Z) (Representation.linearizeMap f)).comp (Representation.LinearizeMonoidal.δ Z X) = (Representation.LinearizeMonoidal.δ Z Y).comp (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f))
• Representation.LinearizeMonoidal.rTensor_comp_δ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} (Z : Action (Type w) G) {k : Type u} [CommSemiring k] (f : X ⟶ Y) : (Representation.IntertwiningMap.rTensor (Representation.linearize k G Z) (Representation.linearizeMap f)).comp (Representation.LinearizeMonoidal.δ X Z) = (Representation.LinearizeMonoidal.δ Y Z).comp (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z))
• Representation.LinearizeMonoidal.μ_comp_lTensor 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (f : X ⟶ Y) (Z : Action (Type w) G) : (Representation.LinearizeMonoidal.μ Z Y).comp (Representation.IntertwiningMap.lTensor (Representation.linearize k G Z) (Representation.linearizeMap f)) = (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)).comp (Representation.LinearizeMonoidal.μ Z X)
• Representation.LinearizeMonoidal.μ_comp_rTensor 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (f : X ⟶ Y) (Z : Action (Type w) G) : (Representation.LinearizeMonoidal.μ Y Z).comp (Representation.IntertwiningMap.rTensor (Representation.linearize k G Z) (Representation.linearizeMap f)) = (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)).comp (Representation.LinearizeMonoidal.μ X Z)
• Representation.LinearizeMonoidal.μ_leftUnitor 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X : Action (Type w) G) {k : Type u} [CommSemiring k] : ↑(Representation.TensorProduct.lid k (Representation.linearize k G X)) = ((Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom).comp (Representation.LinearizeMonoidal.μ (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type w) G)) X)).comp (Representation.IntertwiningMap.rTensor (Representation.linearize k G X) (Representation.LinearizeMonoidal.ε k G))
• Representation.LinearizeMonoidal.μ_rightUnitor 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X : Action (Type w) G) {k : Type u} [CommSemiring k] : ↑(Representation.TensorProduct.rid k (Representation.linearize k G X)) = ((Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom).comp (Representation.LinearizeMonoidal.μ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type w) G)))).comp (Representation.IntertwiningMap.lTensor (Representation.linearize k G X) (Representation.LinearizeMonoidal.ε k G))
• Representation.LinearizeMonoidal.leftUnitor_δ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {k : Type u} [CommSemiring k] (X : Action (Type u) G) : ↑(Representation.TensorProduct.lid k (Representation.linearize k G X)).symm = ((Representation.IntertwiningMap.rTensor (Representation.linearize k G X) (Representation.LinearizeMonoidal.η k G)).comp (Representation.LinearizeMonoidal.δ (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G)) X)).comp (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv)
• Representation.LinearizeMonoidal.rightUnitor_δ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {k : Type u} [CommSemiring k] (X : Action (Type u) G) : ↑(Representation.TensorProduct.rid k (Representation.linearize k G X)).symm = ((Representation.IntertwiningMap.lTensor (Representation.linearize k G X) (Representation.LinearizeMonoidal.η k G)).comp (Representation.LinearizeMonoidal.δ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G)))).comp (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv)
• Representation.LinearizeMonoidal.μ_comp_assoc 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X Y Z : Action (Type w) G) {k : Type u} [CommSemiring k] : ((Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom).comp (Representation.LinearizeMonoidal.μ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)).comp (Representation.IntertwiningMap.rTensor (Representation.linearize k G Z) (Representation.LinearizeMonoidal.μ X Y)) = ((Representation.LinearizeMonoidal.μ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).comp (Representation.IntertwiningMap.lTensor (Representation.linearize k G X) (Representation.LinearizeMonoidal.μ Y Z))).comp ↑(Representation.TensorProduct.assoc (Representation.linearize k G X) (Representation.linearize k G Y) (Representation.linearize k G Z))
• Representation.LinearizeMonoidal.assoc_comp_δ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X Y Z : Action (Type w) G) {k : Type u} [CommSemiring k] : ((↑(Representation.TensorProduct.assoc (Representation.linearize k G X) (Representation.linearize k G Y) (Representation.linearize k G Z))).comp (Representation.IntertwiningMap.rTensor (Representation.linearize k G Z) (Representation.LinearizeMonoidal.δ X Y))).comp (Representation.LinearizeMonoidal.δ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) = ((Representation.IntertwiningMap.lTensor (Representation.linearize k G X) (Representation.LinearizeMonoidal.δ Y Z)).comp (Representation.LinearizeMonoidal.δ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))).comp (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
• Rep.linearization_obj_V 📋 Mathlib.RepresentationTheory.Rep.Basic
  (k : Type u) (G : Type v) [CommRing k] [Monoid G] (X : Action (Type w) G) : ↑((Rep.linearization k G).obj X) = MonoidAlgebra k X.V
• Rep.RepToAction_obj_V_carrier 📋 Mathlib.RepresentationTheory.Rep.Basic
  (k : Type u) (G : Type v) [Ring k] [Monoid G] (X : Rep.{w, u, v} k G) : ↑((Rep.RepToAction k G).obj X).V = ↑X
• Rep.ActionToRep_obj_V 📋 Mathlib.RepresentationTheory.Rep.Basic
  (k : Type u) (G : Type v) [Ring k] [Monoid G] (X : Action (ModuleCat k) G) : ↑((Rep.ActionToRep k G).obj X) = ↑X.V
• Rep.linearization_obj_ρ 📋 Mathlib.RepresentationTheory.Rep.Basic
  (k : Type u) (G : Type v) [CommRing k] [Monoid G] (X : Action (Type w) G) : ((Rep.linearization k G).obj X).ρ = Representation.linearize k G X
• Rep.linearization_map 📋 Mathlib.RepresentationTheory.Rep.Basic
  (k : Type u) (G : Type v) [CommRing k] [Monoid G] {X✝ Y✝ : Action (Type w) G} (f : X✝ ⟶ Y✝) : (Rep.linearization k G).map f = Rep.ofHom (Representation.linearizeMap f)
• Rep.ε_def 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.Functor.LaxMonoidal.ε (Rep.linearization k G) = Rep.ofHom (Representation.LinearizeMonoidal.ε k G)
• Rep.η_def 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.Functor.OplaxMonoidal.η (Rep.linearization k G) = Rep.ofHom (Representation.LinearizeMonoidal.η k G)
• Rep.ActionToRep_obj_ρ 📋 Mathlib.RepresentationTheory.Rep.Basic
  (k : Type u) (G : Type v) [Ring k] [Monoid G] (X : Action (ModuleCat k) G) : ((Rep.ActionToRep k G).obj X).ρ = X.V.endRingEquiv.toMonoidHom.comp X.ρ
• Rep.δ_def 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Action (Type u) G} : CategoryTheory.Functor.OplaxMonoidal.δ (Rep.linearization k G) X Y = Rep.ofHom (Representation.LinearizeMonoidal.δ X Y)
• Rep.μ_def 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Action (Type u) G} : CategoryTheory.Functor.LaxMonoidal.μ (Rep.linearization k G) X Y = Rep.ofHom (Representation.LinearizeMonoidal.μ X Y)
• Rep.ActionToRep_map 📋 Mathlib.RepresentationTheory.Rep.Basic
  (k : Type u) (G : Type v) [Ring k] [Monoid G] {X✝ Y✝ : Action (ModuleCat k) G} (f : X✝ ⟶ Y✝) : (Rep.ActionToRep k G).map f = Rep.ofHom { toLinearMap := ModuleCat.Hom.hom f.hom, isIntertwining' := ⋯ }
• FDRep.isoToLinearEquiv 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] {V W : FDRep R G} (i : V ≅ W) : ↑V.V ≃ₗ[R] ↑W.V
• FDRep.ρ 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] (V : FDRep R G) : G →* ↑V.V →ₗ[R] ↑V.V
• FDRep.of_ρ' 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] {V : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] (ρ : G →* V →ₗ[R] V) : (FDRep.of ρ).ρ = ρ
• FDRep.instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRepIntertwiningMapVρ 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] : CategoryTheory.HasForget₂ (FDRep R G) (Rep.{u, u, v} R G)
• FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] : (CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G)).Faithful
• FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] : (CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G)).Full
• FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G))
• FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] [IsNoetherianRing R] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G))
• FDRep.dualTensorIsoLinHom 📋 Mathlib.RepresentationTheory.FDRep
  {k : Type u} {G : Type v} {V : Type u} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρV : Representation k G V) (W : FDRep k G) : CategoryTheory.MonoidalCategoryStruct.tensorObj (FDRep.of ρV.dual) W ≅ FDRep.of (ρV.linHom W.ρ)
• FDRep.dualTensorIsoLinHomAux 📋 Mathlib.RepresentationTheory.FDRep
  {k : Type u} {G : Type v} {V : Type u} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρV : Representation k G V) (W : FDRep k G) : (CategoryTheory.MonoidalCategoryStruct.tensorObj (FDRep.of ρV.dual) W).V ≅ (FDRep.of (ρV.linHom W.ρ)).V
• FDRep.hom_hom_action_ρ 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] (V : FDRep R G) (g : G) : ModuleCat.Hom.hom (V.ρ g).hom = V.ρ g
• FDRep.dualTensorIsoLinHom_hom_hom 📋 Mathlib.RepresentationTheory.FDRep
  {k : Type u} {G : Type v} {V : Type u} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρV : Representation k G V) (W : FDRep k G) : (FDRep.dualTensorIsoLinHom ρV W).hom.hom = CategoryTheory.ConcreteCategory.ofHom (dualTensorHom k V ↑W.V)
• FDRep.forget₂_ρ 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] (V : FDRep R G) : ((CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G)).obj V).ρ = V.ρ
• FDRep.Iso.conj_ρ 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] {V W : FDRep R G} (i : V ≅ W) (g : G) : W.ρ g = (FDRep.isoToLinearEquiv i).conj (V.ρ g)
• FDRep.forget₂HomLinearEquiv 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] (X Y : FDRep R G) : ((CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G)).obj X ⟶ (CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G)).obj Y) ≃ₗ[R] X ⟶ Y
• FDRep.endRingEquiv_symm_comp_ρ 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] (V : FDRep R G) : (↑V.V.obj.endRingEquiv.symm).comp V.ρ = CategoryTheory.InducedCategory.endEquiv.toMonoidHom.comp V.ρ
• FDRep.endRingEquiv_comp_ρ 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] (V : FDRep R G) : (↑V.V.obj.endRingEquiv).comp (CategoryTheory.InducedCategory.endEquiv.toMonoidHom.comp V.ρ) = V.ρ
• Representation.linHom.invariantsEquivFDRepHom 📋 Mathlib.RepresentationTheory.Invariants
  {k : Type u} [Field k] {G : Type v} [Group G] (X Y : FDRep k G) : ↥(Representation.linHom X.ρ Y.ρ).invariants ≃ₗ[k] X ⟶ Y

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 69fae59