chainsMap₃ — Mathlib

English

There is a level-2 chains map for f with φ, denoted chainsMap₂ f φ, giving a map between the 2-fold domain objects, compatible with φ and f.

Русский

Существуют отображения chainsMap₂ f φ на уровне пары элементов, дающие отображение между 2-разложениями и совместимы с φ и f.

LaTeX

$$$\mathrm{chainsMap}_2 f φ : \mathrm{ModuleCat.of}_k (G × G → A) \to \mathrm{ModuleCat.of}_k (H × H → B)$$$

Lean4

/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map sending `∑ aᵢ·(gᵢ₁, gᵢ₂, gᵢ₃) : G × G × G →₀ A` to
`∑ φ(aᵢ)·(f(gᵢ₁), f(gᵢ₂), f(gᵢ₃)) : H × H × H →₀ B`. -/
noncomputable abbrev chainsMap₃ : ModuleCat.of k (G × G × G →₀ A) ⟶ ModuleCat.of k (H × H × H →₀ B) :=
  ModuleCat.ofHom <| mapRange.linearMap φ.hom.hom ∘ₗ lmapDomain A k (Prod.map f (Prod.map f f))

Похожие утверждения