Documentation

Mathlib.Algebra.DirectSum.Internal

Internally graded rings and algebras #

This module provides DirectSum.GSemiring and DirectSum.GCommSemiring instances for a collection of subobjects A when a SetLike.GradedMonoid instance is available:

With these instances in place, it provides the bundled canonical maps out of a direct sum of subobjects into their carrier type:

DirectSum.coeRingHom (a RingHom version of DirectSum.coeAddMonoidHom)
DirectSum.coeAlgHom (an AlgHom version of DirectSum.coeLinearMap)

Strictly the definitions in this file are not sufficient to fully define an "internal" direct sum; to represent this case, (h : DirectSum.IsInternal A) [SetLike.GradedMonoid A] is needed. In the future there will likely be a data-carrying, constructive, typeclass version of DirectSum.IsInternal for providing an explicit decomposition function.

When CompleteLattice.Independent (Set.range A) (a weaker condition than DirectSum.IsInternal A), these provide a grading of ⨆ i, A i, and the mapping ⨁ i, A i →+ ⨆ i, A i can be obtained as DirectSum.toAddMonoid (fun i ↦ AddSubmonoid.inclusion <| le_iSup A i).

This file also provides some extra structure on A 0, namely:

SetLike.GradeZero.subsemiring, which leads to
- SetLike.GradeZero.instSemiring
- SetLike.GradeZero.instCommSemiring
SetLike.GradeZero.subring, which leads to
- SetLike.GradeZero.instRing
- SetLike.GradeZero.instCommRing
SetLike.GradeZero.subalgebra, which leads to
- SetLike.GradeZero.instAlgebra

Tags #

internally graded ring

instance AddCommMonoid.ofSubmonoidOnSemiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) (i : ι) :

AddCommMonoid { x : R // x ∈ A i }

Equations

AddCommMonoid.ofSubmonoidOnSemiring A i = inferInstance

instance AddCommGroup.ofSubgroupOnRing {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Ring R] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) (i : ι) :

AddCommGroup { x : R // x ∈ A i }

Equations

AddCommGroup.ofSubgroupOnRing A i = inferInstance

theorem SetLike.algebraMap_mem_graded {ι : Type u_1} {S : Type u_3} {R : Type u_4} [Zero ι] [CommSemiring S] [Semiring R] [Algebra S R] (A : ι → Submodule S R) [SetLike.GradedOne A] (s : S) :

(algebraMap S R) s ∈ A 0

theorem SetLike.natCast_mem_graded {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Zero ι] [AddMonoidWithOne R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedOne A] (n : ℕ) :

↑n ∈ A 0

@[deprecated SetLike.natCast_mem_graded]

theorem SetLike.nat_cast_mem_graded {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Zero ι] [AddMonoidWithOne R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedOne A] (n : ℕ) :

↑n ∈ A 0

Alias of SetLike.natCast_mem_graded.

theorem SetLike.intCast_mem_graded {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Zero ι] [AddGroupWithOne R] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) [SetLike.GradedOne A] (z : ℤ) :

↑z ∈ A 0

@[deprecated SetLike.intCast_mem_graded]

theorem SetLike.int_cast_mem_graded {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Zero ι] [AddGroupWithOne R] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) [SetLike.GradedOne A] (z : ℤ) :

↑z ∈ A 0

Alias of SetLike.intCast_mem_graded.

From `AddSubmonoid`s and `AddSubgroup`s #

instance SetLike.gnonUnitalNonAssocSemiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Add ι] [NonUnitalNonAssocSemiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedMul A] :

DirectSum.GNonUnitalNonAssocSemiring fun (i : ι) => { x : R // x ∈ A i }

Build a DirectSum.GNonUnitalNonAssocSemiring instance for a collection of additive submonoids.

Equations

SetLike.gnonUnitalNonAssocSemiring A = DirectSum.GNonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

instance SetLike.gsemiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddMonoid ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedMonoid A] :

