Homogeneous linear maps

This file records the degree of a linear map between modules equipped with families of graded subobjects. A linear map has degree q when it maps everything in the degree-p piece of the source into the degree-p + q piece of the target. This is a containment condition, so no direct-sum hypothesis is imposed and a map can be homogeneous of several degrees at once. The families are indexed by an arbitrary SetLike type, so the homogeneity predicate and the additive closure lemmas cover gradings by submodules, additive subgroups and additive submonoids alike. LinearMap.IsHomogeneous.smul additionally needs the target pieces to be closed under a distributive scalar action, and LinearMap.homogeneousSubmodule needs them to be additive submonoids closed under a module action, i.e. a submodule-valued grading.

The multilinear counterpart, and the degree calculus for substitution, are in TauCeti.LinearAlgebra.Graded.Multilinear.

Main definitions

• LinearMap.IsHomogeneous: a linear map shifts homogeneous degree by a fixed amount.
• LinearMap.homogeneousSubmodule: the submodule of linear maps of a fixed degree.

Main results

• LinearMap.IsHomogeneous.comp: degrees add under composition of linear maps.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 3.1.

def TauCeti.LinearMap.IsHomogeneous {R : Type uR} {ι : Type uι} {M : Type uM} {N : Type uN} {σM : Type u_1} {σN : Type u_2} [Semiring R] [AddMonoid ι] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [SetLike σM M] [SetLike σN N] (f : M →ₗ[R] N) (𝒜 : ι → σM) (ℬ : ι → σN) (q : ι) : Prop

A linear map is homogeneous of degree q if it maps the degree-p piece of 𝒜 into the degree-p + q piece of ℬ. No direct-sum hypothesis on the families is needed.

Equations

• TauCeti.LinearMap.IsHomogeneous f 𝒜 ℬ q = ∀ ⦃p : ι⦄ ⦃x : M⦄, x ∈ 𝒜 p → f x ∈ ℬ (p + q)

theorem TauCeti.LinearMap.isHomogeneous_def {R : Type uR} {ι : Type uι} {M : Type uM} {N : Type uN} {σM : Type u_1} {σN : Type u_2} [Semiring R] [AddMonoid ι] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [SetLike σM M] [SetLike σN N] {f : M →ₗ[R] N} {𝒜 : ι → σM} {ℬ : ι → σN} {q : ι} : IsHomogeneous f 𝒜 ℬ q ↔ ∀ (p : ι), ∀ x ∈ 𝒜 p, f x ∈ ℬ (p + q)

Homogeneity of degree q is exactly the mapping condition on homogeneous elements. This is a convenient introduction rule, and IsHomogeneous.map_mem is the corresponding elimination rule.

theorem TauCeti.LinearMap.IsHomogeneous.map_mem {R : Type uR} {ι : Type uι} {M : Type uM} {N : Type uN} {σM : Type u_1} {σN : Type u_2} [Semiring R] [AddMonoid ι] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [SetLike σM M] [SetLike σN N] {f : M →ₗ[R] N} {𝒜 : ι → σM} {ℬ : ι → σN} {q p : ι} (hf : IsHomogeneous f 𝒜 ℬ q) {x : M} (hx : x ∈ 𝒜 p) : f x ∈ ℬ (p + q)

Apply a homogeneous linear map to a homogeneous element.

@[simp]

theorem TauCeti.LinearMap.isHomogeneous_zero {R : Type uR} {ι : Type uι} {M : Type uM} {N : Type uN} {σM : Type u_1} {σN : Type u_2} [Semiring R] [AddMonoid ι] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [SetLike σM M] [SetLike σN N] [ZeroMemClass σN N] (𝒜 : ι → σM) (ℬ : ι → σN) (q : ι) : IsHomogeneous 0 𝒜 ℬ q

The zero linear map is homogeneous of every degree.

theorem TauCeti.LinearMap.IsHomogeneous.add {R : Type uR} {ι : Type uι} {M : Type uM} {N : Type uN} {σM : Type u_1} {σN : Type u_2} [Semiring R] [AddMonoid ι] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [SetLike σM M] [SetLike σN N] [AddMemClass σN N] {f g : M →ₗ[R] N} {𝒜 : ι → σM} {ℬ : ι → σN} {q : ι} (hf : IsHomogeneous f 𝒜 ℬ q) (hg : IsHomogeneous g 𝒜 ℬ q) : IsHomogeneous (f + g) 𝒜 ℬ q

A sum of linear maps of the same degree has that degree.

@[simp]

theorem TauCeti.LinearMap.isHomogeneous_id {R : Type uR} {ι : Type uι} {M : Type uM} {σM : Type u_1} [Semiring R] [AddMonoid ι] [AddCommMonoid M] [Module R M] [SetLike σM M] (𝒜 : ι → σM) : IsHomogeneous LinearMap.id 𝒜 𝒜 0

