The Hom complex of differential graded right modules #
For two right modules over a differential graded algebra, the degree-p cochains are the
right-module linear maps which raise internal degree by p. Their differential is the graded
commutator
\delta(f) = d_N \circ f - (-1)^p f \circ d_M.
The right-module convention is important here: homogeneous cochains are ordinary
A\^op-linear maps. The two Leibniz terms involving the differential of the algebra cancel in
the displayed commutator, so it is again A\^op-linear and has degree p + 1. This file packages
these cochains and their differential as a cochain complex of modules over the ground ring. Its
degree-zero cocycles are exactly TauCeti.DGRightModuleHom.
Main definitions #
TauCeti.dgRightModuleCochains: homogeneous cochains of a fixed degree between two right DG modules.TauCeti.dgRightModuleCochains.gradedCommutator: the graded commutator of a cochain with two module differentials obeying the right Leibniz rule. Only the Leibniz rule and the degree of the differentials enter, so it also differentiates cochains between curved DG right modules.TauCeti.dgRightModuleHomComplex: the cochain complex of homogeneous right-module maps.TauCeti.dgRightModuleHomLinearEquivZeroCocycles: the linear identification of DG morphisms with closed degree-zero cochains.
Implementation notes #
dgRightModuleHomComplex is exposed because the component types of its public differential
application lemma reduce to the advertised homogeneous-cochain modules. The element-level API is
given by dgRightModuleCochains.differential_apply.
References #
- B. Keller, Deriving DG categories, Section 2.
def
TauCeti.dgRightModuleCochains
{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 M}
{ℳN : ℤ → Submodule R N}
(p : ℤ)
:
The R-submodule of right-module maps of degree p between two differential graded right
modules. The differential does not enter the definition; it supplies the differential between
successive cochain modules below.
Equations
Instances For
@[simp]
theorem
TauCeti.dgRightModuleCochains.mem_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 M}
{ℳN : ℤ → Submodule R N}
{p : ℤ}
{f : M →ₗ[Aᵐᵒᵖ] N}
:
theorem
TauCeti.dgRightModuleCochains.map_mem
{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 M}
{ℳN : ℤ → Submodule R N}
{p q : ℤ}
(f : ↥(dgRightModuleCochains p))
{x : M}
(hx : x ∈ ℳ q)
:
A homogeneous right-module cochain applied to an element of degree q has degree q + p.
def
TauCeti.dgRightModuleCochains.gradedCommutator
{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]
{d : A →ₗ[R] A}
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
{ℳN : ℤ → Submodule R N}
{dN : N →ₗ[R] N}
(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)
(p : ℤ)
:
The graded commutator f ↦ dN ∘ f - (-1) ^ p • f ∘ dM on degree-p right-module
cochains. It only needs module differentials of degree one obeying the right graded Leibniz
rule against the same algebra map d; neither a square-zero nor a curvature equation enters.
It is the differential of the Hom complexes of both ordinary and curved differential graded
right modules.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.dgRightModuleCochains.gradedCommutator_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]
{d : A →ₗ[R] A}
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
{ℳN : ℤ → Submodule R N}
{dN : N →ₗ[R] N}
(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)
(p : ℤ)
(f : ↥(dgRightModuleCochains p))
(x : M)
:
Evaluating the graded commutator of a cochain.
theorem
TauCeti.dgRightModuleCochains.gradedCommutator_gradedCommutator_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]
{d : A →ₗ[R] A}
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
{ℳN : ℤ → Submodule R N}
{dN : N →ₗ[R] N}
(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)
(p : ℤ)
(f : ↥(dgRightModuleCochains p))
(x : M)
:
↑((gradedCommutator hMh ⋯ hNh ⋯ (p + 1)) ((gradedCommutator hMh ⋯ hNh ⋯ p) f)) x = dN (dN (↑f x)) - ↑f (dM (dM x))
Applying the graded commutator twice composes the cochain with the squares of the two module differentials: the mixed terms cancel by the sign rule.
def
TauCeti.dgRightModuleCochains.differential
{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}
(p : ℤ)
:
The differential on homogeneous right-module cochains.
Equations
Instances For
@[simp]
theorem
TauCeti.dgRightModuleCochains.differential_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}
(p : ℤ)
(f : ↥(dgRightModuleCochains p))
(x : M)
:
Evaluating the differential gives the graded commutator with the module differentials.
theorem
TauCeti.dgRightModuleCochains.differential_comp_self
{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}
(p : ℤ)
:
The differential on right-module cochains squares to zero.
def
TauCeti.dgRightModuleHomComplex
{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)
:
CochainComplex (ModuleCat R) ℤ
The Hom complex between two differential graded right modules. Its degree-p term consists
of the right-module linear maps raising internal degree by p, and its differential is the graded
commutator with the two module differentials.
Equations
- TauCeti.dgRightModuleHomComplex hM hN = CochainComplex.of (fun (p : ℤ) => ↧↥(TauCeti.dgRightModuleCochains p)) (fun (p : ℤ) => ModuleCat.ofHom (TauCeti.dgRightModuleCochains.differential p)) ⋯
Instances For
@[simp]
theorem
TauCeti.dgRightModuleHomComplex_X
{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)
(p : ℤ)
:
The degree-p term of the Hom complex is the module of degree-p homogeneous cochains.
@[simp]
theorem
TauCeti.dgRightModuleHomComplex_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)
(p : ℤ)
:
(dgRightModuleHomComplex hM hN).d p (p + 1) = ModuleCat.ofHom (dgRightModuleCochains.differential p)
The differential morphism of the Hom complex is induced by the graded commutator map.
@[simp]
theorem
TauCeti.dgRightModuleHomComplex_d_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)
(p : ℤ)
(f : ↑((dgRightModuleHomComplex hM hN).X p))
:
(ModuleCat.Hom.hom ((dgRightModuleHomComplex hM hN).d p (p + 1))) f = (dgRightModuleCochains.differential p) f
The differential of the Hom complex, evaluated on a homogeneous cochain, is the graded commutator with the module differentials.
def
TauCeti.dgRightModuleHomEquivZeroCocycles
{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)
:
Closed degree-zero cochains in the Hom complex are exactly morphisms of differential graded right modules.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.dgRightModuleHomEquivZeroCocycles_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)
:
The zero-cocycle associated to a DG right-module morphism has the same underlying map.
@[simp]
theorem
TauCeti.dgRightModuleHomEquivZeroCocycles_symm_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 : ↥(dgRightModuleCochains.differential 0).ker)
(x : M)
:
The DG right-module morphism associated to a zero-cocycle has the same underlying map.
def
TauCeti.dgRightModuleHomLinearEquivZeroCocycles
{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)
:
The identification of DG right-module maps with closed degree-zero cochains is linear.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.dgRightModuleHomLinearEquivZeroCocycles_toEquiv
{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)
:
@[simp]
theorem
TauCeti.dgRightModuleHomLinearEquivZeroCocycles_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)
:
The zero-cocycle associated linearly to a DG right-module morphism has the same underlying map.
@[simp]
theorem
TauCeti.dgRightModuleHomLinearEquivZeroCocycles_symm_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 : ↥(dgRightModuleCochains.differential 0).ker)
(x : M)
:
The DG right-module morphism associated linearly to a zero-cocycle has the same underlying map.