Internally graded modules

This file packages a ℤ-graded module as a total module together with an internal direct-sum decomposition. The total-module presentation is convenient for DG and A∞ operations, while DirectSum.IsInternal ensures that every element is a finite, uniquely determined sum of homogeneous elements.

Mathlib already provides the direct-sum equivalence and its induction principle through DirectSum.Decomposition. An InternalGrading retains the family of homogeneous submodules and the proof that it is internal; the instance below makes Mathlib's decomposition API available without duplicating it.

The file also records that a finitely generated internally graded module has only finitely many nonzero pieces, the Koszul twist operator used to encode Koszul signs on homogeneous elements, and the letterwise tuple operation that applies it on a half-open index interval.

Main definitions

• InternalGrading: an internal ℤ-grading of a module.
• InternalGrading.ofDecomposition: the internal grading carried by a family of submodules with a DirectSum.Decomposition, as graded algebras store it.
• InternalGrading.map: transport an internal grading across a linear equivalence.
• InternalGrading.koszulTwist: the operator scaling degree-e elements by (-1)^(q * e).
• InternalGrading.quadraticTwist: multiplication of degree p by (-1)^(p choose 2).
• InternalGrading.twistedTuple: a tuple with a consecutive block of letters Koszul-twisted.

Main results

• TauCeti.InternalGrading.ext: internal gradings are determined by their homogeneous pieces.
• TauCeti.InternalGrading.linearMap_ext: linear maps agree when they agree on homogeneous elements.
• TauCeti.InternalGrading.finite_piece_ne_bot: a finitely generated internally graded module has only finitely many nonzero homogeneous pieces.
• TauCeti.InternalGrading.koszulTwist_apply_of_mem: the twist acts by the Koszul scalar on each homogeneous piece.
• TauCeti.InternalGrading.koszulTwist_comp: twists compose by adding the twist parameters.
• TauCeti.InternalGrading.quadraticTwist_involutive: the quadratic twist is an involution.
• TauCeti.LinearMap.IsHomogeneous.linearEquiv_symm: the inverse of a degree-zero homogeneous linear equivalence is homogeneous.
• TauCeti.LinearMap.IsHomogeneous.map_decompose: a homogeneous map commutes with homogeneous projection, up to the shift of degree.
• TauCeti.LinearMap.IsHomogeneous.isHomogeneous_ker and TauCeti.LinearMap.IsHomogeneous.isHomogeneous_range: the kernel and the image of a homogeneous map are homogeneous submodules.
• TauCeti.LinearMap.IsHomogeneous.koszulTwist_comp: a homogeneous linear map commutes with Koszul twists up to the sign determined by its degree.
• TauCeti.LinearMap.IsHomogeneous.twistedTuple_map: a degree-zero homogeneous map commutes with twisting a block of a tuple.

This is the first graded-module target in Layer 0 of the DGAInfinity roadmap. Later files use Mathlib's decomposition API to define maps of nonzero degree, shifts, tensor-product gradings, and signed multilinear operations.

