Additively-graded algebra structures on ⨁ i, A i #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_sum.galgebra R A, the typeclass.direct_sum.galgebra.of_submodules, for creating the above instance from a collection of submodules.direct_sum.to_algebraextendsdirect_sum.to_semiringto produce analg_hom.
@[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)
- to_fun : R →+ A 0
- map_one : ⇑direct_sum.galgebra.to_fun 1 = graded_monoid.ghas_one.one
- map_mul : ∀ (r s : R), graded_monoid.mk 0 (⇑direct_sum.galgebra.to_fun (r * s)) = ⟨0 + 0, graded_monoid.ghas_mul.mul (⇑direct_sum.galgebra.to_fun r) (⇑direct_sum.galgebra.to_fun s)⟩
- commutes : ∀ (r : R) (x : graded_monoid A), graded_monoid.mk 0 (⇑direct_sum.galgebra.to_fun r) * x = x * ⟨0, ⇑direct_sum.galgebra.to_fun r⟩
- smul_def : ∀ (r : R) (x : graded_monoid A), graded_monoid.mk x.fst (r • x.snd) = ⟨0, ⇑direct_sum.galgebra.to_fun r⟩ * x
A graded version of algebra. An instance of direct_sum.galgebra R A endows (⨁ i, A i)
with an R-algebra structure.
Instances of this typeclass
Instances of other typeclasses for direct_sum.galgebra
- direct_sum.galgebra.has_sizeof_inst
@[protected, 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 (direct_sum ι (λ (i : ι), A i))
Equations
- direct_sum.algebra R A = {to_has_smul := smul_zero_class.to_has_smul smul_with_zero.to_smul_zero_class, to_ring_hom := {to_fun := ⇑((direct_sum.of A 0).comp direct_sum.galgebra.to_fun), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
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) :
⇑(algebra_map R (direct_sum ι (λ (i : ι), A i))) r = ⇑(direct_sum.of A 0) (⇑direct_sum.galgebra.to_fun 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] :
↑(algebra_map R (direct_sum ι (λ (i : ι), A i))) = (direct_sum.of A 0).comp direct_sum.galgebra.to_fun
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) :
direct_sum ι (λ (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
- direct_sum.to_algebra R A f hone hmul hcommutes = {to_fun := ⇑(direct_sum.to_semiring (λ (i : ι), (f i).to_add_monoid_hom) hone hmul), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
@[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)
(ᾰ : direct_sum ι (λ (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 : direct_sum ι (λ (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.
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 : direct_sum ι (λ (i : ι), A i) →ₐ[R] B⦄
(h : ∀ (i : ι) (x : A i), ⇑f (⇑(direct_sum.of A i) x) = ⇑g (⇑(direct_sum.of A i) x)) :
f = g
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] :
@[protected, 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
- algebra.direct_sum_galgebra = {to_fun := (algebra_map R A).to_add_monoid_hom, map_one := _, map_mul := _, commutes := _, smul_def := _}