The Koszul-signed opposite of an internally graded algebra

For an internally ℤ-graded algebra A, its graded opposite has the same underlying graded module and the multiplication

op a * op b = (-1) ^ (p * q) • op (b * a)

when a and b have degrees p and q. The sign is essential for differentials and higher graded operations; Mathlib's ordinary MulOpposite reverses multiplication without it.

The construction transports the ordinary opposite ring structure through the involution which multiplies degree p by (-1) ^ (p choose 2). The binomial identity (p + q choose 2) = (p choose 2) + (q choose 2) + p*q gives exactly the Koszul sign in the transported product. This avoids choosing degrees for nonhomogeneous elements and makes associativity follow from transport.

Main definitions

• GradedOpposite G: the Koszul-signed opposite algebra associated to an internal grading G.
• GradedOpposite.op and GradedOpposite.unop: the additive, degree-preserving passage between an algebra and its graded opposite.
• GradedOpposite.map: the induced homomorphism of signed opposites of graded algebras.
• GradedOpposite.opAlgEquiv: the algebra equivalence from the ordinary opposite of the graded opposite back to the original algebra.
• GradedOpposite.differential: the linear endomorphism induced on the graded opposite by a linear endomorphism of the algebra, unchanged on underlying elements.

Main results

• GradedOpposite.op_mul: the signed reversed-product formula on homogeneous elements.
• GradedOpposite.op_mem_piece_iff: op preserves degree.
• GradedOpposite.op_mul_op_of_even_right and GradedOpposite.op_mul_op_of_even_left: a homogeneous factor of even degree reverses products without a Koszul sign.
• GradedOpposite.map_id and GradedOpposite.map_comp: functoriality of the signed opposite.
• GradedOpposite.differential_map_mem and GradedOpposite.differential_leibniz: the degree and graded Leibniz laws of a differential transport to the graded opposite, using only those two laws.

The convention follows B. Keller, Introduction to A-infinity algebras and modules, Sections 3 and 7.

inductive TauCeti.GradedOpposite {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] : InternalGrading R A → Type uA

The Koszul-signed opposite of the internally graded algebra A.

Its carrier is a copy of A; its multiplication below includes the Koszul sign.