DirectSum.GSemiring fun (i : ι) => { x : R // x ∈ A i }

Build a DirectSum.GSemiring instance for a collection of additive submonoids.

Equations

SetLike.gsemiring A = DirectSum.GSemiring.mk ⋯ ⋯ ⋯ GradedMonoid.GMonoid.gnpow ⋯ ⋯ (fun (n : ℕ) => ⟨↑n, ⋯⟩) ⋯ ⋯

instance SetLike.gcommSemiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddCommMonoid ι] [CommSemiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedMonoid A] :

DirectSum.GCommSemiring fun (i : ι) => { x : R // x ∈ A i }

Build a DirectSum.GCommSemiring instance for a collection of additive submonoids.

Equations

SetLike.gcommSemiring A = DirectSum.GCommSemiring.mk ⋯

instance SetLike.gring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddMonoid ι] [Ring R] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) [SetLike.GradedMonoid A] :

DirectSum.GRing fun (i : ι) => { x : R // x ∈ A i }

Build a DirectSum.GRing instance for a collection of additive subgroups.

Equations

SetLike.gring A = DirectSum.GRing.mk (fun (z : ℤ) => ⟨↑z, ⋯⟩) ⋯ ⋯

instance SetLike.gcommRing {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddCommMonoid ι] [CommRing R] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) [SetLike.GradedMonoid A] :

