noncomputable def gradingOfInjection {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_4} [AddCommMonoid ι] [AddCommMonoid ι'] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) (ρ : ι →+ ι') [(i : ι') → Decidable (i ∈ Set.range ⇑ρ)] : ι' → Submodule R A

Equations

• gradingOfInjection 𝒜 ρ i = if mem : i ∈ Set.range ⇑ρ then 𝒜 (Set.rangeSplitting ⇑ρ ⟨i, mem⟩) else ⊥

instance gradingOfInjection_isGradedMonoid {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_4} [AddCommMonoid ι] [AddCommMonoid ι'] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [DecidableEq ι] [GradedAlgebra 𝒜] (ρ : ι →+ ι') (inj : Function.Injective ⇑ρ) [(i : ι') → Decidable (i ∈ Set.range ⇑ρ)] : SetLike.GradedMonoid (gradingOfInjection 𝒜 ρ)

noncomputable def decomposeOfInjectionAux {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_4} [AddCommMonoid ι] [AddCommMonoid ι'] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [DecidableEq ι] [GradedAlgebra 𝒜] (ρ : ι →+ ι') (inj : Function.Injective ⇑ρ) [(i : ι') → Decidable (i ∈ Set.range ⇑ρ)] [DecidableEq ι'] : (DirectSum ι fun (i : ι) => ↥(𝒜 i)) →+ DirectSum ι' fun (i : ι') => ↥(gradingOfInjection 𝒜 ρ i)

Equations

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

noncomputable instance gradingOfInjection_decomposition {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_4} [AddCommMonoid ι] [AddCommMonoid ι'] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [DecidableEq ι] [GradedAlgebra 𝒜] (ρ : ι →+ ι') (inj : Function.Injective ⇑ρ) [(i : ι') → Decidable (i ∈ Set.range ⇑ρ)] [DecidableEq ι'] : DirectSum.Decomposition (gradingOfInjection 𝒜 ρ)

Equations

• gradingOfInjection_decomposition 𝒜 ρ inj = { decompose' := ⇑(decomposeOfInjectionAux 𝒜 ρ inj) ∘ ⇑(DirectSum.decompose 𝒜), left_inv := ⋯, right_inv := ⋯ }

noncomputable instance gradingOfInjection_isGradedAlgebra {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_4} [AddCommMonoid ι] [AddCommMonoid ι'] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [DecidableEq ι] [GradedAlgebra 𝒜] (ρ : ι →+ ι') (inj : Function.Injective ⇑ρ) [(i : ι') → Decidable (i ∈ Set.range ⇑ρ)] [DecidableEq ι'] : GradedAlgebra (gradingOfInjection 𝒜 ρ)

Equations

• gradingOfInjection_isGradedAlgebra 𝒜 ρ inj = GradedRing.mk

noncomputable def ρNatToInt (ι : Type u_1) : (ι →₀ ℕ) →+ ι →₀ ℤ

Equations

• ρNatToInt ι = { toFun := fun (v : ι →₀ ℕ) => Finsupp.mapRange Int.ofNat ρNatToInt.proof_1 v, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem ρNatToInt_apply (ι : Type u_1) (v : ι →₀ ℕ) : (ρNatToInt ι) v = Finsupp.mapRange Int.ofNat ρNatToInt.proof_1 v

theorem ρNatToInt_inj {ι : Type u_1} : Function.Injective ⇑(ρNatToInt ι)