mathlib documentation

algebra.direct_sum.algebra

Additively-graded algebra structures on ⨁ i, A i #

This file provides R-algebra structures on external direct sums of R-modules.

Recall that if A i are a family of add_comm_monoids indexed by an add_monoid, then an instance of direct_sum.gmonoid A is a multiplication A i → A j → A (i + j) giving ⨁ i, A i the structure of a semiring. In this file, we introduce the direct_sum.galgebra R A class for the case where all A i are R-modules. This is the extra structure needed to promote ⨁ i, A i to an R-algebra.

Main definitions #

Direct sums of subobjects #

Additionally, this module provides the instance direct_sum.galgebra.of_submodules which promotes any instance constructed with direct_sum.gmonoid.of_submodules to an R-algebra.

@[class]
structure direct_sum.galgebra {ι : Type uι} (R : Type uR) (A : ι → Type uA) [decidable_eq ι] [comm_semiring R] [Π (i : ι), add_comm_monoid (A i)] [Π (i : ι), module R (A i)] [add_monoid ι] [direct_sum.gsemiring A] :
Type (max uA uR)

A graded version of algebra. An instance of direct_sum.galgebra R A endows (⨁ i, A i) with an R-algebra structure.

Instances
@[instance]
def direct_sum.algebra {ι : Type uι} (R : Type uR) (A : ι → Type uA) [decidable_eq ι] [comm_semiring R] [Π (i : ι), add_comm_monoid (A i)] [Π (i : ι), module R (A i)] [add_monoid ι] [direct_sum.gsemiring A] [direct_sum.galgebra R A] :
algebra R (⨁ (i : ι), A i)
Equations
theorem direct_sum.algebra_map_apply {ι : Type uι} (R : Type uR) (A : ι → Type uA) [decidable_eq ι] [comm_semiring R] [Π (i : ι), add_comm_monoid (A i)] [Π (i : ι), module R (A i)] [add_monoid ι] [direct_sum.gsemiring A] [direct_sum.galgebra R A] (r : R) :
theorem direct_sum.algebra_map_to_add_monoid_hom {ι : Type uι} (R : Type uR) (A : ι → Type uA) [decidable_eq ι] [comm_semiring R] [Π (i : ι), add_comm_monoid (A i)] [Π (i : ι), module R (A i)] [add_monoid ι] [direct_sum.gsemiring A] [direct_sum.galgebra R A] :
@[instance]
def direct_sum.galgebra.of_submodules {ι : Type uι} (R : Type uR) {B : Type uB} [decidable_eq ι] [comm_semiring R] [add_monoid ι] [semiring B] [algebra R B] (carriers : ι → submodule R B) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.galgebra R (λ (i : ι), (carriers i))

A direct_sum.gmonoid instance produced by direct_sum.gmonoid.of_submodules is automatically a direct_sum.galgebra.

Equations
@[simp]
theorem direct_sum.galgebra.of_submodules_to_fun_apply {ι : Type uι} (R : Type uR) {B : Type uB} [decidable_eq ι] [comm_semiring R] [add_monoid ι] [semiring B] [algebra R B] (carriers : ι → submodule R B) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) (ᾰ : R) :
def direct_sum.to_algebra {ι : Type uι} (R : Type uR) (A : ι → Type uA) {B : Type uB} [decidable_eq ι] [comm_semiring R] [Π (i : ι), add_comm_monoid (A i)] [Π (i : ι), module R (A i)] [add_monoid ι] [direct_sum.gsemiring A] [semiring B] [direct_sum.galgebra R A] [algebra R B] (f : Π (i : ι), A i →ₗ[R] B) (hone : (f 0) graded_monoid.ghas_one.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (graded_monoid.ghas_mul.mul ai aj) = ((f i) ai) * (f j) aj) (hcommutes : ∀ (r : R), (f 0) (direct_sum.galgebra.to_fun r) = (algebra_map R B) r) :
(⨁ (i : ι), A i) →ₐ[R] B

A family of linear_maps preserving direct_sum.ghas_one.one and direct_sum.ghas_mul.mul describes an alg_hom on ⨁ i, A i. This is a stronger version of direct_sum.to_semiring.

Of particular interest is the case when A i are bundled subojects, f is the family of coercions such as submodule.subtype (A i), and the [gmonoid A] structure originates from direct_sum.gmonoid.of_add_submodules, in which case the proofs about ghas_one and ghas_mul can be discharged by rfl.

Equations
@[simp]
theorem direct_sum.to_algebra_apply {ι : Type uι} (R : Type uR) (A : ι → Type uA) {B : Type uB} [decidable_eq ι] [comm_semiring R] [Π (i : ι), add_comm_monoid (A i)] [Π (i : ι), module R (A i)] [add_monoid ι] [direct_sum.gsemiring A] [semiring B] [direct_sum.galgebra R A] [algebra R B] (f : Π (i : ι), A i →ₗ[R] B) (hone : (f 0) graded_monoid.ghas_one.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (graded_monoid.ghas_mul.mul ai aj) = ((f i) ai) * (f j) aj) (hcommutes : ∀ (r : R), (f 0) (direct_sum.galgebra.to_fun r) = (algebra_map R B) r) (ᾰ : ⨁ (i : ι), (λ (i : ι), A i) i) :
(direct_sum.to_algebra R A f hone hmul hcommutes) = (direct_sum.to_semiring (λ (i : ι), (f i).to_add_monoid_hom) hone hmul)
@[ext]
theorem direct_sum.alg_hom_ext {ι : Type uι} (R : Type uR) (A : ι → Type uA) {B : Type uB} [decidable_eq ι] [comm_semiring R] [Π (i : ι), add_comm_monoid (A i)] [Π (i : ι), module R (A i)] [add_monoid ι] [direct_sum.gsemiring A] [semiring B] [direct_sum.galgebra R A] [algebra R B] ⦃f g : (⨁ (i : ι), A i) →ₐ[R] B⦄ (h : ∀ (i : ι), f.to_linear_map.comp (direct_sum.lof R ι A i) = g.to_linear_map.comp (direct_sum.lof R ι A i)) :
f = g

Two alg_homs out of a direct sum are equal if they agree on the generators.

See note [partially-applied ext lemmas].

Concrete instances #

@[simp]
theorem algebra.direct_sum_galgebra_to_fun {ι : Type uι} {R : Type u_1} {A : Type u_2} [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A] :
@[instance]
def algebra.direct_sum_galgebra {ι : Type uι} {R : Type u_1} {A : Type u_2} [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A] :
direct_sum.galgebra R (λ (i : ι), A)

A direct sum of copies of a algebra inherits the algebra structure.

Equations