Composition in differential graded right-module Hom complexes #
Homogeneous right-module cochains are closed under composition. If g has degree p and f
has degree q, their composite has degree p + q, and the graded-commutator differential obeys
\delta(g \circ f) = \delta(g) \circ f + (-1)^p g \circ \delta(f).
Consequently composition assembles into a morphism of cochain complexes
Hom(N, P) \otimes Hom(M, N) \longrightarrow Hom(M, P).
The order of the tensor factors is Keller's order: the map applied second occurs first. This is also the order for which the tensor-product differential gives the displayed Leibniz rule. The closed composition and unit maps are the algebraic input for the DG category of right modules.
Main definitions #
TauCeti.dgRightModuleCochains.comp: composition of homogeneous right-module cochains.TauCeti.dgRightModuleCochainCompTensor: composition on a pair of homogeneous degrees.TauCeti.dgRightModuleHomComplexComp: composition as a morphism of cochain complexes.TauCeti.dgRightModuleHomComplexUnit: the identity cochain as a morphism from the tensor unit.
References #
- B. Keller, Deriving DG categories, Section 2.
def
TauCeti.dgRightModuleCochains.comp
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{ℳ : ℤ → Submodule R M}
{ℳN : ℤ → Submodule R N}
{ℳP : ℤ → Submodule R P}
{p q j : ℤ}
(g : ↥(dgRightModuleCochains p))
(f : ↥(dgRightModuleCochains q))
(hpq : p + q = j)
:
Composition of homogeneous right-module cochains.
Instances For
@[simp]
theorem
TauCeti.dgRightModuleCochains.comp_apply
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{ℳ : ℤ → Submodule R M}
{ℳN : ℤ → Submodule R N}
{ℳP : ℤ → Submodule R P}
{p q j : ℤ}
(g : ↥(dgRightModuleCochains p))
(f : ↥(dgRightModuleCochains q))
(hpq : p + q = j)
(x : M)
:
Composition of homogeneous right-module cochains is pointwise composition.
@[simp]
theorem
TauCeti.dgRightModuleCochains.add_comp
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{ℳ : ℤ → Submodule R M}
{ℳN : ℤ → Submodule R N}
{ℳP : ℤ → Submodule R P}
{p q j : ℤ}
(g g' : ↥(dgRightModuleCochains p))
(f : ↥(dgRightModuleCochains q))
(hpq : p + q = j)
:
@[simp]
theorem
TauCeti.dgRightModuleCochains.comp_add
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{ℳ : ℤ → Submodule R M}
{ℳN : ℤ → Submodule R N}
{ℳP : ℤ → Submodule R P}
{p q j : ℤ}
(g : ↥(dgRightModuleCochains p))
(f f' : ↥(dgRightModuleCochains q))
(hpq : p + q = j)
:
@[simp]
theorem
TauCeti.dgRightModuleCochains.zero_comp
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{ℳ : ℤ → Submodule R M}
{ℳN : ℤ → Submodule R N}
{ℳP : ℤ → Submodule R P}
{p q j : ℤ}
(f : ↥(dgRightModuleCochains q))
(hpq : p + q = j)
:
@[simp]
theorem
TauCeti.dgRightModuleCochains.comp_zero
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{ℳ : ℤ → Submodule R M}
{ℳN : ℤ → Submodule R N}
{ℳP : ℤ → Submodule R P}
{p q j : ℤ}
(g : ↥(dgRightModuleCochains p))
(hpq : p + q = j)
:
@[simp]
theorem
TauCeti.dgRightModuleCochains.smul_comp
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{ℳ : ℤ → Submodule R M}
{ℳN : ℤ → Submodule R N}
{ℳP : ℤ → Submodule R P}
{p q j : ℤ}
(r : R)
(g : ↥(dgRightModuleCochains p))
(f : ↥(dgRightModuleCochains q))
(hpq : p + q = j)
:
@[simp]
theorem
TauCeti.dgRightModuleCochains.comp_smul
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{ℳ : ℤ → Submodule R M}
{ℳN : ℤ → Submodule R N}
{ℳP : ℤ → Submodule R P}
{p q j : ℤ}
(r : R)
(g : ↥(dgRightModuleCochains p))
(f : ↥(dgRightModuleCochains q))
(hpq : p + q = j)
:
def
TauCeti.dgRightModuleCochains.id
{R A M : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
:
The degree-zero identity cochain of a graded right module.
Equations
Instances For
@[simp]
theorem
TauCeti.dgRightModuleCochains.comp_id
{R A M N : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
{ℳ : ℤ → Submodule R M}
{ℳN : ℤ → Submodule R N}
{p : ℤ}
(f : ↥(dgRightModuleCochains p))
:
Composing on the right with the identity cochain changes nothing.
@[simp]
theorem
TauCeti.dgRightModuleCochains.id_comp
{R A M N : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
{ℳ : ℤ → Submodule R M}
{ℳN : ℤ → Submodule R N}
{p : ℤ}
(f : ↥(dgRightModuleCochains p))
:
Composing on the left with the identity cochain changes nothing.
@[simp]
theorem
TauCeti.dgRightModuleCochains.comp_assoc
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{ℳ : ℤ → Submodule R M}
{ℳN : ℤ → Submodule R N}
{ℳP : ℤ → Submodule R P}
{Q : Type u}
[AddCommGroup Q]
[Module R Q]
[Module Aᵐᵒᵖ Q]
[IsScalarTower R Aᵐᵒᵖ Q]
{ℳQ : ℤ → Submodule R Q}
{r p q j : ℤ}
(k : ↥(dgRightModuleCochains r))
(g : ↥(dgRightModuleCochains p))
(f : ↥(dgRightModuleCochains q))
(hrpq : r + p + q = j)
:
Composition of homogeneous right-module cochains is associative.
theorem
TauCeti.dgRightModuleCochains.gradedCommutator_comp
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{d : A →ₗ[R] A}
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
{ℳN : ℤ → Submodule R N}
[DirectSum.Decomposition ℳN]
{dN : N →ₗ[R] N}
{ℳP : ℤ → Submodule R P}
{dP : P →ₗ[R] P}
(hMh : LinearMap.IsHomogeneous dM ℳ ℳ 1)
(hMl :
∀ {q : ℤ} {x : M},
x ∈ ℳ q → ∀ (a : A), dM (MulOpposite.op a • x) = MulOpposite.op a • dM x + q.negOnePow • MulOpposite.op (d a) • x)
(hNh : LinearMap.IsHomogeneous dN ℳN ℳN 1)
(hNl :
∀ {q : ℤ} {x : N},
x ∈ ℳN q → ∀ (a : A), dN (MulOpposite.op a • x) = MulOpposite.op a • dN x + q.negOnePow • MulOpposite.op (d a) • x)
(hPh : LinearMap.IsHomogeneous dP ℳP ℳP 1)
(hPl :
∀ {q : ℤ} {x : P},
x ∈ ℳP q → ∀ (a : A), dP (MulOpposite.op a • x) = MulOpposite.op a • dP x + q.negOnePow • MulOpposite.op (d a) • x)
{p q : ℤ}
(g : ↥(dgRightModuleCochains p))
(f : ↥(dgRightModuleCochains q))
:
(gradedCommutator hMh ⋯ hPh ⋯ (p + q)) (comp g f ⋯) = comp ((gradedCommutator hNh ⋯ hPh ⋯ p) g) f ⋯ + p.negOnePow • comp g ((gradedCommutator hMh ⋯ hNh ⋯ q) f) ⋯
The graded commutator satisfies the graded Leibniz rule for composition of cochains, with the sign carried by the degree of the outer factor. Only the degree and the Leibniz rule of the module differentials enter, so this is the Leibniz rule of the Hom differentials of both ordinary and curved differential graded right modules.
@[simp]
theorem
TauCeti.dgRightModuleCochains.gradedCommutator_id
{R A M : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
{d : A →ₗ[R] A}
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hMh : LinearMap.IsHomogeneous dM ℳ ℳ 1)
(hMl :
∀ {q : ℤ} {x : M},
x ∈ ℳ q → ∀ (a : A), dM (MulOpposite.op a • x) = MulOpposite.op a • dM x + q.negOnePow • MulOpposite.op (d a) • x)
:
The identity cochain is closed for the graded commutator.
theorem
TauCeti.dgRightModuleCochains.differential_comp
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
{ℳN : ℤ → Submodule R N}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳN]
[DirectSum.Decomposition ℳN]
{dN : N →ₗ[R] N}
{ℳP : ℤ → Submodule R P}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳP]
[DirectSum.Decomposition ℳP]
{dP : P →ₗ[R] P}
{hM : IsDGRightModule h ℳ dM}
{hN : IsDGRightModule h ℳN dN}
{hP : IsDGRightModule h ℳP dP}
{p q : ℤ}
(g : ↥(dgRightModuleCochains p))
(f : ↥(dgRightModuleCochains q))
:
(differential (p + q)) (comp g f ⋯) = comp ((differential p) g) f ⋯ + p.negOnePow • comp g ((differential q) f) ⋯
The differential on homogeneous right-module cochains satisfies the graded Leibniz rule for composition.
@[simp]
theorem
TauCeti.dgRightModuleCochains.differential_id
{R A M : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
:
The identity cochain is closed.
noncomputable def
TauCeti.dgRightModuleCochainCompTensor
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
{ℳN : ℤ → Submodule R N}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳN]
[DirectSum.Decomposition ℳN]
{dN : N →ₗ[R] N}
{ℳP : ℤ → Submodule R P}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳP]
[DirectSum.Decomposition ℳP]
{dP : P →ₗ[R] P}
{hM : IsDGRightModule h ℳ dM}
{hN : IsDGRightModule h ℳN dN}
{hP : IsDGRightModule h ℳP dP}
(p q j : ℤ)
(hpq : p + q = j)
:
CategoryTheory.MonoidalCategoryStruct.tensorObj ((dgRightModuleHomComplex hN hP).X p)
((dgRightModuleHomComplex hM hN).X q) ⟶ (dgRightModuleHomComplex hM hP).X j
Composition on a pair of homogeneous degrees, as a map out of the tensor product of the two cochain modules.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.dgRightModuleCochainCompTensor_tmul
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
{ℳN : ℤ → Submodule R N}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳN]
[DirectSum.Decomposition ℳN]
{dN : N →ₗ[R] N}
{ℳP : ℤ → Submodule R P}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳP]
[DirectSum.Decomposition ℳP]
{dP : P →ₗ[R] P}
{hM : IsDGRightModule h ℳ dM}
{hN : IsDGRightModule h ℳN dN}
{hP : IsDGRightModule h ℳP dP}
(p q j : ℤ)
(hpq : p + q = j)
(g : ↥(dgRightModuleCochains p))
(f : ↥(dgRightModuleCochains q))
:
(ModuleCat.Hom.hom (dgRightModuleCochainCompTensor p q j hpq)) (g ⊗ₜ[R] f) = dgRightModuleCochains.comp g f hpq
On a pure tensor, homogeneous composition is ordinary composition of the underlying maps.
noncomputable def
TauCeti.dgRightModuleHomComplexComp
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
{ℳN : ℤ → Submodule R N}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳN]
[DirectSum.Decomposition ℳN]
{dN : N →ₗ[R] N}
{ℳP : ℤ → Submodule R P}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳP]
[DirectSum.Decomposition ℳP]
{dP : P →ₗ[R] P}
{hM : IsDGRightModule h ℳ dM}
{hN : IsDGRightModule h ℳN dN}
{hP : IsDGRightModule h ℳP dP}
:
Composition of DG right-module cochains is a closed degree-zero map of Hom complexes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
TauCeti.dgRightModuleHomComplexUnit
{R A M : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
:
The identity cochain, as a closed morphism from the tensor unit to the endomorphism Hom complex.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.dgRightModuleHomComplexUnit_f_zero_apply
{R A M : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
(r : R)
:
The degree-zero component of the unit sends a scalar to that scalar multiple of the identity cochain.
@[simp]
theorem
TauCeti.ι_dgRightModuleHomComplexComp
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
{ℳN : ℤ → Submodule R N}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳN]
[DirectSum.Decomposition ℳN]
{dN : N →ₗ[R] N}
{ℳP : ℤ → Submodule R P}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳP]
[DirectSum.Decomposition ℳP]
{dP : P →ₗ[R] P}
{hM : IsDGRightModule h ℳ dM}
{hN : IsDGRightModule h ℳN dN}
{hP : IsDGRightModule h ℳP dP}
(p q j : ℤ)
(hpq : p + q = j)
:
CategoryTheory.CategoryStruct.comp
(HomologicalComplex.ιMapBifunctor (dgRightModuleHomComplex hN hP) (dgRightModuleHomComplex hM hN)
(CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)) (ComplexShape.up ℤ) p q j hpq)
(dgRightModuleHomComplexComp.f j) = dgRightModuleCochainCompTensor p q j hpq
Restricting closed composition to a pair of homogeneous summands gives pointwise composition.
@[simp]
theorem
TauCeti.ι_dgRightModuleHomComplexComp_assoc
{R A M N P : Type u}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
[AddCommGroup P]
[Module R P]
[Module Aᵐᵒᵖ P]
[IsScalarTower R Aᵐᵒᵖ P]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
{ℳN : ℤ → Submodule R N}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳN]
[DirectSum.Decomposition ℳN]
{dN : N →ₗ[R] N}
{ℳP : ℤ → Submodule R P}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳP]
[DirectSum.Decomposition ℳP]
{dP : P →ₗ[R] P}
{hM : IsDGRightModule h ℳ dM}
{hN : IsDGRightModule h ℳN dN}
{hP : IsDGRightModule h ℳP dP}
(p q j : ℤ)
(hpq : p + q = j)
{Z : ModuleCat R}
(h✝ : (dgRightModuleHomComplex hM hP).X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(HomologicalComplex.ιMapBifunctor (dgRightModuleHomComplex hN hP) (dgRightModuleHomComplex hM hN)
(CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)) (ComplexShape.up ℤ) p q j hpq)
(CategoryTheory.CategoryStruct.comp (dgRightModuleHomComplexComp.f j) h✝) = CategoryTheory.CategoryStruct.comp (dgRightModuleCochainCompTensor p q j hpq) h✝
Restricting closed composition to a pair of homogeneous summands gives pointwise composition.