DirectSum.GCommRing fun (i : ι) => { x : R // x ∈ A i }

Build a DirectSum.GCommRing instance for a collection of additive submonoids.

Equations

SetLike.gcommRing A = DirectSum.GCommRing.mk ⋯

def DirectSum.coeRingHom {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddMonoid ι] [SetLike.GradedMonoid A] :

(DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) →+* R

The canonical ring isomorphism between ⨁ i, A i and R

Equations

DirectSum.coeRingHom A = DirectSum.toSemiring (fun (i : ι) => AddSubmonoidClass.subtype (A i)) ⋯ ⋯

Instances For

@[simp]

theorem DirectSum.coeRingHom_of {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddMonoid ι] [SetLike.GradedMonoid A] (i : ι) (x : { x : R // x ∈ A i }) :

(DirectSum.coeRingHom A) ((DirectSum.of (fun (i : ι) => { x : R // x ∈ A i }) i) x) = ↑x

The canonical ring isomorphism between ⨁ i, A i and R

theorem DirectSum.coe_mul_apply {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddMonoid ι] [SetLike.GradedMonoid A] [(i : ι) → (x : { x : R // x ∈ A i }) → Decidable (x ≠ 0)] (r : DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) (r' : DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) (n : ι) :

↑((r * r') n) = ∑ ij ∈ Finset.filter (fun (ij : ι × ι) => ij.1 + ij.2 = n) (DFinsupp.support r ×ˢ DFinsupp.support r'), ↑(r ij.1) * ↑(r' ij.2)

theorem DirectSum.coe_mul_apply_eq_dfinsupp_sum {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddMonoid ι] [SetLike.GradedMonoid A] [(i : ι) → (x : { x : R // x ∈ A i }) → Decidable (x ≠ 0)] (r : DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) (r' : DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) (n : ι) :

↑((r * r') n) = DFinsupp.sum r fun (i : ι) (ri : { x : R // x ∈ A i }) => DFinsupp.sum r' fun (j : ι) (rj : { x : R // x ∈ A j }) => if i + j = n then ↑ri * ↑rj else 0

theorem DirectSum.coe_of_mul_apply_aux {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddMonoid ι] [SetLike.GradedMonoid A] {i : ι} (r : { x : R // x ∈ A i }) (r' : DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) {j : ι} {n : ι} (H : ∀ (x : ι), i + x = n ↔ x = j) :

↑(((DirectSum.of (fun (i : ι) => { x : R // x ∈ A i }) i) r * r') n) = ↑r * ↑(r' j)

theorem DirectSum.coe_mul_of_apply_aux {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddMonoid ι] [SetLike.GradedMonoid A] (r : DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) {i : ι} (r' : { x : R // x ∈ A i }) {j : ι} {n : ι} (H : ∀ (x : ι), x + i = n ↔ x = j) :

↑((r * (DirectSum.of (fun (i : ι) => { x : R // x ∈ A i }) i) r') n) = ↑(r j) * ↑r'

theorem DirectSum.coe_of_mul_apply_add {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddLeftCancelMonoid ι] [SetLike.GradedMonoid A] {i : ι} (r : { x : R // x ∈ A i }) (r' : DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) (j : ι) :

↑(((DirectSum.of (fun (i : ι) => { x : R // x ∈ A i }) i) r * r') (i + j)) = ↑r * ↑(r' j)

theorem DirectSum.coe_mul_of_apply_add {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddRightCancelMonoid ι] [SetLike.GradedMonoid A] (r : DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) {i : ι} (r' : { x : R // x ∈ A i }) (j : ι) :

↑((r * (DirectSum.of (fun (i : ι) => { x : R // x ∈ A i }) i) r') (j + i)) = ↑(r j) * ↑r'

theorem DirectSum.coe_of_mul_apply_of_not_le {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [CanonicallyOrderedAddCommMonoid ι] [SetLike.GradedMonoid A] {i : ι} (r : { x : R // x ∈ A i }) (r' : DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) (n : ι) (h : ¬i ≤ n) :

↑(((DirectSum.of (fun (i : ι) => { x : R // x ∈ A i }) i) r * r') n) = 0

theorem DirectSum.coe_mul_of_apply_of_not_le {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [CanonicallyOrderedAddCommMonoid ι] [SetLike.GradedMonoid A] (r : DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) {i : ι} (r' : { x : R // x ∈ A i }) (n : ι) (h : ¬i ≤ n) :

↑((r * (DirectSum.of (fun (i : ι) => { x : R // x ∈ A i }) i) r') n) = 0

theorem DirectSum.coe_mul_of_apply_of_le {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [CanonicallyOrderedAddCommMonoid ι] [SetLike.GradedMonoid A] [Sub ι] [OrderedSub ι] [ContravariantClass ι ι (fun (x1 x2 : ι) => x1 + x2) fun (x1 x2 : ι) => x1 ≤ x2] (r : DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) {i : ι} (r' : { x : R // x ∈ A i }) (n : ι) (h : i ≤ n) :

↑((r * (DirectSum.of (fun (i : ι) => { x : R // x ∈ A i }) i) r') n) = ↑(r (n - i)) * ↑r'

theorem DirectSum.coe_of_mul_apply_of_le {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [CanonicallyOrderedAddCommMonoid ι] [SetLike.GradedMonoid A] [Sub ι] [OrderedSub ι] [ContravariantClass ι ι (fun (x1 x2 : ι) => x1 + x2) fun (x1 x2 : ι) => x1 ≤ x2] {i : ι} (r : { x : R // x ∈ A i }) (r' : DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) (n : ι) (h : i ≤ n) :

↑(((DirectSum.of (fun (i : ι) => { x : R // x ∈ A i }) i) r * r') n) = ↑r * ↑(r' (n - i))

theorem DirectSum.coe_mul_of_apply {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [CanonicallyOrderedAddCommMonoid ι] [SetLike.GradedMonoid A] [Sub ι] [OrderedSub ι] [ContravariantClass ι ι (fun (x1 x2 : ι) => x1 + x2) fun (x1 x2 : ι) => x1 ≤ x2] (r : DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) {i : ι} (r' : { x : R // x ∈ A i }) (n : ι) [Decidable (i ≤ n)] :

↑((r * (DirectSum.of (fun (i : ι) => { x : R // x ∈ A i }) i) r') n) = if i ≤ n then ↑(r (n - i)) * ↑r' else 0

theorem DirectSum.coe_of_mul_apply {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [CanonicallyOrderedAddCommMonoid ι] [SetLike.GradedMonoid A] [Sub ι] [OrderedSub ι] [ContravariantClass ι ι (fun (x1 x2 : ι) => x1 + x2) fun (x1 x2 : ι) => x1 ≤ x2] {i : ι} (r : { x : R // x ∈ A i }) (r' : DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) (n : ι) [Decidable (i ≤ n)] :

↑(((DirectSum.of (fun (i : ι) => { x : R // x ∈ A i }) i) r * r') n) = if i ≤ n then ↑r * ↑(r' (n - i)) else 0

From `Submodule`s #

instance Submodule.galgebra {ι : Type u_1} {S : Type u_3} {R : Type u_4} [AddMonoid ι] [CommSemiring S] [Semiring R] [Algebra S R] (A : ι → Submodule S R) [SetLike.GradedMonoid A] :

DirectSum.GAlgebra S fun (i : ι) => { x : R // x ∈ A i }

Build a DirectSum.GAlgebra instance for a collection of Submodules.

Equations

Submodule.galgebra A = { toFun := (LinearMap.codRestrict (A 0) (Algebra.linearMap S R) ⋯).toAddMonoidHom, map_one := ⋯, map_mul := ⋯, commutes := ⋯, smul_def := ⋯ }

@[simp]

theorem Submodule.setLike.coe_galgebra_toFun {S : Type u_3} {R : Type u_4} {ι : Type u_5} [AddMonoid ι] [CommSemiring S] [Semiring R] [Algebra S R] (A : ι → Submodule S R) [SetLike.GradedMonoid A] (s : S) :

↑(DirectSum.GAlgebra.toFun s) = (algebraMap S R) s

instance Submodule.nat_power_gradedMonoid {S : Type u_3} {R : Type u_4} [CommSemiring S] [Semiring R] [Algebra S R] (p : Submodule S R) :

SetLike.GradedMonoid fun (i : ℕ) => p ^ i

A direct sum of powers of a submodule of an algebra has a multiplicative structure.

Equations

⋯ = ⋯

def DirectSum.coeAlgHom {ι : Type u_1} {S : Type u_3} {R : Type u_4} [DecidableEq ι] [AddMonoid ι] [CommSemiring S] [Semiring R] [Algebra S R] (A : ι → Submodule S R) [SetLike.GradedMonoid A] :

(DirectSum ι fun (i : ι) => { x : R // x ∈ A i }) →ₐ[S] R

The canonical algebra isomorphism between ⨁ i, A i and R.

Equations

DirectSum.coeAlgHom A = DirectSum.toAlgebra S (fun (i : ι) => { x : R // x ∈ A i }) (fun (i : ι) => (A i).subtype) ⋯ ⋯

Instances For

theorem Submodule.iSup_eq_toSubmodule_range {ι : Type u_1} {S : Type u_3} {R : Type u_4} [DecidableEq ι] [AddMonoid ι] [CommSemiring S] [Semiring R] [Algebra S R] (A : ι → Submodule S R) [SetLike.GradedMonoid A] :

⨆ (i : ι), A i = Subalgebra.toSubmodule (DirectSum.coeAlgHom A).range

The supremum of submodules that form a graded monoid is a subalgebra, and equal to the range of DirectSum.coeAlgHom.

@[simp]

theorem DirectSum.coeAlgHom_of {ι : Type u_1} {S : Type u_3} {R : Type u_4} [DecidableEq ι] [AddMonoid ι] [CommSemiring S] [Semiring R] [Algebra S R] (A : ι → Submodule S R) [SetLike.GradedMonoid A] (i : ι) (x : { x : R // x ∈ A i }) :

(DirectSum.coeAlgHom A) ((DirectSum.of (fun (i : ι) => { x : R // x ∈ A i }) i) x) = ↑x

Facts about grade zero #

def SetLike.GradeZero.subsemiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Semiring R] [AddMonoid ι] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedMonoid A] :

The subsemiring A 0 of R.

Equations

SetLike.GradeZero.subsemiring A = { carrier := ↑(A 0), mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

instance SetLike.GradeZero.instSemiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Semiring R] [AddMonoid ι] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedMonoid A] :

Semiring { x : R // x ∈ A 0 }

The semiring A 0 inherited from R in the presence of SetLike.GradedMonoid A.

Equations

SetLike.GradeZero.instSemiring A = (SetLike.GradeZero.subsemiring A).toSemiring

@[simp]

theorem SetLike.GradeZero.coe_natCast {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Semiring R] [AddMonoid ι] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedMonoid A] (n : ℕ) :

↑↑n = ↑n

@[simp]

theorem SetLike.GradeZero.coe_ofNat {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Semiring R] [AddMonoid ι] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedMonoid A] (n : ℕ) [n.AtLeastTwo] :

↑(OfNat.ofNat n) = OfNat.ofNat n

instance SetLike.GradeZero.instCommSemiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [CommSemiring R] [AddCommMonoid ι] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedMonoid A] :

CommSemiring { x : R // x ∈ A 0 }

The commutative semiring A 0 inherited from R in the presence of SetLike.GradedMonoid A.

Equations

SetLike.GradeZero.instCommSemiring A = (SetLike.GradeZero.subsemiring A).toCommSemiring

def SetLike.GradeZero.subring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Ring R] [AddMonoid ι] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) [SetLike.GradedMonoid A] :

The subring A 0 of R.

Equations

SetLike.GradeZero.subring A = { carrier := ↑(A 0), mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

Instances For

instance SetLike.GradeZero.instRing {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Ring R] [AddMonoid ι] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) [SetLike.GradedMonoid A] :

Ring { x : R // x ∈ A 0 }

The ring A 0 inherited from R in the presence of SetLike.GradedMonoid A.

Equations

SetLike.GradeZero.instRing A = (SetLike.GradeZero.subring A).toRing

theorem SetLike.GradeZero.coe_intCast {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Ring R] [AddMonoid ι] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) [SetLike.GradedMonoid A] (z : ℤ) :

↑↑z = ↑z

instance SetLike.GradeZero.instCommRing {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [CommRing R] [AddCommMonoid ι] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) [SetLike.GradedMonoid A] :

CommRing { x : R // x ∈ A 0 }

The commutative ring A 0 inherited from R in the presence of SetLike.GradedMonoid A.

Equations

SetLike.GradeZero.instCommRing A = (SetLike.GradeZero.subring A).toCommRing

def SetLike.GradeZero.subalgebra {ι : Type u_1} {S : Type u_3} {R : Type u_4} [CommSemiring S] [Semiring R] [Algebra S R] [AddMonoid ι] (A : ι → Submodule S R) [SetLike.GradedMonoid A] :

The subalgebra A 0 of R.

Equations

SetLike.GradeZero.subalgebra A = { carrier := ↑(A 0), mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

Instances For

instance SetLike.GradeZero.instAlgebra {ι : Type u_1} {S : Type u_3} {R : Type u_4} [CommSemiring S] [Semiring R] [Algebra S R] [AddMonoid ι] (A : ι → Submodule S R) [SetLike.GradedMonoid A] :

Algebra S { x : R // x ∈ A 0 }

The S-algebra A 0 inherited from R in the presence of SetLike.GradedMonoid A.

Equations

SetLike.GradeZero.instAlgebra A = inferInstanceAs (Algebra S { x : R // x ∈ SetLike.GradeZero.subalgebra A })

@[simp]

theorem SetLike.GradeZero.coe_algebraMap {ι : Type u_1} {S : Type u_3} {R : Type u_4} [CommSemiring S] [Semiring R] [Algebra S R] [AddMonoid ι] (A : ι → Submodule S R) [SetLike.GradedMonoid A] (s : S) :

↑((algebraMap S { x : R // x ∈ A 0 }) s) = (algebraMap S R) s

theorem SetLike.homogeneous_zero_submodule {ι : Type u_1} {S : Type u_3} {R : Type u_4} [Zero ι] [Semiring S] [AddCommMonoid R] [Module S R] (A : ι → Submodule S R) :

SetLike.Homogeneous A 0

theorem SetLike.Homogeneous.smul {ι : Type u_1} {S : Type u_3} {R : Type u_4} [CommSemiring S] [Semiring R] [Algebra S R] {A : ι → Submodule S R} {s : S} {r : R} (hr : SetLike.Homogeneous A r) :

SetLike.Homogeneous A (s • r)