summand_eq_zero_of_smul_invariant

English

If swapping σ by a transposition yields the same σ (i.e., σ is invariant under swap on v), then the summand vanishes.

Русский

Еслиswap не меняет σ на v, то соответствующий summand равен нулю.

LaTeX

$$$$\text{swap}(i,j)\cdot σ = σ \implies \text{domCoprod.summand}(a,b,σ)\,v = 0.$$$$

Lean4

/-- Swapping elements in `σ` with equal values in `v` result in zero if the swap has no effect
on the quotient. -/
theorem summand_eq_zero_of_smul_invariant (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Perm.ModSumCongr ιa ιb)
    {v : ιa ⊕ ιb → Mᵢ} {i j : ιa ⊕ ιb} (hv : v i = v j) (hij : i ≠ j) :
    swap i j • σ = σ → domCoprod.summand a b σ v = 0 :=
  by
  refine Quotient.inductionOn' σ fun σ => ?_
  dsimp only [Quotient.liftOn'_mk'', Quotient.map'_mk'', MultilinearMap.smul_apply, MultilinearMap.domDomCongr_apply,
    MultilinearMap.domCoprod_apply, domCoprod.summand]
  intro hσ
  obtain ⟨⟨sl, sr⟩, hσ⟩ := QuotientGroup.leftRel_apply.mp (Quotient.exact' hσ)
  rcases hi : σ⁻¹ i with i' | i' <;> rcases hj : σ⁻¹ j with j' | j' <;> rw [Perm.inv_eq_iff_eq] at hi hj <;>
    substs hi hj
  case inl.inr => simpa using Equiv.congr_fun hσ (Sum.inl i')
  case inr.inl =>
    simpa using
      Equiv.congr_fun hσ
        (Sum.inr i')
          -- the term does not pair but is zero

  case inl.inl =>
    suffices (a fun i ↦ v (σ (Sum.inl i))) = 0 by simp_all
    exact AlternatingMap.map_eq_zero_of_eq _ _ hv fun hij' => hij (hij' ▸ rfl)
  case inr.inr =>
    suffices (b fun i ↦ v (σ (Sum.inr i))) = 0 by simp_all
    exact b.map_eq_zero_of_eq _ hv fun hij' => hij (hij' ▸ rfl)

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