noncomputable def TensorProduct.gradingByProduct {ιA : Type u_1} {ιB : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (𝒜 : ιA → Submodule R A) (ℬ : ιB → Submodule R B) : ιA × ιB → Submodule R (TensorProduct R A B)

Equations

• TensorProduct.gradingByProduct 𝒜 ℬ p = LinearMap.range (TensorProduct.map (𝒜 p.1).subtype (ℬ p.2).subtype)

def TensorProduct.«term_⊗__1» : Lean.TrailingParserDescr

Equations

• TensorProduct.«term_⊗__1» = Lean.ParserDescr.trailingNode `TensorProduct.«term_⊗__1» 10 11 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊗") (Lean.ParserDescr.cat `term 11))

instance TensorProduct.instGradedMonoidProdSubmoduleGradingByProduct {ιA : Type u_1} {ιB : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [DecidableEq ιA] [AddCommGroup ιA] [DecidableEq ιB] [AddCommGroup ιB] [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (𝒜 : ιA → Submodule R A) (ℬ : ιB → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : SetLike.GradedMonoid (TensorProduct.gradingByProduct 𝒜 ℬ)

noncomputable def TensorProduct.decompositionByProduct {ιA : Type u_1} {ιB : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [DecidableEq ιA] [AddCommGroup ιA] [DecidableEq ιB] [AddCommGroup ιB] [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (𝒜 : ιA → Submodule R A) (ℬ : ιB → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : TensorProduct R A B →ₗ[R] DirectSum (ιA × ιB) fun (p : ιA × ιB) => ↥(TensorProduct.gradingByProduct 𝒜 ℬ p)

Equations

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

@[simp]

theorem TensorProduct.decompositionByProduct_apply_tmul_homogeneous {ιA : Type u_1} {ιB : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [DecidableEq ιA] [AddCommGroup ιA] [DecidableEq ιB] [AddCommGroup ιB] [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (𝒜 : ιA → Submodule R A) (ℬ : ιB → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (a : A) (b : B) (i : ιA) (j : ιB) (ha : a ∈ 𝒜 i) (hb : b ∈ ℬ j) : (TensorProduct.decompositionByProduct 𝒜 ℬ) (a ⊗ₜ[R] b) = (DirectSum.lof R (ιA × ιB) (fun (p : ιA × ιB) => ↥(TensorProduct.gradingByProduct 𝒜 ℬ p)) (i, j)) ⟨(TensorProduct.map (𝒜 (i, j).1).subtype (ℬ (i, j).2).subtype) (⟨a, ha⟩ ⊗ₜ[R] ⟨b, hb⟩), ⋯⟩

noncomputable instance TensorProduct.instDecompositionProdSubmoduleGradingByProduct {ιA : Type u_1} {ιB : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [DecidableEq ιA] [AddCommGroup ιA] [DecidableEq ιB] [AddCommGroup ιB] [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (𝒜 : ιA → Submodule R A) (ℬ : ιB → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : DirectSum.Decomposition (TensorProduct.gradingByProduct 𝒜 ℬ)

Equations

• TensorProduct.instDecompositionProdSubmoduleGradingByProduct 𝒜 ℬ = { decompose' := ⇑(TensorProduct.decompositionByProduct 𝒜 ℬ), left_inv := ⋯, right_inv := ⋯ }

noncomputable instance TensorProduct.instGradedAlgebraProdGradingByProduct {ιA : Type u_1} {ιB : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [DecidableEq ιA] [AddCommGroup ιA] [DecidableEq ιB] [AddCommGroup ιB] [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (𝒜 : ιA → Submodule R A) (ℬ : ιB → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : GradedAlgebra (TensorProduct.gradingByProduct 𝒜 ℬ)

Equations

• TensorProduct.instGradedAlgebraProdGradingByProduct 𝒜 ℬ = GradedRing.mk

theorem TensorProduct.tmul_homogeneous {ιA : Type u_1} {ιB : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] {𝒜 : ιA → Submodule R A} {ℬ : ιB → Submodule R B} {a : A} {b : B} (ha : SetLike.Homogeneous 𝒜 a) (hb : SetLike.Homogeneous ℬ b) : SetLike.Homogeneous (TensorProduct.gradingByProduct 𝒜 ℬ) (a ⊗ₜ[R] b)

theorem TensorProduct.mem_degree_iff {ιA : Type u_1} {ιB : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] {𝒜 : ιA → Submodule R A} {ℬ : ιB → Submodule R B} {iA : ιA} {iB : ιB} (x : TensorProduct R A B) : x ∈ TensorProduct.gradingByProduct 𝒜 ℬ (iA, iB) ↔ ∃ (c : TensorProduct R ↥(𝒜 iA) ↥(ℬ iB) →₀ ↥(𝒜 iA) × ↥(ℬ iB)), x = ∑ i ∈ c.support, ↑(c i).1 ⊗ₜ[R] ↑(c i).2

theorem TensorProduct.tmul_elemIsRelevant {ιA : Type u_1} {ιB : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [DecidableEq ιA] [AddCommGroup ιA] [DecidableEq ιB] [AddCommGroup ιB] [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] {𝒜 : ιA → Submodule R A} {ℬ : ιB → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] {x : A} {y : B} {hom_x : SetLike.Homogeneous 𝒜 x} {hom_y : SetLike.Homogeneous ℬ y} (rel_x : HomogeneousSubmonoid.ElemIsRelevant x hom_x) (rel_y : HomogeneousSubmonoid.ElemIsRelevant y hom_y) : HomogeneousSubmonoid.ElemIsRelevant (x ⊗ₜ[R] y) ⋯

theorem TensorProduct.elemIsRelevant_of_exists {ιA : Type u_1} {ιB : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [DecidableEq ιA] [AddCommGroup ιA] [DecidableEq ιB] [AddCommGroup ιB] [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] {𝒜 : ιA → Submodule R A} {ℬ : ιB → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [AddGroup.FG ιA] [AddGroup.FG ιB] (x : TensorProduct R A B) (hom_x : SetLike.Homogeneous (TensorProduct.gradingByProduct 𝒜 ℬ) x) (rel_x : HomogeneousSubmonoid.ElemIsRelevant x hom_x) : ∃ (n : ℕ) (sA : Fin n → A) (sB : Fin n → B) (hom_sA : ∀ (i : Fin n), SetLike.Homogeneous 𝒜 (sA i)) (hom_sB : ∀ (i : Fin n), SetLike.Homogeneous ℬ (sB i)) (_ : ∀ (i : Fin n), HomogeneousSubmonoid.ElemIsRelevant (sA i) ⋯) (_ : ∀ (i : Fin n), HomogeneousSubmonoid.ElemIsRelevant (sB i) ⋯) (k : ℕ), x ^ k = ∑ i : Fin n, sA i ⊗ₜ[R] sB i

noncomputable def TensorProduct.dagger {ιA : Type u_1} {ιB : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [DecidableEq ιA] [AddCommGroup ιA] [DecidableEq ιB] [AddCommGroup ιB] [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (𝒜 : ιA → Submodule R A) (ℬ : ιB → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : Ideal (TensorProduct R A B)

Equations

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

theorem TensorProduct.rad_dagger {ιA : Type u_1} {ιB : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [DecidableEq ιA] [AddCommGroup ιA] [DecidableEq ιB] [AddCommGroup ιB] [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] {𝒜 : ιA → Submodule R A} {ℬ : ιB → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [AddGroup.FG ιA] [AddGroup.FG ιB] : (HomogeneousSubmonoid.dagger (TensorProduct.gradingByProduct 𝒜 ℬ)).toIdeal.radical = (TensorProduct.dagger 𝒜 ℬ).radical