class CategoryTheory.NonzeroModuleCategory (M : Type u₂) [Category.{v₂, u₂} M] : Prop

The module category M is nonzero: it contains some object that is not initial.

• exists_nonzero : ∃ (X : M), IsEmpty (Limits.IsInitial X)

structure CategoryTheory.InternalHomExactInSecondVar (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] : Type (max (max (max u₁ u₂) v₁) v₂)

Data witnessing the internal-Hom adjunction Hom(X ⊗ m, n) ≃ Hom(X, iHom m n) together with the second-variable exactness assumption that iHom m - preserves both monos and epis.

• iHom : M → M → C
• iHomEquiv (X : C) (m n : M) : (LeftModuleCategoryStruct.actObj X m ⟶ n) ≃ (X ⟶ self.iHom m n)
• iHomMap (m : M) {n₁ n₂ : M} : (n₁ ⟶ n₂) → (self.iHom m n₁ ⟶ self.iHom m n₂)
• preserves_mono (m : M) {n₁ n₂ : M} (f : n₁ ⟶ n₂) : Mono f → Mono (self.iHomMap m f)
• preserves_epi (m : M) {n₁ n₂ : M} (f : n₁ ⟶ n₂) : Epi f → Epi (self.iHomMap m f)
• iHomEquiv_natural (X : C) (m : M) {n₁ n₂ : M} (g : LeftModuleCategoryStruct.actObj X m ⟶ n₁) (f : n₁ ⟶ n₂) : (self.iHomEquiv X m n₂) (CategoryStruct.comp g f) = CategoryStruct.comp ((self.iHomEquiv X m n₁) g) (self.iHomMap m f)

@[reducible]

def CategoryTheory.prop_2_10_7_hom_exact_implies_exact {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : Type u₂} [Category.{v₂, u₂} M] [LeftModuleCategory C M] (h : InternalHomExactInSecondVar C M) : ExactModuleCategory C M

Proposition 2.10.7(1): If the internal Hom Hom(N, -) : M → C is exact in the second variable, then the module category M over C is exact.

structure CategoryTheory.ModuleInternalHomData (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] : Type (max (max (max u₁ u₂) v₁) v₂)

The internal-Hom data of a left C-module category M without any exactness conditions: the adjunction Hom(X ⊗ m, n) ≃ Hom(X, iHom m n) along with naturality.

• iHom : M → M → C
• iHomEquiv (X : C) (m n : M) : (LeftModuleCategoryStruct.actObj X m ⟶ n) ≃ (X ⟶ self.iHom m n)
• iHomMap (m : M) {n₁ n₂ : M} : (n₁ ⟶ n₂) → (self.iHom m n₁ ⟶ self.iHom m n₂)
• iHomEquiv_natural (X : C) (m : M) {n₁ n₂ : M} (g : LeftModuleCategoryStruct.actObj X m ⟶ n₁) (f : n₁ ⟶ n₂) : (self.iHomEquiv X m n₂) (CategoryStruct.comp g f) = CategoryStruct.comp ((self.iHomEquiv X m n₁) g) (self.iHomMap m f)

noncomputable def CategoryTheory.moduleInternalHomData_exists (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] : ModuleInternalHomData C M

Existence of internal-Hom data for any left C-module category M.

theorem CategoryTheory.iHomMap_exact_of_allFunctorsExact {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M₁ : Type u₂} [Category.{v₂, u₂} M₁] [LeftModuleCategory C M₁] {M₂ : Type u₃} [Category.{v₃, u₃} M₂] [LeftModuleCategory C M₂] [NonzeroModuleCategory M₂] (h : ∀ (F : ModuleFunctor C M₁ M₂), ModuleFunctorIsExact F) (d : ModuleInternalHomData C M₁) (m : M₁) : (∀ {n₁ n₂ : M₁} (f : n₁ ⟶ n₂), Mono f → Mono (d.iHomMap m f)) ∧ ∀ {n₁ n₂ : M₁} (f : n₁ ⟶ n₂), Epi f → Epi (d.iHomMap m f)

If every module functor M₁ → M₂ (for some nonzero target) is exact, then for every object m ∈ M₁ the internal-Hom functor iHom m - preserves both monos and epis.

noncomputable def CategoryTheory.internalHomExactInSecondVar_of_allFunctorsExact {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M₁ : Type u₂} [Category.{v₂, u₂} M₁] [LeftModuleCategory C M₁] {M₂ : Type u₃} [Category.{v₃, u₃} M₂] [LeftModuleCategory C M₂] [NonzeroModuleCategory M₂] (h : ∀ (F : ModuleFunctor C M₁ M₂), ModuleFunctorIsExact F) : InternalHomExactInSecondVar C M₁

Builds internal-Hom data exact in the second variable assuming all module functors out of M₁ are exact.

@[reducible]

noncomputable def CategoryTheory.prop_2_10_7_all_functors_exact_implies_exact {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M₁ : Type u₂} [Category.{v₂, u₂} M₁] [LeftModuleCategory C M₁] {M₂ : Type u₃} [Category.{v₃, u₃} M₂] [LeftModuleCategory C M₂] [NonzeroModuleCategory M₂] (h : ∀ (F : ModuleFunctor C M₁ M₂), ModuleFunctorIsExact F) : ExactModuleCategory C M₁

Proposition 2.10.7(2): If every module functor from M₁ to some nonzero M₂ is exact, then M₁ is an exact module category over C.

@[reducible, inline]

abbrev CategoryTheory.proposition_2_10_7_part1 {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : Type u₂} [Category.{v₂, u₂} M] [LeftModuleCategory C M] (h : InternalHomExactInSecondVar C M) : ExactModuleCategory C M

Restatement of Proposition 2.10.7(1) as an alias of prop_2_10_7_hom_exact_implies_exact.

@[reducible]

noncomputable def CategoryTheory.proposition_2_10_7_part2 {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M₁ : Type u₂} [Category.{v₂, u₂} M₁] [LeftModuleCategory C M₁] {M₂ : Type u₃} [Category.{v₃, u₃} M₂] [LeftModuleCategory C M₂] [NonzeroModuleCategory M₂] (h : ∀ (F : ModuleFunctor C M₁ M₂), ModuleFunctorIsExact F) : ExactModuleCategory C M₁

Restatement of Proposition 2.10.7(2) as an alias of prop_2_10_7_all_functors_exact_implies_exact.

@[reducible]

noncomputable def CategoryTheory.proposition_2_10_7 {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : Type u₂} [Category.{v₂, u₂} M] [LeftModuleCategory C M] (h : InternalHomExactInSecondVar C M) : ExactModuleCategory C M

Proposition 2.10.7: combined statement, defaulting to the first part.