• op {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (a : A) : GradedOpposite G

  Regard an element as an element of the graded opposite.

def TauCeti.GradedOpposite.unop {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) : GradedOpposite G → A

Return an element of the graded opposite to the original algebra.

Equations

• TauCeti.GradedOpposite.unop G (TauCeti.GradedOpposite.op G a) = a

@[simp]

theorem TauCeti.GradedOpposite.unop_op {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (a : A) : unop G (op G a) = a

@[simp]

theorem TauCeti.GradedOpposite.op_unop {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (a : GradedOpposite G) : op G (unop G a) = a

@[instance_reducible]

noncomputable instance TauCeti.GradedOpposite.instRing {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) : Ring (GradedOpposite G)

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.GradedOpposite.instAlgebra {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) : Algebra R (GradedOpposite G)

Equations

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

noncomputable def TauCeti.GradedOpposite.opAlgEquiv {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) : (GradedOpposite G)ᵐᵒᵖ ≃ₐ[R] A

The ordinary opposite of the Koszul-signed opposite is canonically equivalent to the original algebra. This is the scalar equivalence which identifies left modules over A with right modules over its graded opposite.

Equations

• TauCeti.GradedOpposite.opAlgEquiv G = AlgEquiv.opComm (TauCeti.GradedOpposite.transportAlgEquiv✝ G)

@[simp]

theorem TauCeti.GradedOpposite.opAlgEquiv_op_op {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (a : A) : (opAlgEquiv G) (MulOpposite.op (op G a)) = G.quadraticTwist a

On an element represented by a : A, the scalar equivalence from the ordinary opposite of the graded opposite applies the quadratic twist.

@[simp]

theorem TauCeti.GradedOpposite.opAlgEquiv_symm_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (a : A) : (opAlgEquiv G).symm a = MulOpposite.op (op G (G.quadraticTwist a))

The inverse of the scalar equivalence represents a by the quadratic twist of a, since the quadratic twist is an involution.

theorem TauCeti.GradedOpposite.ext {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) {a b : GradedOpposite G} (h : unop G a = unop G b) : a = b

Two elements of a graded opposite are equal if their underlying elements are equal.

theorem TauCeti.GradedOpposite.ext_iff {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {G : InternalGrading R A} {a b : GradedOpposite G} : a = b ↔ unop G a = unop G b

noncomputable def TauCeti.GradedOpposite.opLinearEquiv {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) : A ≃ₗ[R] GradedOpposite G

Passage to the graded opposite is an R-linear equivalence.

Equations

• TauCeti.GradedOpposite.opLinearEquiv G = { toFun := TauCeti.GradedOpposite.op G, map_add' := ⋯, map_smul' := ⋯, invFun := TauCeti.GradedOpposite.unop G, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.GradedOpposite.opLinearEquiv_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (a : A) : (opLinearEquiv G) a = op G a

@[simp]

theorem TauCeti.GradedOpposite.opLinearEquiv_symm_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (a : GradedOpposite G) : (opLinearEquiv G).symm a = unop G a

noncomputable def TauCeti.GradedOpposite.grading {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) : InternalGrading R (GradedOpposite G)

The grading on the signed opposite, transported degreewise by op.

Equations

• TauCeti.GradedOpposite.grading G = G.map (TauCeti.GradedOpposite.opLinearEquiv G)

theorem TauCeti.GradedOpposite.op_mem_piece_iff {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (p : ℤ) (a : A) : op G a ∈ (grading G).piece p ↔ a ∈ G.piece p

An element belongs to degree p of the graded opposite exactly when its underlying element belongs to degree p in the original algebra.

@[simp]

theorem TauCeti.GradedOpposite.mem_piece_iff {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (p : ℤ) (a : GradedOpposite G) : a ∈ (grading G).piece p ↔ unop G a ∈ G.piece p

Membership in a graded-opposite piece can be tested after applying unop.

@[simp]

theorem TauCeti.GradedOpposite.op_zero {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) : op G 0 = 0

@[simp]

theorem TauCeti.GradedOpposite.op_add {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (a b : A) : op G (a + b) = op G a + op G b

@[simp]

theorem TauCeti.GradedOpposite.op_neg {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (a : A) : op G (-a) = -op G a

@[simp]

theorem TauCeti.GradedOpposite.op_sub {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (a b : A) : op G (a - b) = op G a - op G b

@[simp]

theorem TauCeti.GradedOpposite.op_smul {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (r : R) (a : A) : op G (r • a) = r • op G a

@[simp]

theorem TauCeti.GradedOpposite.op_zsmul {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (n : ℤ) (a : A) : op G (↑n * a) = n • op G a

@[simp]

theorem TauCeti.GradedOpposite.unop_zero {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) : unop G 0 = 0

@[simp]

theorem TauCeti.GradedOpposite.unop_add {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (a b : GradedOpposite G) : unop G (a + b) = unop G a + unop G b

@[simp]

theorem TauCeti.GradedOpposite.unop_neg {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (a : GradedOpposite G) : unop G (-a) = -unop G a

@[simp]

theorem TauCeti.GradedOpposite.unop_sub {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (a b : GradedOpposite G) : unop G (a - b) = unop G a - unop G b

@[simp]

theorem TauCeti.GradedOpposite.unop_smul {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (r : R) (a : GradedOpposite G) : unop G (r • a) = r • unop G a

@[simp]

theorem TauCeti.GradedOpposite.unop_zsmul {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (n : ℤ) (a : GradedOpposite G) : unop G (↑n * a) = n • unop G a

@[simp]

theorem TauCeti.GradedOpposite.op_one {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) [SetLike.GradedMonoid G.piece] : op G 1 = 1

The unit of the graded opposite is the image of the original unit.

@[simp]

theorem TauCeti.GradedOpposite.unop_one {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) [SetLike.GradedMonoid G.piece] : unop G 1 = 1

theorem TauCeti.GradedOpposite.op_mul {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) [SetLike.GradedMonoid G.piece] {p q : ℤ} {a b : A} (ha : a ∈ G.piece p) (hb : b ∈ G.piece q) : op G a * op G b = (p * q).negOnePow • op G (b * a)

Multiplication in the graded opposite reverses homogeneous factors and inserts their Koszul sign.

theorem TauCeti.GradedOpposite.op_mul_op_of_even_right {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) [SetLike.GradedMonoid G.piece] {q : ℤ} {b : A} (hb : b ∈ G.piece q) (hq : Even q) (a : A) : op G a * op G b = op G (b * a)

Multiplying on the right by the image of a homogeneous element of even degree in the graded opposite reverses the factors without a Koszul sign.

theorem TauCeti.GradedOpposite.op_mul_op_of_even_left {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) [SetLike.GradedMonoid G.piece] {q : ℤ} {b : A} (hb : b ∈ G.piece q) (hq : Even q) (a : A) : op G b * op G a = op G (a * b)

Multiplying on the left by the image of a homogeneous element of even degree in the graded opposite reverses the factors without a Koszul sign.

theorem TauCeti.GradedOpposite.unop_mul {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) [SetLike.GradedMonoid G.piece] {p q : ℤ} {a b : GradedOpposite G} (ha : a ∈ (grading G).piece p) (hb : b ∈ (grading G).piece q) : unop G (a * b) = (p * q).negOnePow • (unop G b * unop G a)

Returning a homogeneous product from the graded opposite reverses its factors and retains the Koszul sign.

instance TauCeti.GradedOpposite.instGradedMonoid {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) [SetLike.GradedMonoid G.piece] : SetLike.GradedMonoid (grading G).piece

The homogeneous pieces of a graded opposite are closed under its signed multiplication.

@[instance_reducible]

noncomputable instance TauCeti.GradedOpposite.instGradedAlgebra {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) [SetLike.GradedMonoid G.piece] : GradedAlgebra (grading G).piece

The signed opposite is internally graded by the same degrees as the original algebra.

Equations

• TauCeti.GradedOpposite.instGradedAlgebra G = ⋯.gradedAlgebra

noncomputable def TauCeti.GradedOpposite.map {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {B : Type u_1} [Ring B] [Algebra R B] (G : InternalGrading R A) (H : InternalGrading R B) [GradedAlgebra G.piece] [GradedAlgebra H.piece] (f : G.piece →ₐᵍ[R] H.piece) : (grading G).piece →ₐᵍ[R] (grading H).piece

A graded algebra homomorphism induces a homomorphism of Koszul-signed opposites.

Equations

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

theorem TauCeti.GradedOpposite.map_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {B : Type u_1} [Ring B] [Algebra R B] (G : InternalGrading R A) (H : InternalGrading R B) [GradedAlgebra G.piece] [GradedAlgebra H.piece] (f : G.piece →ₐᵍ[R] H.piece) (x : GradedOpposite G) : (map G H f) x = op H (f (unop G x))

On underlying elements, the induced map is the original homomorphism.

@[simp]

theorem TauCeti.GradedOpposite.map_op {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {B : Type u_1} [Ring B] [Algebra R B] (G : InternalGrading R A) (H : InternalGrading R B) [GradedAlgebra G.piece] [GradedAlgebra H.piece] (f : G.piece →ₐᵍ[R] H.piece) (a : A) : (map G H f) (op G a) = op H (f a)

The induced opposite map sends op a to op (f a).

@[simp]

theorem TauCeti.GradedOpposite.unop_map {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {B : Type u_1} [Ring B] [Algebra R B] (G : InternalGrading R A) (H : InternalGrading R B) [GradedAlgebra G.piece] [GradedAlgebra H.piece] (f : G.piece →ₐᵍ[R] H.piece) (x : GradedOpposite G) : unop H ((map G H f) x) = f (unop G x)

Applying unop after the induced opposite map recovers the original map on unop x.

@[simp]

theorem TauCeti.GradedOpposite.map_id {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) [GradedAlgebra G.piece] : map G G (GradedAlgHom.id R G.piece) = GradedAlgHom.id R (grading G).piece

Taking the signed opposite preserves identity homomorphisms.

@[simp]

theorem TauCeti.GradedOpposite.map_comp {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {B : Type u_1} {C : Type u_2} [Ring B] [Ring C] [Algebra R B] [Algebra R C] (G : InternalGrading R A) (H : InternalGrading R B) (K : InternalGrading R C) [GradedAlgebra G.piece] [GradedAlgebra H.piece] [GradedAlgebra K.piece] (g : H.piece →ₐᵍ[R] K.piece) (f : G.piece →ₐᵍ[R] H.piece) : map G K (g.comp f) = (map H K g).comp (map G H f)

Taking the signed opposite preserves composition.

theorem TauCeti.GradedOpposite.map_injective {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {B : Type u_1} [Ring B] [Algebra R B] (G : InternalGrading R A) (H : InternalGrading R B) [GradedAlgebra G.piece] [GradedAlgebra H.piece] : Function.Injective (map G H)

A homomorphism is determined by its map on signed opposites.

Differentials on the graded opposite

A linear endomorphism d of A induces one on the graded opposite, unchanged on underlying elements. If d raises degree by one and satisfies the graded Leibniz rule on homogeneous left factors, so does the induced map, with respect to the Koszul-signed product. Only these two laws are used, so the transport serves differential graded algebras and curved differential graded algebras alike; the square-zero and curvature laws are added by their respective theories.

noncomputable def TauCeti.GradedOpposite.differential {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (d : A →ₗ[R] A) : GradedOpposite G →ₗ[R] GradedOpposite G

The differential on the graded opposite, unchanged on underlying elements.

Equations

• TauCeti.GradedOpposite.differential G d = (TauCeti.GradedOpposite.opLinearEquiv G).conj d

@[simp]

theorem TauCeti.GradedOpposite.differential_op {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (d : A →ₗ[R] A) (a : A) : (differential G d) (op G a) = op G (d a)

The opposite differential acts by the original differential on underlying elements.

@[simp]

theorem TauCeti.GradedOpposite.differential_unop {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) (d : A →ₗ[R] A) (a : GradedOpposite G) : unop G ((differential G d) a) = d (unop G a)

Returning the opposite differential to the original algebra gives the original differential.

theorem TauCeti.GradedOpposite.differential_map_mem {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) {d : A →ₗ[R] A} (hd : ∀ {p : ℤ} {a : A}, a ∈ G.piece p → d a ∈ G.piece (p + 1)) {p : ℤ} {x : GradedOpposite G} (hx : x ∈ (grading G).piece p) : (differential G d) x ∈ (grading G).piece (p + 1)

If d raises degree by one, so does the opposite differential.

theorem TauCeti.GradedOpposite.differential_leibniz {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (G : InternalGrading R A) [GradedAlgebra G.piece] {d : A →ₗ[R] A} (hd : ∀ {p : ℤ} {a : A}, a ∈ G.piece p → d a ∈ G.piece (p + 1)) (hl : ∀ {p : ℤ} {a : A}, a ∈ G.piece p → ∀ (b : A), d (a * b) = d a * b + p.negOnePow • (a * d b)) {p : ℤ} {x : GradedOpposite G} (hx : x ∈ (grading G).piece p) (y : GradedOpposite G) : (differential G d) (x * y) = (differential G d) x * y + p.negOnePow • (x * (differential G d) y)

The Leibniz rule transports to the graded opposite. If d raises degree by one and satisfies the graded Leibniz rule on homogeneous left factors, then the opposite differential satisfies the graded Leibniz rule on the Koszul-signed opposite. Only these two properties of d are used, so the statement applies to differential graded and to curved differential graded algebras alike.