Morphisms of differential graded right modules

A morphism of differential graded right modules is an Aᵐᵒᵖ-linear map which preserves every homogeneous degree and commutes with the differentials. This file bundles these maps and supplies their pointwise module structure, extensionality, identity, and composition API. They form the degree-zero closed maps which later enter the morphism complexes and DG category of right modules.

Main definitions

• TauCeti.DGRightModuleHom: a degree-zero right-module map commuting with the differentials.
• TauCeti.DGRightModuleHom.id and TauCeti.DGRightModuleHom.comp: identity and composition.

References

• B. Keller, Deriving DG categories, Sections 1 and 2.

structure TauCeti.DGRightModuleHom {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} (hM : IsDGRightModule h ℳ dM) (hN : IsDGRightModule h ℳN dN) extends M →ₗ[Aᵐᵒᵖ] N : Type (max uM uN)

A morphism of differential graded right modules: a right-module homomorphism which preserves the internal degree and commutes with the differentials.

• toFun : M → N
• map_add' (x y : M) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : Aᵐᵒᵖ) (x : M) : self.toFun (m • x) = (RingHom.id Aᵐᵒᵖ) m • self.toFun x
• map_mem' {q : ℤ} {x : M} : x ∈ ℳ q → self.toLinearMap x ∈ ℳN q

  A DG right-module morphism preserves each homogeneous degree.

• map_d' (x : M) : dN (self.toLinearMap x) = self.toLinearMap (dM x)

  A DG right-module morphism commutes with the differentials.

theorem TauCeti.DGRightModuleHom.toLinearMap_injective {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} : Function.Injective toLinearMap

Two DG right-module morphisms are equal if their underlying module homomorphisms are equal.

@[instance_reducible]

instance TauCeti.DGRightModuleHom.instFunLike {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} : FunLike (DGRightModuleHom hM hN) M N

Equations

• TauCeti.DGRightModuleHom.instFunLike = { coe := fun (f : TauCeti.DGRightModuleHom hM hN) => ⇑f.toLinearMap, coe_injective := ⋯ }

instance TauCeti.DGRightModuleHom.instGradedFunLikeSubmoduleInt {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} : GradedFunLike (DGRightModuleHom hM hN) ℳ ℳN

instance TauCeti.DGRightModuleHom.instLinearMapClassMulOpposite {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} : LinearMapClass (DGRightModuleHom hM hN) Aᵐᵒᵖ M N

@[instance_reducible]

instance TauCeti.DGRightModuleHom.instCoeOutLinearMapMulOppositeId {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} : CoeOut (DGRightModuleHom hM hN) (M →ₗ[Aᵐᵒᵖ] N)

Equations

• TauCeti.DGRightModuleHom.instCoeOutLinearMapMulOppositeId = { coe := TauCeti.DGRightModuleHom.toLinearMap }

@[simp]

theorem TauCeti.DGRightModuleHom.coe_toLinearMap {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} (f : DGRightModuleHom hM hN) : ⇑f.toLinearMap = ⇑f

@[simp]

theorem TauCeti.DGRightModuleHom.coe_mk {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} (f : M →ₗ[Aᵐᵒᵖ] N) (hf : ∀ {q : ℤ} {x : M}, x ∈ ℳ q → f x ∈ ℳN q) (hdf : ∀ (x : M), dN (f x) = f (dM x)) : ⇑{ toLinearMap := f, map_mem' := hf, map_d' := hdf } = ⇑f

theorem TauCeti.DGRightModuleHom.ext {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} {f g : DGRightModuleHom hM hN} (hfg : ∀ (x : M), f x = g x) : f = g

Two DG right-module morphisms are equal if they agree on every element.

theorem TauCeti.DGRightModuleHom.ext_iff {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} {f g : DGRightModuleHom hM hN} : f = g ↔ ∀ (x : M), f x = g x

@[simp]

theorem TauCeti.DGRightModuleHom.map_d {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} (f : DGRightModuleHom hM hN) (x : M) : dN (f x) = f (dM x)

A DG right-module morphism commutes with the differentials.

@[instance_reducible]

instance TauCeti.DGRightModuleHom.instZero {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} : Zero (DGRightModuleHom hM hN)

Equations

• TauCeti.DGRightModuleHom.instZero = { zero := let __LinearMap := 0; { toLinearMap := __LinearMap, map_mem' := ⋯, map_d' := ⋯ } }

@[instance_reducible]

instance TauCeti.DGRightModuleHom.instAdd {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} : Add (DGRightModuleHom hM hN)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.DGRightModuleHom.instNeg {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} : Neg (DGRightModuleHom hM hN)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.DGRightModuleHom.instSub {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} : Sub (DGRightModuleHom hM hN)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DGRightModuleHom.zero_apply {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} (x : M) : 0 x = 0

@[simp]

theorem TauCeti.DGRightModuleHom.add_apply {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} (f g : DGRightModuleHom hM hN) (x : M) : (f + g) x = f x + g x

