Documentation

Mathlib.Algebra.DirectSum.Ring

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

This module provides a set of heterogeneous typeclasses for defining a multiplicative structure over ⨁ i, A i such that (*) : A i → A j → A (i + j); that is to say, A forms an additively-graded ring. The typeclasses are:

Respectively, these imbue the external direct sum ⨁ i, A i with:

the base ring A 0 with:

and the ith grade A i with A 0-actions () defined as left-multiplication:

Note that in the presence of these instances, ⨁ i, A i itself inherits an A 0-action.

DirectSum.ofZeroRingHom : A 0 →+* ⨁ i, A i provides DirectSum.of A 0 as a ring homomorphism.

DirectSum.toSemiring extends DirectSum.toAddMonoid to produce a RingHom.

Direct sums of subobjects #

Additionally, this module provides helper functions to construct GSemiring and GCommSemiring instances for:

If CompleteLattice.independent (Set.range A), these provide a gradation of ⨆ i, A i, and the mapping ⨁ i, A i →+ ⨆ i, A i can be obtained as DirectSum.toMonoid (fun i ↦ AddSubmonoid.inclusion <| le_iSup A i).

Tags #

graded ring, filtered ring, direct sum, add_submonoid

Typeclasses #

class DirectSum.GNonUnitalNonAssocSemiring {ι : Type u_1} (A : ιType u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] extends GradedMonoid.GMul :
Type (max u_1 u_2)

A graded version of NonUnitalNonAssocSemiring.

