A left module category M over C has internal Hom if for every pair m, n ∈ M
there is an object moduleIHom m n ∈ C and a natural equivalence
(X ⊗ᵐ m ⟶ n) ≃ (X ⟶ moduleIHom m n) (Definition 2.10.2).
- moduleIHom : M → M → C
- moduleIHomEquiv (X : C) (m n : M) : (LeftModuleCategoryStruct.actObj X m ⟶ n) ≃ (X ⟶ moduleIHom m n)
- moduleIHomEquiv_natural {X Y : C} (f : X ⟶ Y) (m n : M) (g : LeftModuleCategoryStruct.actObj Y m ⟶ n) : (moduleIHomEquiv X m n) (CategoryStruct.comp (LeftModuleCategoryStruct.actWhiskerRight f m) g) = CategoryStruct.comp f ((moduleIHomEquiv Y m n) g)
Instances
Convenience abbreviation for moduleIHom m₁ m₂, the internal Hom in C of the
module objects m₁, m₂ : M.
Instances For
Definition 2.10.2: the internal Hom Hom(m₁, m₂) in C of two module objects of
the module category M.
Instances For
The evaluation morphism moduleIHom m n ⊗ᵐ m ⟶ n, obtained as the counit of the
internal Hom adjunction by transporting the identity of moduleIHom m n.
Instances For
The inverse of moduleIHomEquiv is given by whiskering by m and post-composing
with the evaluation morphism.
The composition morphism Hom(n, p) ⊗ Hom(m, n) ⟶ Hom(m, p) of internal Homs,
defined via the action associator and the evaluation morphisms.
Instances For
Right whiskering of a composition of morphisms in C by a module object equals the
composition of right whiskerings.
Right whiskering of a composition of morphisms in C by a module object equals the
composition of right whiskerings.
Left whiskering of a composition of module morphisms by an object of C equals the
composition of left whiskerings.
Left whiskering of a composition of module morphisms by an object of C equals the
composition of left whiskerings.
Interchange law for the module action: right whiskering by M₁ followed by left
whiskering by X₂ equals left whiskering by X₁ followed by right whiskering by M₂.
Interchange law for the module action: right whiskering by M₁ followed by left
whiskering by X₂ equals left whiskering by X₁ followed by right whiskering by M₂.
The internal Hom adjunction equivalence
(X ⊗ᵐ m ⟶ n) ≃ (X ⟶ moduleIHom m n), packaged as a standalone definition.
Instances For
The natural isomorphism Hom(𝟙_ C ⊗ᵐ m, n) ≅ Hom(m, n) coming from the unit
isomorphism actℓ_ m : 𝟙_ C ⊗ᵐ m ≅ m.
Instances For
Curry equivalence: (T ⊗ X ⟶ Hom(m, n)) ≃ (T ⟶ Hom(X ⊗ᵐ m, n)), obtained by
combining the internal Hom adjunction with the action associator.
Instances For
Tensor equivalence: (Y ⟶ Hom(X ⊗ᵐ m, n)) ≃ (Y ⟶ Hom(m, n) ⊗ Xᘁ) when X has a
right dual, obtained from moduleIHom_curry_equiv and tensorRightHomEquiv.
Instances For
Naturality in T of the inverse curry equivalence:
(curry^{-1} _ _ m n) (f ≫ g) = f ▷ X ≫ (curry^{-1} _ _ m n) g.
Naturality in Y of moduleIHom_tensor_equiv:
tensor_equiv (f ≫ g) = f ≫ tensor_equiv g.
The natural isomorphism Hom(X ⊗ᵐ m, n) ≅ Hom(m, n) ⊗ Xᘁ produced from
moduleIHom_tensor_equiv (Lemma 2.10.4 part 3).
Instances For
Left inverse condition for modTensorHomEquiv: applying the unit-evaluation pair
recovers the original morphism f : N ⟶ X ⊗ᵐ P.
Right inverse condition for modTensorHomEquiv: applying the inverse direction
recovers the original morphism g : Xᘁ ⊗ᵐ N ⟶ P.
The module-level duality equivalence (N ⟶ X ⊗ᵐ P) ≃ (Xᘁ ⊗ᵐ N ⟶ P) arising from
the rigidity of C together with the left module structure on M.
Instances For
Naturality of modTensorHomEquiv in the source module object:
(f ≫ g)^∨ = Xᘁ ◁ᵐ f ≫ g^∨.
Equivalence (Y ⟶ Hom(m₁, X ⊗ᵐ m₂)) ≃ (Y ⟶ X ⊗ Hom(m₁, m₂)), built from the
internal Hom adjunction, the module duality equivalence, and the action associator.
Instances For
Naturality in Y of moduleIHom_tensor_left_equiv:
tensor_left_equiv (f ≫ g) = f ≫ tensor_left_equiv g.
The natural isomorphism Hom(m₁, X ⊗ᵐ m₂) ≅ X ⊗ Hom(m₁, m₂) (Lemma 2.10.4 part 4).
Instances For
Global sections equivalence (m₁ ⟶ X ⊗ᵐ m₂) ≃ (𝟙_ C ⟶ X ⊗ Hom(m₁, m₂)),
underlying Lemma 2.10.4 part 2.
Instances For
Lemma 2.10.4 part 1: the internal Hom adjunction
(X ⊗ᵐ m ⟶ n) ≃ (X ⟶ Hom(m, n)).
Instances For
Lemma 2.10.4 part 2: when X is rigid, morphisms m₁ ⟶ X ⊗ᵐ m₂ correspond to
global sections of X ⊗ Hom(m₁, m₂).
Instances For
Lemma 2.10.4 part 3: when X is rigid, Hom(X ⊗ᵐ m, n) ≅ Hom(m, n) ⊗ Xᘁ.
Instances For
Lemma 2.10.4 part 4: when X is rigid, Hom(m₁, X ⊗ᵐ m₂) ≅ X ⊗ Hom(m₁, m₂).
Instances For
Lemma 2.10.4 (combined): the four natural equivalences/isomorphisms for the internal
Hom with a rigid object X, packaged as a single product.
Instances For
Functorial action of moduleIHom on a morphism in the right argument:
Hom(m₁, m₂) ⟶ Hom(m₁, m₂') induced by f : m₂ ⟶ m₂'.
Instances For
Contravariant functorial action of moduleIHom in the left argument:
Hom(m₁', m₂) ⟶ Hom(m₁, m₂) induced by f : m₁ ⟶ m₁'.
Instances For
Naturality of moduleIHomEquiv in the right (target) module argument:
moduleIHomEquiv X m₁ m₂' (h ≫ g) = moduleIHomEquiv X m₁ m₂ h ≫ moduleIHomMapRight m₁ g.
Naturality of moduleIHom_tensor_left_equiv in the right module argument m₂:
post-composition with Hom(m₁, X ◁ᵐ f) corresponds to post-composition with
X ◁ Hom(m₁, f).
Naturality of moduleIHom_tensor_left_equiv in the rigid object X:
post-composition with Hom(m₁, f ▷ᵐ m₂) corresponds to post-composition with f ▷ Hom(m₁, m₂).
If f : m₂ ⟶ m₂' is a monomorphism, then moduleIHomMapRight m₁ f is also a
monomorphism, using the internal Hom adjunction.
In an exact module category, if f : m₂ ⟶ m₂' is an epimorphism, then
moduleIHomMapRight m₁ f is also an epimorphism (Corollary 2.10.6, exactness in m₂).
In an exact module category, a monomorphism f : m₁ ⟶ m₁' induces an epimorphism
moduleIHomMapLeft f m₂ (Corollary 2.10.6, mono-to-epi exactness in m₁).
In an exact module category, an epimorphism f : m₁ ⟶ m₁' induces a monomorphism
moduleIHomMapLeft f m₂ (Corollary 2.10.6, epi-to-mono exactness in m₁).
Combined statement of Corollary 2.10.6 collecting the four exactness properties of
the internal Hom functors moduleIHomMapRight and moduleIHomMapLeft in an exact module
category.
Corollary 2.10.6: in an exact module category, the internal Hom is biexact, i.e.
preserves monos in m₂, epis in m₂, sends monos in m₁ to epis, and epis in m₁ to
monos.