structure TauCeti.InternalGrading (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type v

An internal integer grading of an R-module M.

The isInternal field says that the canonical map from the external direct sum of the piece p to M is bijective. Thus elements of M have unique finite homogeneous decompositions.

• piece : ℤ → Submodule R M

  The submodule of elements of degree p.

• isInternal : DirectSum.IsInternal self.piece

  The homogeneous pieces form an internal direct sum.

theorem TauCeti.InternalGrading.ext {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {G H : InternalGrading R M} : (∀ (p : ℤ), G.piece p = H.piece p) → G = H

Two internal gradings of the same module are equal as soon as their homogeneous pieces agree.

theorem TauCeti.InternalGrading.ext_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {G H : InternalGrading R M} : G = H ↔ ∀ (p : ℤ), G.piece p = H.piece p

@[instance_reducible]

noncomputable instance TauCeti.InternalGrading.instDecompositionIntSubmodulePiece {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) : DirectSum.Decomposition G.piece

The decomposition attached to an internal grading.

Equations

• G.instDecompositionIntSubmodulePiece = DirectSum.IsInternal.chooseDecomposition G.piece ⋯

noncomputable def TauCeti.InternalGrading.ofDecomposition {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (ℳ : ℤ → Submodule R M) [DirectSum.Decomposition ℳ] : InternalGrading R M

The internal grading carried by a family of submodules with a DirectSum.Decomposition. This is the bridge from Mathlib's decomposition typeclass, under which graded algebras are stated, to the bundled internal grading of this file.

Equations

• TauCeti.InternalGrading.ofDecomposition ℳ = { piece := ℳ, isInternal := ⋯ }

@[simp]

theorem TauCeti.InternalGrading.ofDecomposition_piece {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (ℳ : ℤ → Submodule R M) [DirectSum.Decomposition ℳ] : (ofDecomposition ℳ).piece = ℳ

@[simp]

theorem TauCeti.InternalGrading.isHomogeneous_ofDecomposition_piece_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (ℳ : ℤ → Submodule R M) [DirectSum.Decomposition ℳ] (U : Submodule R M) : DirectSum.SetLike.IsHomogeneous (ofDecomposition ℳ).piece U ↔ DirectSum.SetLike.IsHomogeneous ℳ U

A submodule is homogeneous for the internal grading ofDecomposition ℳ exactly when it is homogeneous for ℳ: the decomposition carried by ofDecomposition ℳ is the given one, as decompositions are unique.

theorem TauCeti.InternalGrading.linearMap_ext {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] (G : InternalGrading R M) {f g : M →ₗ[R] N} (h : ∀ (p : ℤ), ∀ x ∈ G.piece p, f x = g x) : f = g

Two linear maps on an internally graded module agree if they agree on homogeneous elements.

theorem TauCeti.InternalGrading.span_setOf_exists_mem_piece_eq_top {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_1) [Semiring S] [Module S M] (G : InternalGrading R M) : Submodule.span S {x : M | ∃ (p : ℤ), x ∈ G.piece p} = ⊤

The homogeneous elements of an internally graded module span it over any scalar semiring acting on the total module. No compatibility between that action and the grading is needed.

noncomputable def TauCeti.InternalGrading.map {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] (G : InternalGrading R M) (e : M ≃ₗ[R] N) : InternalGrading R N

Transport an internal grading across a linear equivalence. The degree-p piece of the target is the image of the degree-p piece of the source.

Equations

• G.map e = { piece := fun (p : ℤ) => Submodule.map (↑e) (G.piece p), isInternal := ⋯ }

@[simp]

theorem TauCeti.InternalGrading.map_piece {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] (G : InternalGrading R M) (e : M ≃ₗ[R] N) (p : ℤ) : (G.map e).piece p = Submodule.map (↑e) (G.piece p)

The degree-p piece of a transported grading is the image of the original piece.

theorem TauCeti.InternalGrading.mem_map_piece_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] (G : InternalGrading R M) (e : M ≃ₗ[R] N) (p : ℤ) (y : N) : y ∈ (G.map e).piece p ↔ e.symm y ∈ G.piece p

Membership in a transported piece can be checked after applying the inverse equivalence.

This is not a simp lemma: map_piece already rewrites the left-hand side to a Submodule.map, on which the simp set fires Submodule.mem_map_equiv to reach the same right-hand side.

theorem TauCeti.InternalGrading.apply_mem_map_piece_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] (G : InternalGrading R M) (e : M ≃ₗ[R] N) (p : ℤ) (x : M) : e x ∈ (G.map e).piece p ↔ x ∈ G.piece p

A linear equivalence maps a homogeneous element into the transported piece of the same degree. This is the special case of mem_map_piece_iff that simp already reaches.

theorem TauCeti.InternalGrading.isHomogeneous_map {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] (G : InternalGrading R M) (e : M ≃ₗ[R] N) : LinearMap.IsHomogeneous (↑e) G.piece (G.map e).piece 0

The equivalence used to transport a grading is homogeneous of degree zero.

theorem TauCeti.InternalGrading.isHomogeneous_map_symm {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] (G : InternalGrading R M) (e : M ≃ₗ[R] N) : LinearMap.IsHomogeneous (↑e.symm) (G.map e).piece G.piece 0

The inverse of an equivalence used to transport a grading is homogeneous of degree zero.

@[simp]

theorem TauCeti.InternalGrading.map_refl {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) : G.map (LinearEquiv.refl R M) = G

Transport along the identity equivalence leaves an internal grading unchanged.

@[simp]

theorem TauCeti.InternalGrading.map_trans {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {P : Type u_1} [AddCommMonoid P] [Module R P] (G : InternalGrading R M) (e : M ≃ₗ[R] N) (f : N ≃ₗ[R] P) : (G.map e).map f = G.map (e ≪≫ₗ f)

Successive transport agrees with transport along the composite equivalence.

theorem TauCeti.InternalGrading.map_eq_map_decompose {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] (G : InternalGrading R M) (f : M →+ N) {i : ℤ} (hf : ∀ (j : ℤ), ∀ x ∈ G.piece j, j ≠ i → f x = 0) (x : M) : f x = f ↑(((DirectSum.decompose G.piece) x) i)

An additive map that vanishes on every homogeneous piece except degree i sees only the degree-i component of each argument.

theorem TauCeti.LinearMap.IsHomogeneous.linearEquiv_symm {R : Type u_1} {S : Type u_2} {M : Type v} {N : Type w} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [AddCommMonoid N] [Module R N] [Module S N] {G : InternalGrading R M} {H : InternalGrading R N} {e : M ≃ₗ[S] N} (he : IsHomogeneous (↑e) G.piece H.piece 0) : IsHomogeneous (↑e.symm) H.piece G.piece 0

The inverse of a degree-zero homogeneous linear equivalence of internally graded modules is again homogeneous of degree zero. The equivalence may be linear over a ring S other than the ring R over which the homogeneous pieces are submodules.

theorem TauCeti.LinearMap.IsHomogeneous.map_decompose {R : Type u_3} {S : Type u_4} {M : Type v} {N : Type w} [Semiring R] [Semiring S] [SMul R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[S] N} {r : ℤ} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] {𝓝 : ℤ → Submodule R N} [DirectSum.Decomposition 𝓝] (hf : IsHomogeneous f ℳ 𝓝 r) (p : ℤ) (x : M) : f ↑(((DirectSum.decompose ℳ) x) p) = ↑(((DirectSum.decompose 𝓝) (f x)) (p + r))

A homogeneous linear map of degree r carries the degree-p component of an element to the degree-(p + r) component of its image. The gradings are any families of submodules with DirectSum.Decomposition instances, so this applies to the pieces of internal gradings and to Mathlib's graded algebras alike.

theorem TauCeti.LinearMap.IsHomogeneous.isHomogeneous_ker {R : Type u_3} {S : Type u_4} {M : Type v} {N : Type w} [Semiring R] [Semiring S] [SMul R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[S] N} {r : ℤ} {G : InternalGrading R M} {H : InternalGrading R N} (hf : IsHomogeneous f G.piece H.piece r) : DirectSum.SetLike.IsHomogeneous G.piece f.ker

The kernel of a homogeneous linear map is a homogeneous submodule.

theorem TauCeti.LinearMap.IsHomogeneous.isHomogeneous_range {R : Type u_3} {S : Type u_4} {M : Type v} {N : Type w} [Semiring R] [Semiring S] [SMul R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[S] N} {r : ℤ} {G : InternalGrading R M} {H : InternalGrading R N} (hf : IsHomogeneous f G.piece H.piece r) : DirectSum.SetLike.IsHomogeneous H.piece f.range

The image of a homogeneous linear map is a homogeneous submodule.

theorem TauCeti.InternalGrading.finite_piece_ne_bot {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) [Module.Finite R M] : {p : ℤ | G.piece p ≠ ⊥}.Finite

A finitely generated internally graded module has only finitely many nonzero homogeneous pieces.

theorem TauCeti.InternalGrading.sum_decompose_toFinset {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (hG : {p : ℤ | G.piece p ≠ ⊥}.Finite) (x : M) : ∑ p ∈ hG.toFinset, ↑(((DirectSum.decompose G.piece) x) p) = x

Summing the homogeneous components over the finite set of nonzero pieces reconstructs the original element.

noncomputable def TauCeti.InternalGrading.koszulTwist {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) : M →ₗ[R] M

The Koszul twist of parameter q: on the homogeneous piece of degree e it acts as the scalar (-1)^(q * e).

This is multiplication by the same coefficient that MultilinearMap.koszulSign records for a single homogeneous input of degree e. Downstream modules express their Koszul signs through this operator: the sign acquired by moving an operation of degree q past homogeneous inputs of total degree D is the scalar by which koszulTwist G q scales those inputs.

Equations

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

noncomputable def TauCeti.InternalGrading.twistedTuple {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) {n : ℕ} (x : Fin n → M) (a p : ℕ) : Fin n → M

The tuple x with exactly the letters at positions in the half-open interval [a, a + p) Koszul-twisted. Downstream, the Taylor summand collapsing the block of length d starting at a + p is supported on this tuple: the collapse carries the Koszul sign of moving the operation past those preceding letters, and twisting them is how that sign is encoded.

Equations

• G.twistedTuple q x a p i = if a ≤ ↑i ∧ ↑i < a + p then (G.koszulTwist q) (x i) else x i

theorem TauCeti.InternalGrading.koszulTwist_apply_of_mem {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) {x : M} {e : ℤ} (hx : x ∈ G.piece e) (q : ℤ) : (G.koszulTwist q) x = ↑↑(q * e).negOnePow • x

On a homogeneous element of degree e, the Koszul twist of parameter q acts as the scalar (-1)^(q * e).

theorem TauCeti.InternalGrading.koszulTwist_mem_piece {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) {x : M} {e : ℤ} (hx : x ∈ G.piece e) (q : ℤ) : (G.koszulTwist q) x ∈ G.piece e

The Koszul twist preserves each homogeneous piece.

@[simp]

theorem TauCeti.InternalGrading.koszulTwist_zero {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) : G.koszulTwist 0 = LinearMap.id

The Koszul twist of parameter zero is the identity.

theorem TauCeti.InternalGrading.koszulTwist_comp {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q q' : ℤ) : G.koszulTwist q ∘ₗ G.koszulTwist q' = G.koszulTwist (q + q')

Koszul twists compose by adding their parameters.

@[simp]

theorem TauCeti.InternalGrading.koszulTwist_two_mul {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) : G.koszulTwist (2 * q) = LinearMap.id

The Koszul twist of an even parameter is the identity.

@[simp]

theorem TauCeti.InternalGrading.koszulTwist_two {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) : G.koszulTwist 2 = LinearMap.id

The Koszul twist of parameter two is the identity.

@[simp]

theorem TauCeti.InternalGrading.koszulTwist_comp_self {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) : G.koszulTwist q ∘ₗ G.koszulTwist q = LinearMap.id

The Koszul twist of any parameter is an involution.

@[simp]

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

The Koszul twist of any parameter is an involution, pointwise.

theorem TauCeti.LinearMap.IsHomogeneous.koszulTwist_comp {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {H : InternalGrading R N} {f : M →ₗ[R] N} {r : ℤ} (hf : IsHomogeneous f G.piece H.piece r) (q : ℤ) : H.koszulTwist q ∘ₗ f = ↑↑(q * r).negOnePow • f ∘ₗ G.koszulTwist q

A homogeneous linear map of degree r commutes with the Koszul twist of parameter q up to the scalar (-1)^(q * r). This is the operator form of the sign acquired by moving a degree-r map past a homogeneous input.

@[simp]

theorem TauCeti.InternalGrading.twistedTuple_apply_of_mem_Ico {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) {n : ℕ} (x : Fin n → M) (a p : ℕ) (i : Fin n) (hi : a ≤ ↑i ∧ ↑i < a + p) : G.twistedTuple q x a p i = (G.koszulTwist q) (x i)

Evaluation of twistedTuple on an index inside the twisted interval [a, a + p).

@[simp]

theorem TauCeti.InternalGrading.twistedTuple_apply_of_not_mem_Ico {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) {n : ℕ} (x : Fin n → M) (a p : ℕ) (i : Fin n) (hi : ¬(a ≤ ↑i ∧ ↑i < a + p)) : G.twistedTuple q x a p i = x i

Evaluation of twistedTuple on an index outside the twisted interval [a, a + p).

@[simp]

theorem TauCeti.InternalGrading.twistedTuple_apply {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) {n : ℕ} (x : Fin n → M) (a p : ℕ) (i : Fin n) : G.twistedTuple q x a p i = if a ≤ ↑i ∧ ↑i < a + p then (G.koszulTwist q) (x i) else x i

Unfolding of twistedTuple as a branch on membership in [a, a + p).

theorem TauCeti.LinearMap.IsHomogeneous.twistedTuple_map {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] {N : Type w} [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {H : InternalGrading R N} {f : M →ₗ[R] N} (hf : IsHomogeneous f G.piece H.piece 0) (q : ℤ) {n : ℕ} (x : Fin n → M) (a p : ℕ) : H.twistedTuple q (fun (i : Fin n) => f (x i)) a p = fun (i : Fin n) => f (G.twistedTuple q x a p i)

A degree-zero homogeneous linear map commutes with twisting a consecutive block of a tuple.

@[simp]

theorem TauCeti.InternalGrading.twistedTuple_zero_length {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) {n : ℕ} (x : Fin n → M) (a : ℕ) : G.twistedTuple q x a 0 = x

Twisting an empty interval leaves the tuple unchanged.

@[simp]

theorem TauCeti.InternalGrading.twistedTuple_zero_twist {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) {n : ℕ} (x : Fin n → M) (a p : ℕ) : G.twistedTuple 0 x a p = x

The Koszul twist of parameter zero leaves every letter of the tuple unchanged.

def TauCeti.InternalGrading.quadraticExponent (p : ℤ) : ℤ

The quadratic sign exponent attached to degree p, namely the generalized binomial coefficient p choose 2.

Equations

• TauCeti.InternalGrading.quadraticExponent p = Ring.choose p 2

@[simp]

theorem TauCeti.InternalGrading.quadraticExponent_zero : quadraticExponent 0 = 0

The quadratic exponent vanishes in degree zero.

theorem TauCeti.InternalGrading.quadraticExponent_add (p q : ℤ) : quadraticExponent (p + q) = quadraticExponent p + quadraticExponent q + p * q

The quadratic exponent turns addition into addition plus the bilinear cross term.

theorem TauCeti.InternalGrading.negOnePow_quadraticExponent_add (p q : ℤ) : (quadraticExponent (p + q)).negOnePow = (p * q).negOnePow * (quadraticExponent p).negOnePow * (quadraticExponent q).negOnePow

The signs associated to the quadratic exponent differ under addition by the Koszul sign.

noncomputable def TauCeti.InternalGrading.quadraticTwist {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) : M →ₗ[R] M

The quadratic twist multiplies the degree-p component by (-1) ^ (p choose 2).

Transporting the ordinary opposite multiplication through this involution produces the Koszul-signed opposite multiplication.

Equations

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

theorem TauCeti.InternalGrading.quadraticTwist_apply_of_mem {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) {x : M} {p : ℤ} (hx : x ∈ G.piece p) : G.quadraticTwist x = ↑↑(quadraticExponent p).negOnePow • x

On a homogeneous element of degree p, the quadratic twist is multiplication by (-1) ^ (p choose 2).

theorem TauCeti.InternalGrading.quadraticTwist_mem_piece {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) {x : M} {p : ℤ} (hx : x ∈ G.piece p) : G.quadraticTwist x ∈ G.piece p

The quadratic twist preserves every homogeneous piece.

theorem TauCeti.InternalGrading.quadraticTwist_involutive {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) : Function.Involutive ⇑G.quadraticTwist

Applying the quadratic twist twice is the identity.

noncomputable def TauCeti.InternalGrading.quadraticTwistEquiv {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) : M ≃ₗ[R] M

The quadratic twist as a linear involution.

Equations

• G.quadraticTwistEquiv = LinearEquiv.ofInvolutive G.quadraticTwist ⋯

@[simp]

theorem TauCeti.InternalGrading.quadraticTwistEquiv_apply {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (x : M) : G.quadraticTwistEquiv x = G.quadraticTwist x

@[simp]

theorem TauCeti.InternalGrading.quadraticTwistEquiv_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (x : M) : G.quadraticTwistEquiv.symm x = G.quadraticTwist x