def twisting {ι : Type u_1} {τ : Type u_5} [AddCommGroup ι] (𝒬 : ι → τ) (c i : ι) : τ

Equations

• 𝒬⸨c⸩ i = 𝒬 (c + i)

def «term_⸨_⸩» : Lean.TrailingParserDescr

Equations

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

instance instGradedSMulTwisting {ι : Type u_1} {A : Type u_2} {Q : Type u_3} {σ : Type u_4} {τ : Type u_5} [AddCommGroup ι] [CommRing A] [AddCommGroup Q] [SetLike σ A] [SetLike τ Q] (𝒜 : ι → σ) (𝒬 : ι → τ) [Module A Q] [SetLike.GradedSMul 𝒜 𝒬] (c : ι) : SetLike.GradedSMul 𝒜 𝒬⸨c⸩

noncomputable instance instGmoduleSubtypeMemTwisting {ι : Type u_1} {A : Type u_2} {Q : Type u_3} {σ : Type u_4} {τ : Type u_5} [AddCommGroup ι] [CommRing A] [AddCommGroup Q] [SetLike σ A] [SetLike τ Q] (𝒜 : ι → σ) (𝒬 : ι → τ) [Module A Q] [DecidableEq ι] [AddSubgroupClass σ A] [AddSubmonoidClass τ Q] [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝒬] (c : ι) : DirectSum.Gmodule (fun (i : ι) => ↥(𝒜 i)) fun (i : ι) => ↥(𝒬⸨c⸩ i)

Equations

• instGmoduleSubtypeMemTwisting 𝒜 𝒬 c = DirectSum.Gmodule.mk ⋯ ⋯

noncomputable instance instModuleDirectSumSubtypeMemTwisting {ι : Type u_1} {A : Type u_2} {Q : Type u_3} {σ : Type u_4} {τ : Type u_5} [AddCommGroup ι] [CommRing A] [AddCommGroup Q] [SetLike σ A] [SetLike τ Q] (𝒜 : ι → σ) (𝒬 : ι → τ) [Module A Q] [DecidableEq ι] [AddSubgroupClass σ A] [AddSubmonoidClass τ Q] [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝒬] (c : ι) : Module (DirectSum ι fun (i : ι) => ↥(𝒜 i)) (DirectSum ι fun (i : ι) => ↥(𝒬⸨c⸩ i))

Equations

• instModuleDirectSumSubtypeMemTwisting 𝒜 𝒬 c = inferInstance

noncomputable instance twistingmodulestructure {ι : Type u_1} {A : Type u_2} {Q : Type u_3} {σ : Type u_4} {τ : Type u_5} [AddCommGroup ι] [CommRing A] [AddCommGroup Q] [SetLike σ A] [SetLike τ Q] (𝒜 : ι → σ) (𝒬 : ι → τ) [Module A Q] [DecidableEq ι] [AddSubgroupClass σ A] [AddSubmonoidClass τ Q] [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝒬] (c : ι) : Module A (DirectSum ι fun (i : ι) => ↥(𝒬⸨c⸩ i))

Equations

• twistingmodulestructure 𝒜 𝒬 c = Module.compHom (DirectSum ι fun (i : ι) => ↥(𝒬⸨c⸩ i)) (DirectSum.decomposeRingEquiv 𝒜).toRingHom

noncomputable instance instGmoduleSubtypeMem_project {ι : Type u_1} {A : Type u_2} {Q : Type u_3} {σ : Type u_4} {τ : Type u_5} [AddCommGroup ι] [CommRing A] [AddCommGroup Q] [SetLike σ A] [SetLike τ Q] (𝒜 : ι → σ) (𝒬 : ι → τ) [Module A Q] [DecidableEq ι] [AddSubgroupClass σ A] [AddSubmonoidClass τ Q] [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝒬] : DirectSum.Gmodule (fun (i : ι) => ↥(𝒜 i)) fun (i : ι) => ↥(𝒬 i)

Equations

• instGmoduleSubtypeMem_project 𝒜 𝒬 = DirectSum.Gmodule.mk ⋯ ⋯

noncomputable instance modulestructure {ι : Type u_1} {A : Type u_2} {Q : Type u_3} {σ : Type u_4} {τ : Type u_5} [AddCommGroup ι] [CommRing A] [AddCommGroup Q] [SetLike σ A] [SetLike τ Q] (𝒜 : ι → σ) (𝒬 : ι → τ) [Module A Q] [DecidableEq ι] [AddSubgroupClass σ A] [AddSubmonoidClass τ Q] [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝒬] : Module A (DirectSum ι fun (i : ι) => ↥(𝒬 i))

Equations

• modulestructure 𝒜 𝒬 = Module.compHom (DirectSum ι fun (i : ι) => ↥(𝒬 i)) (DirectSum.decomposeRingEquiv 𝒜).toRingHom

def maptwistingshift {ι : Type u_1} {Q : Type u_3} {τ : Type u_5} [AddCommGroup ι] [AddCommGroup Q] [SetLike τ Q] (𝒬 : ι → τ) [DecidableEq ι] [AddSubmonoidClass τ Q] (c : ι) : (DirectSum ι fun (i : ι) => ↥(𝒬 i)) →+ DirectSum ι fun (i : ι) => ↥(𝒬⸨c⸩ i)

Equations

• maptwistingshift 𝒬 c = DirectSum.toAddMonoid fun (i : ι) => { toFun := fun (qi : ↥(𝒬 i)) => (DirectSum.of (fun (i : ι) => ↥(𝒬⸨c⸩ i)) (i - c)) ⟨↑qi, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

def maptwisting {ι : Type u_1} {Q : Type u_3} {τ : Type u_5} [AddCommGroup ι] [AddCommGroup Q] [SetLike τ Q] (𝒬 : ι → τ) [DecidableEq ι] [AddSubmonoidClass τ Q] [DirectSum.Decomposition 𝒬] (c : ι) : Q →+ DirectSum ι fun (i : ι) => ↥(𝒬⸨c⸩ i)

Equations

• maptwisting 𝒬 c = (maptwistingshift 𝒬 c).comp (DirectSum.decomposeAddEquiv 𝒬).toAddMonoidHom

instance instDecompositionTwisting {ι : Type u_1} {Q : Type u_3} {τ : Type u_5} [AddCommGroup ι] [AddCommGroup Q] [SetLike τ Q] (𝒬 : ι → τ) [DecidableEq ι] [AddSubmonoidClass τ Q] [DirectSum.Decomposition 𝒬] (c : ι) : DirectSum.Decomposition 𝒬⸨c⸩

Equations

• instDecompositionTwisting 𝒬 c = { decompose' := ⇑(maptwisting 𝒬 c), left_inv := ⋯, right_inv := ⋯ }