The identity linear map is homogeneous of degree zero.

theorem TauCeti.LinearMap.IsHomogeneous.comp {R : Type uR} {ι : Type uι} {M : Type uM} {N : Type uN} {σM : Type u_1} {σN : Type u_2} [Semiring R] [AddMonoid ι] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [SetLike σM M] [SetLike σN N] {P : Type uP} {σP : Type u_3} [AddCommMonoid P] [Module R P] [SetLike σP P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} {𝒜 : ι → σM} {ℬ : ι → σN} {𝒞 : ι → σP} {q r : ι} (hg : IsHomogeneous g ℬ 𝒞 r) (hf : IsHomogeneous f 𝒜 ℬ q) : IsHomogeneous (g ∘ₗ f) 𝒜 𝒞 (q + r)

Degrees add under composition of linear maps.

theorem TauCeti.LinearMap.IsHomogeneous.neg {R : Type uR} {ι : Type uι} {M : Type uM} {N : Type uN} {σM : Type u_1} {σN : Type u_2} [Semiring R] [AddMonoid ι] [AddCommMonoid M] [AddCommGroup N] [Module R M] [Module R N] [SetLike σM M] [SetLike σN N] [NegMemClass σN N] {f : M →ₗ[R] N} {𝒜 : ι → σM} {ℬ : ι → σN} {q : ι} (hf : IsHomogeneous f 𝒜 ℬ q) : IsHomogeneous (-f) 𝒜 ℬ q

The negative of a homogeneous linear map has the same degree.

theorem TauCeti.LinearMap.IsHomogeneous.sub {R : Type uR} {ι : Type uι} {M : Type uM} {N : Type uN} {σM : Type u_1} {σN : Type u_2} [Semiring R] [AddMonoid ι] [AddCommMonoid M] [AddCommGroup N] [Module R M] [Module R N] [SetLike σM M] [SetLike σN N] [AddMemClass σN N] [NegMemClass σN N] {f g : M →ₗ[R] N} {𝒜 : ι → σM} {ℬ : ι → σN} {q : ι} (hf : IsHomogeneous f 𝒜 ℬ q) (hg : IsHomogeneous g 𝒜 ℬ q) : IsHomogeneous (f - g) 𝒜 ℬ q

A difference of linear maps of the same degree has that degree.

theorem TauCeti.LinearMap.IsHomogeneous.smul {R : Type uR} {S : Type u_1} {ι : Type uι} {M : Type uM} {N : Type uN} {σM : Type u_2} {σN : Type u_3} [Semiring R] [AddMonoid ι] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [SetLike σM M] [SetLike σN N] [DistribSMul S N] [SMulCommClass R S N] [SMulMemClass σN S N] {f : M →ₗ[R] N} {𝒜 : ι → σM} {ℬ : ι → σN} {q : ι} (hf : IsHomogeneous f 𝒜 ℬ q) (s : S) : IsHomogeneous (s • f) 𝒜 ℬ q

A scalar multiple of a homogeneous linear map has the same degree.

def TauCeti.LinearMap.homogeneousSubmodule {R : Type uR} {S : Type u_1} {ι : Type uι} {M : Type uM} {N : Type uN} {σM : Type u_2} {σN : Type u_3} [Semiring R] [AddMonoid ι] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [SetLike σM M] [SetLike σN N] [Semiring S] [Module S N] [SMulCommClass R S N] [AddSubmonoidClass σN N] [SMulMemClass σN S N] (𝒜 : ι → σM) (ℬ : ι → σN) (q : ι) : Submodule S (M →ₗ[R] N)

Linear maps of a fixed degree form a submodule over any scalar ring acting on the target.

Equations

• TauCeti.LinearMap.homogeneousSubmodule 𝒜 ℬ q = { carrier := {f : M →ₗ[R] N | TauCeti.LinearMap.IsHomogeneous f 𝒜 ℬ q}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.LinearMap.mem_homogeneousSubmodule {R : Type uR} {S : Type u_1} {ι : Type uι} {M : Type uM} {N : Type uN} {σM : Type u_2} {σN : Type u_3} [Semiring R] [AddMonoid ι] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [SetLike σM M] [SetLike σN N] [Semiring S] [Module S N] [SMulCommClass R S N] [AddSubmonoidClass σN N] [SMulMemClass σN S N] {f : M →ₗ[R] N} {𝒜 : ι → σM} {ℬ : ι → σN} {q : ι} : f ∈ homogeneousSubmodule 𝒜 ℬ q ↔ IsHomogeneous f 𝒜 ℬ q