TensorPower.gradedMonoid_eq_of_cast
theorem TensorPower.gradedMonoid_eq_of_cast :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{a b : GradedMonoid fun n => PiTensorProduct R fun x => M} (h : a.fst = b.fst),
(TensorPower.cast R M h) a.snd = b.snd → a = b
The theorem `TensorPower.gradedMonoid_eq_of_cast` states that for any commutative semiring `R` and any additive commutative monoid `M` that is also an `R`-module, if we have two elements `a` and `b` of a graded monoid (which is defined as a sigma type over a family of types indexed by some type `ι`), where each element of the graded monoid is a Pi tensor product for a given `n`, then if the first elements (`fst`) of `a` and `b` are equal, and if the second elements (`snd`) of `a` and `b` are related by a certain `TensorPower.cast`, then `a` and `b` are equal. The `TensorPower.cast` is a function that casts between "equal" tensor powers, according to some proof of equality `h`, which is given as a parameter to the function.
More concisely: Given a commutative semiring `R`, an additive commutative monoid `M` that is an `R`-module, and elements `a` and `b` of their corresponding graded monoids with equal first components, if the second components of `a` and `b` are related by `TensorPower.cast` with some proof `h`, then `a` and `b` are equal.
|
PiTensorProduct.gradedMonoid_eq_of_reindex_cast
theorem PiTensorProduct.gradedMonoid_eq_of_reindex_cast :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{ιι : Type u_3} {ι : ιι → Type u_4} {a b : GradedMonoid fun ii => PiTensorProduct R fun x => M}
(h : a.fst = b.fst), (PiTensorProduct.reindex R (fun x => M) (Equiv.cast ⋯)) a.snd = b.snd → a = b
This theorem states that given two dependent pairs of tensor products, if their index is the same and the contents are the same after applying a specific re-indexing operation (which is the canonical re-indexing operation using equivalence cast), then these two dependent pairs of tensor products are identical. The specifics are as follows: for a given commutative semiring `R`, an additive commutative monoid `M` that is a `R`-module, a type `ιι`, and a function `ι` that assigns to each element of `ιι` a type, if we have `a` and `b` which are elements of the graded monoid of the pi tensor product of `M` indexed by `ι`, then if the first component of `a` and `b` are equal and the second components of `a` and `b`, after re-indexing and applying an equivalence cast, are also equal, then `a` and `b` are identical.
More concisely: Given two dependent pairs of tensor products over a commutative semiring and an additive commutative monoid, if their index types are equal and their contents are equal after canonical re-indexing, then they are identical.
|