Instances
    class DirectSum.GSemiring {ι : Type u_1} (A : ιType u_2) [AddMonoid ι] [(i : ι) → AddCommMonoid (A i)] extends DirectSum.GNonUnitalNonAssocSemiring , GradedMonoid.GOne :
    Type (max u_1 u_2)

    A graded version of Semiring.

    Instances
      class DirectSum.GCommSemiring {ι : Type u_1} (A : ιType u_2) [AddCommMonoid ι] [(i : ι) → AddCommMonoid (A i)] extends DirectSum.GSemiring :
      Type (max u_1 u_2)

      A graded version of CommSemiring.

      Instances
        class DirectSum.GRing {ι : Type u_1} (A : ιType u_2) [AddMonoid ι] [(i : ι) → AddCommGroup (A i)] extends DirectSum.GSemiring :
        Type (max u_1 u_2)

        A graded version of Ring.

        Instances
          class DirectSum.GCommRing {ι : Type u_1} (A : ιType u_2) [AddCommMonoid ι] [(i : ι) → AddCommGroup (A i)] extends DirectSum.GRing :
          Type (max u_1 u_2)

          A graded version of CommRing.

          Instances
            theorem DirectSum.of_eq_of_gradedMonoid_eq {ι : Type u_1} [DecidableEq ι] {A : ιType u_2} [(i : ι) → AddCommMonoid (A i)] {i : ι} {j : ι} {a : A i} {b : A j} (h : GradedMonoid.mk i a = GradedMonoid.mk j b) :
            (DirectSum.of A i) a = (DirectSum.of A j) b

            Instances for ⨁ i, A i #

            instance DirectSum.instOneDirectSum {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [Zero ι] [GradedMonoid.GOne A] [(i : ι) → AddCommMonoid (A i)] :
            One (DirectSum ι fun (i : ι) => A i)
            Equations
            theorem DirectSum.one_def {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [Zero ι] [GradedMonoid.GOne A] [(i : ι) → AddCommMonoid (A i)] :
            1 = (DirectSum.of A 0) GradedMonoid.GOne.one
            @[simp]
            theorem DirectSum.gMulHom_apply_apply {ι : Type u_1} (A : ιType u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] [DirectSum.GNonUnitalNonAssocSemiring A] {i : ι} {j : ι} (a : A i) (b : A j) :
            def DirectSum.gMulHom {ι : Type u_1} (A : ιType u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] [DirectSum.GNonUnitalNonAssocSemiring A] {i : ι} {j : ι} :
            A i →+ A j →+ A (i + j)

            The piecewise multiplication from the Mul instance, as a bundled homomorphism.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def DirectSum.mulHom {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] [DirectSum.GNonUnitalNonAssocSemiring A] :
              (DirectSum ι fun (i : ι) => A i) →+ (DirectSum ι fun (i : ι) => A i) →+ DirectSum ι fun (i : ι) => A i

              The multiplication from the Mul instance, as a bundled homomorphism.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                instance DirectSum.instNonUnitalNonAssocSemiringDirectSum {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] [DirectSum.GNonUnitalNonAssocSemiring A] :
                NonUnitalNonAssocSemiring (DirectSum ι fun (i : ι) => A i)
                Equations
                theorem DirectSum.mulHom_apply {ι : Type u_1} [DecidableEq ι] {A : ιType u_2} [Add ι] [(i : ι) → AddCommMonoid (A i)] [DirectSum.GNonUnitalNonAssocSemiring A] (a : DirectSum ι fun (i : ι) => A i) (b : DirectSum ι fun (i : ι) => A i) :
                ((DirectSum.mulHom A) a) b = a * b
                theorem DirectSum.mulHom_of_of {ι : Type u_1} [DecidableEq ι] {A : ιType u_2} [Add ι] [(i : ι) → AddCommMonoid (A i)] [DirectSum.GNonUnitalNonAssocSemiring A] {i : ι} {j : ι} (a : A i) (b : A j) :
                theorem DirectSum.of_mul_of {ι : Type u_1} [DecidableEq ι] {A : ιType u_2} [Add ι] [(i : ι) → AddCommMonoid (A i)] [DirectSum.GNonUnitalNonAssocSemiring A] {i : ι} {j : ι} (a : A i) (b : A j) :
                instance DirectSum.semiring {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] :
                Semiring (DirectSum ι fun (i : ι) => A i)

                The Semiring structure derived from GSemiring A.

                Equations
                theorem DirectSum.ofPow {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] {i : ι} (a : A i) (n : ) :
                theorem DirectSum.ofList_dProd {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] {α : Type u_3} (l : List α) (fι : αι) (fA : (a : α) → A ( a)) :
                (DirectSum.of A (List.dProdIndex l )) (List.dProd l fA) = List.prod (List.map (fun (a : α) => (DirectSum.of A ( a)) (fA a)) l)
                theorem DirectSum.list_prod_ofFn_of_eq_dProd {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] (n : ) (fι : Fin nι) (fA : (a : Fin n) → A ( a)) :
                List.prod (List.ofFn fun (a : Fin n) => (DirectSum.of A ( a)) (fA a)) = (DirectSum.of A (List.dProdIndex (List.finRange n) )) (List.dProd (List.finRange n) fA)
                theorem DirectSum.mul_eq_dfinsupp_sum {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [(i : ι) → (x : A i) → Decidable (x 0)] (a : DirectSum ι fun (i : ι) => A i) (a' : DirectSum ι fun (i : ι) => A i) :
                a * a' = DFinsupp.sum a fun (i : ι) (ai : (fun (i : ι) => A i) i) => DFinsupp.sum a' fun (j : ι) (aj : (fun (i : ι) => A i) j) => (DirectSum.of A (i + j)) (GradedMonoid.GMul.mul ai aj)
                theorem DirectSum.mul_eq_sum_support_ghas_mul {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [(i : ι) → (x : A i) → Decidable (x 0)] (a : DirectSum ι fun (i : ι) => A i) (a' : DirectSum ι fun (i : ι) => A i) :
                a * a' = Finset.sum (DFinsupp.support a ×ˢ DFinsupp.support a') fun (ij : ι × ι) => (DirectSum.of (fun (i : ι) => A i) (ij.1 + ij.2)) (GradedMonoid.GMul.mul (a ij.1) (a' ij.2))

                A heavily unfolded version of the definition of multiplication

                instance DirectSum.commSemiring {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddCommMonoid ι] [DirectSum.GCommSemiring A] :
                CommSemiring (DirectSum ι fun (i : ι) => A i)

                The CommSemiring structure derived from GCommSemiring A.

                Equations
                instance DirectSum.nonAssocRing {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [Add ι] [DirectSum.GNonUnitalNonAssocSemiring A] :
                NonUnitalNonAssocRing (DirectSum ι fun (i : ι) => A i)

                The Ring derived from GSemiring A.

                Equations
                instance DirectSum.ring {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [AddMonoid ι] [DirectSum.GRing A] :
                Ring (DirectSum ι fun (i : ι) => A i)

                The Ring derived from GSemiring A.

                Equations
                instance DirectSum.commRing {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [AddCommMonoid ι] [DirectSum.GCommRing A] :
                CommRing (DirectSum ι fun (i : ι) => A i)

                The CommRing derived from GCommSemiring A.

                Equations

                Instances for A 0 #

                The various G* instances are enough to promote the AddCommMonoid (A 0) structure to various types of multiplicative structure.

                @[simp]
                theorem DirectSum.of_zero_one {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [Zero ι] [GradedMonoid.GOne A] [(i : ι) → AddCommMonoid (A i)] :
                (DirectSum.of A 0) 1 = 1
                @[simp]
                theorem DirectSum.of_zero_smul {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [AddZeroClass ι] [(i : ι) → AddCommMonoid (A i)] [DirectSum.GNonUnitalNonAssocSemiring A] {i : ι} (a : A 0) (b : A i) :
                (DirectSum.of A i) (a b) = (DirectSum.of A 0) a * (DirectSum.of A i) b
                @[simp]
                theorem DirectSum.of_zero_mul {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [AddZeroClass ι] [(i : ι) → AddCommMonoid (A i)] [DirectSum.GNonUnitalNonAssocSemiring A] (a : A 0) (b : A 0) :
                (DirectSum.of A 0) (a * b) = (DirectSum.of A 0) a * (DirectSum.of A 0) b
                @[simp]
                theorem DirectSum.of_zero_pow {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] (a : A 0) (n : ) :
                (DirectSum.of A 0) (a ^ n) = (DirectSum.of A 0) a ^ n
                instance DirectSum.instNatCastOfNatToOfNat0ToZero {ι : Type u_1} (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] :
                NatCast (A 0)
                Equations
                @[simp]
                theorem DirectSum.of_natCast {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] (n : ) :
                (DirectSum.of A 0) n = n
                @[simp]
                theorem DirectSum.of_zero_ofNat {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] (n : ) [Nat.AtLeastTwo n] :
                instance DirectSum.GradeZero.semiring {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] :
                Semiring (A 0)

                The Semiring structure derived from GSemiring A.

                Equations
                def DirectSum.ofZeroRingHom {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] :
                A 0 →+* DirectSum ι fun (i : ι) => A i

                of A 0 is a RingHom, using the DirectSum.GradeZero.semiring structure.

                Equations
                • DirectSum.ofZeroRingHom A = let __src := DirectSum.of A 0; { toMonoidHom := { toOneHom := { toFun := __src.toFun, map_one' := }, map_mul' := }, map_zero' := , map_add' := }
                Instances For
                  instance DirectSum.GradeZero.module {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] {i : ι} :
                  Module (A 0) (A i)

                  Each grade A i derives an A 0-module structure from GSemiring A. Note that this results in an overall Module (A 0) (⨁ i, A i) structure via DirectSum.module.

                  Equations
                  instance DirectSum.GradeZero.commSemiring {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [AddCommMonoid ι] [DirectSum.GCommSemiring A] :

                  The CommSemiring structure derived from GCommSemiring A.

                  Equations
                  instance DirectSum.instIntCastOfNatToOfNat0ToZero {ι : Type u_1} (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [AddMonoid ι] [DirectSum.GRing A] :
                  IntCast (A 0)
                  Equations
                  @[simp]
                  theorem DirectSum.of_intCast {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [AddMonoid ι] [DirectSum.GRing A] (n : ) :
                  (DirectSum.of A 0) n = n
                  instance DirectSum.GradeZero.ring {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [AddMonoid ι] [DirectSum.GRing A] :
                  Ring (A 0)

                  The Ring derived from GSemiring A.

                  Equations
                  instance DirectSum.GradeZero.commRing {ι : Type u_1} [DecidableEq ι] (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [AddCommMonoid ι] [DirectSum.GCommRing A] :
                  CommRing (A 0)

                  The CommRing derived from GCommSemiring A.

                  Equations
                  theorem DirectSum.ringHom_ext' {ι : Type u_1} [DecidableEq ι] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [Semiring R] ⦃F : (DirectSum ι fun (i : ι) => A i) →+* R ⦃G : (DirectSum ι fun (i : ι) => A i) →+* R (h : ∀ (i : ι), AddMonoidHom.comp (F) (DirectSum.of A i) = AddMonoidHom.comp (G) (DirectSum.of A i)) :
                  F = G

                  If two ring homomorphisms from ⨁ i, A i are equal on each of A i y, then they are equal.

                  See note [partially-applied ext lemmas].

                  theorem DirectSum.ringHom_ext {ι : Type u_1} [DecidableEq ι] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [Semiring R] ⦃f : (DirectSum ι fun (i : ι) => A i) →+* R ⦃g : (DirectSum ι fun (i : ι) => A i) →+* R (h : ∀ (i : ι) (x : A i), f ((DirectSum.of A i) x) = g ((DirectSum.of A i) x)) :
                  f = g

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

                  @[simp]
                  theorem DirectSum.toSemiring_apply {ι : Type u_1} [DecidableEq ι] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [Semiring R] (f : (i : ι) → A i →+ R) (hone : (f 0) GradedMonoid.GOne.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) (a : DirectSum ι fun (i : ι) => A i) :
                  def DirectSum.toSemiring {ι : Type u_1} [DecidableEq ι] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [Semiring R] (f : (i : ι) → A i →+ R) (hone : (f 0) GradedMonoid.GOne.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) :
                  (DirectSum ι fun (i : ι) => A i) →+* R

                  A family of AddMonoidHoms preserving DirectSum.One.one and DirectSum.Mul.mul describes a RingHoms on ⨁ i, A i. This is a stronger version of DirectSum.toMonoid.

                  Of particular interest is the case when A i are bundled subojects, f is the family of coercions such as AddSubmonoid.subtype (A i), and the [GSemiring A] structure originates from DirectSum.gsemiring.ofAddSubmonoids, in which case the proofs about GOne and GMul can be discharged by rfl.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem DirectSum.toSemiring_of {ι : Type u_1} [DecidableEq ι] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [Semiring R] (f : (i : ι) → A i →+ R) (hone : (f 0) GradedMonoid.GOne.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) (i : ι) (x : A i) :
                    (DirectSum.toSemiring f hone hmul) ((DirectSum.of (fun (i : ι) => A i) i) x) = (f i) x
                    @[simp]
                    theorem DirectSum.toSemiring_coe_addMonoidHom {ι : Type u_1} [DecidableEq ι] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [Semiring R] (f : (i : ι) → A i →+ R) (hone : (f 0) GradedMonoid.GOne.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) :
                    @[simp]
                    theorem DirectSum.liftRingHom_symm_apply_coe {ι : Type u_1} [DecidableEq ι] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [Semiring R] (F : (DirectSum ι fun (i : ι) => A i) →+* R) {i : ι} :
                    (DirectSum.liftRingHom.symm F) = AddMonoidHom.comp (F) (DirectSum.of A i)
                    @[simp]
                    theorem DirectSum.liftRingHom_apply {ι : Type u_1} [DecidableEq ι] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [Semiring R] (f : { f : {i : ι} → A i →+ R // f GradedMonoid.GOne.one = 1 ∀ {i j : ι} (ai : A i) (aj : A j), f (GradedMonoid.GMul.mul ai aj) = f ai * f aj }) :
                    DirectSum.liftRingHom f = DirectSum.toSemiring (fun (x : ι) => f)
                    def DirectSum.liftRingHom {ι : Type u_1} [DecidableEq ι] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [Semiring R] :
                    { f : {i : ι} → A i →+ R // f GradedMonoid.GOne.one = 1 ∀ {i j : ι} (ai : A i) (aj : A j), f (GradedMonoid.GMul.mul ai aj) = f ai * f aj } ((DirectSum ι fun (i : ι) => A i) →+* R)

                    Families of AddMonoidHoms preserving DirectSum.One.one and DirectSum.Mul.mul are isomorphic to RingHoms on ⨁ i, A i. This is a stronger version of DFinsupp.liftAddHom.

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

                      Concrete instances #

                      instance Semiring.directSumGSemiring (ι : Type u_1) {R : Type u_2} [AddMonoid ι] [Semiring R] :
                      DirectSum.GSemiring fun (x : ι) => R

                      A direct sum of copies of a Semiring inherits the multiplication structure.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      instance CommSemiring.directSumGCommSemiring (ι : Type u_1) {R : Type u_2} [AddCommMonoid ι] [CommSemiring R] :
                      DirectSum.GCommSemiring fun (x : ι) => R

                      A direct sum of copies of a CommSemiring inherits the commutative multiplication structure.

                      Equations