Opposites of internally graded modules

This file applies transport of an internal grading across a linear equivalence to the multiplicative opposite. The degree of an element is unchanged by MulOpposite.op, and an internal graded algebra therefore induces an internal graded algebra on its opposite. The order of homogeneous factors reverses, but their total degree is unchanged because the grading group is ℤ.

The Koszul twist commutes with passage to the opposite. This is the compatibility needed to form opposite DG and A∞ objects without changing their sign convention.

Main definitions

• InternalGrading.opposite: the induced grading on the multiplicative opposite.

Main results

• InternalGrading.op_mem_opposite_piece_iff: op preserves each degree.
• InternalGrading.oppositeGradedAlgebra: a graded algebra induces one on its opposite.
• instGradedSMulOppositeSelf: right multiplication makes a graded algebra a graded right module over itself.
• InternalGrading.op_koszulTwist: the Koszul twist commutes with op.
• InternalGrading.opLinearEquiv_comp_quadraticTwist, InternalGrading.op_quadraticTwist, and InternalGrading.unop_quadraticTwist: the quadratic twist commutes with passage to and from the opposite.

This supplies the opposite compatibility in Layer 0 of the DGAInfinity roadmap. The conventions follow B. Keller, Introduction to A-infinity algebras and modules, Sections 3 and 7.

noncomputable def TauCeti.InternalGrading.opposite {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) : InternalGrading R Mᵐᵒᵖ

The internal grading on the multiplicative opposite, with op x in the same degree as x.

Equations

• G.opposite = G.map (MulOpposite.opLinearEquiv R)

@[simp]

theorem TauCeti.InternalGrading.opposite_piece {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (p : ℤ) : G.opposite.piece p = Submodule.map (↑(MulOpposite.opLinearEquiv R)) (G.piece p)

The degree-p opposite piece is the image of the original piece under op.

theorem TauCeti.InternalGrading.op_mem_opposite_piece_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (p : ℤ) (x : M) : MulOpposite.op x ∈ G.opposite.piece p ↔ x ∈ G.piece p

An opposite element belongs to degree p exactly when the original element does. This is the special case of mem_opposite_piece_iff that simp already reaches.

theorem TauCeti.InternalGrading.mem_opposite_piece_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (p : ℤ) (x : Mᵐᵒᵖ) : x ∈ G.opposite.piece p ↔ MulOpposite.unop x ∈ G.piece p

Membership in an opposite piece is membership of the underlying element in the original piece.

This is not a simp lemma: opposite_piece already rewrites the left-hand side to a Submodule.map, from which the simp set reaches the same right-hand side.

theorem TauCeti.InternalGrading.isHomogeneous_op {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) : LinearMap.IsHomogeneous (↑(MulOpposite.opLinearEquiv R)) G.piece G.opposite.piece 0

Passage to the multiplicative opposite is homogeneous of degree zero.

theorem TauCeti.InternalGrading.isHomogeneous_unop {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) : LinearMap.IsHomogeneous (↑(MulOpposite.opLinearEquiv R).symm) G.opposite.piece G.piece 0

Returning from the multiplicative opposite is homogeneous of degree zero.

theorem TauCeti.InternalGrading.opLinearEquiv_comp_koszulTwist {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) : ↑(MulOpposite.opLinearEquiv R) ∘ₗ G.koszulTwist q = G.opposite.koszulTwist q ∘ₗ ↑(MulOpposite.opLinearEquiv R)

The Koszul twist commutes with the linear equivalence to the multiplicative opposite.

@[simp]

theorem TauCeti.InternalGrading.op_koszulTwist {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) (x : M) : MulOpposite.op ((G.koszulTwist q) x) = (G.opposite.koszulTwist q) (MulOpposite.op x)

Applying the Koszul twist and then op agrees with twisting the opposite element.

@[simp]

theorem TauCeti.InternalGrading.unop_koszulTwist {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) (x : Mᵐᵒᵖ) : MulOpposite.unop ((G.opposite.koszulTwist q) x) = (G.koszulTwist q) (MulOpposite.unop x)

Applying the Koszul twist to an opposite element and then unop agrees with twisting its underlying element.

theorem TauCeti.InternalGrading.opLinearEquiv_comp_quadraticTwist {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) : ↑(MulOpposite.opLinearEquiv R) ∘ₗ G.quadraticTwist = G.opposite.quadraticTwist ∘ₗ ↑(MulOpposite.opLinearEquiv R)

The quadratic twist commutes with the linear equivalence to the multiplicative opposite.

@[simp]

theorem TauCeti.InternalGrading.op_quadraticTwist {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (x : M) : MulOpposite.op (G.quadraticTwist x) = G.opposite.quadraticTwist (MulOpposite.op x)

Applying the quadratic twist and then op agrees with twisting the opposite element.

@[simp]

theorem TauCeti.InternalGrading.unop_quadraticTwist {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (x : Mᵐᵒᵖ) : MulOpposite.unop (G.opposite.quadraticTwist x) = G.quadraticTwist (MulOpposite.unop x)

Applying the quadratic twist to an opposite element and then unop agrees with twisting its underlying element.

instance TauCeti.InternalGrading.oppositeGradedMonoid {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (G : InternalGrading R A) [SetLike.GradedMonoid G.piece] : SetLike.GradedMonoid G.opposite.piece

The opposite pieces are multiplicative: reversing the factors reverses their degrees, which does not change their sum in the integer grading.

@[instance_reducible]

noncomputable instance TauCeti.InternalGrading.oppositeGradedAlgebra {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (G : InternalGrading R A) [SetLike.GradedMonoid G.piece] : GradedAlgebra G.opposite.piece

An internally graded algebra induces the internal graded algebra on its multiplicative opposite.

Equations

• G.oppositeGradedAlgebra = ⋯.gradedAlgebra

instance TauCeti.instGradedSMulOppositeSelf {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ℤ → Submodule R A) [GradedAlgebra 𝒜] : SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece 𝒜

Right multiplication makes a graded algebra a graded right module over itself: the degrees of the two factors add, in the order fixed by the opposite grading.