@[simp]

theorem TauCeti.DGRightModuleHom.neg_apply {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} (f : DGRightModuleHom hM hN) (x : M) : (-f) x = -f x

@[simp]

theorem TauCeti.DGRightModuleHom.sub_apply {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} (f g : DGRightModuleHom hM hN) (x : M) : (f - g) x = f x - g x

@[instance_reducible]

instance TauCeti.DGRightModuleHom.instSMulNat {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} : SMul ℕ (DGRightModuleHom hM hN)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.DGRightModuleHom.instSMulInt {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} : SMul ℤ (DGRightModuleHom hM hN)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.DGRightModuleHom.instAddCommGroup {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} : AddCommGroup (DGRightModuleHom hM hN)

Equations

• TauCeti.DGRightModuleHom.instAddCommGroup = Function.Injective.addCommGroup TauCeti.DGRightModuleHom.toLinearMap ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance TauCeti.DGRightModuleHom.instSMul {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} : SMul R (DGRightModuleHom hM hN)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DGRightModuleHom.smul_apply {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} (r : R) (f : DGRightModuleHom hM hN) (x : M) : (r • f) x = r • f x

@[instance_reducible]

instance TauCeti.DGRightModuleHom.instModule {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} : Module R (DGRightModuleHom hM hN)

Equations

• TauCeti.DGRightModuleHom.instModule = Function.Injective.module R { toFun := TauCeti.DGRightModuleHom.toLinearMap, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

def TauCeti.DGRightModuleHom.id {R : Type uR} {A : Type uA} {M : Type uM} [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) : DGRightModuleHom hM hM

The identity morphism of a differential graded right module.

Equations

• TauCeti.DGRightModuleHom.id hM = { toLinearMap := LinearMap.id, map_mem' := ⋯, map_d' := ⋯ }

@[simp]

theorem TauCeti.DGRightModuleHom.id_toLinearMap {R : Type uR} {A : Type uA} {M : Type uM} [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) : (DGRightModuleHom.id hM).toLinearMap = LinearMap.id

@[simp]

theorem TauCeti.DGRightModuleHom.coe_id {R : Type uR} {A : Type uA} {M : Type uM} [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) : ⇑(DGRightModuleHom.id hM) = id

@[simp]

theorem TauCeti.DGRightModuleHom.id_apply {R : Type uR} {A : Type uA} {M : Type uM} [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) (x : M) : (DGRightModuleHom.id hM) x = x

def TauCeti.DGRightModuleHom.comp {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [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} (g : DGRightModuleHom hN hP) (f : DGRightModuleHom hM hN) : DGRightModuleHom hM hP

Composition of morphisms of differential graded right modules.

Equations

• g.comp f = { toLinearMap := g.toLinearMap ∘ₗ f.toLinearMap, map_mem' := ⋯, map_d' := ⋯ }

@[simp]

theorem TauCeti.DGRightModuleHom.comp_toLinearMap {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [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} (g : DGRightModuleHom hN hP) (f : DGRightModuleHom hM hN) : (g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap

@[simp]

theorem TauCeti.DGRightModuleHom.coe_comp {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [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} (g : DGRightModuleHom hN hP) (f : DGRightModuleHom hM hN) : ⇑(g.comp f) = ⇑g ∘ ⇑f

@[simp]

theorem TauCeti.DGRightModuleHom.comp_apply {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [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} (g : DGRightModuleHom hN hP) (f : DGRightModuleHom hM hN) (x : M) : (g.comp f) x = g (f x)

@[simp]

theorem TauCeti.DGRightModuleHom.comp_id {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} (f : DGRightModuleHom hM hN) : f.comp (DGRightModuleHom.id hM) = f

Composing a DG right-module morphism on the right with the identity morphism of its source leaves it unchanged.

@[simp]

theorem TauCeti.DGRightModuleHom.id_comp {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [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 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} {hM : IsDGRightModule h ℳ dM} {hN : IsDGRightModule h ℳN dN} (f : DGRightModuleHom hM hN) : (DGRightModuleHom.id hN).comp f = f

Composing a DG right-module morphism on the left with the identity morphism of its target leaves it unchanged.

@[simp]

theorem TauCeti.DGRightModuleHom.comp_assoc {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [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} {Q : Type u_1} [AddCommGroup Q] [Module R Q] [Module Aᵐᵒᵖ Q] [IsScalarTower R Aᵐᵒᵖ Q] {ℳQ : ℤ → Submodule R Q} [SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳQ] [DirectSum.Decomposition ℳQ] {dQ : Q →ₗ[R] Q} {hQ : IsDGRightModule h ℳQ dQ} (k : DGRightModuleHom hP hQ) (g : DGRightModuleHom hN hP) (f : DGRightModuleHom hM hN) : (k.comp g).comp f = k.comp (g.comp f)

Composition of DG right-module morphisms is associative.