English
The application of GradedAlgebra.ι to m matches the componentwise embedding into the direct sum graded by parity.
Русский
Применение GradedAlgebra.ι к m совпадает с вложением в прямую сумму, градуируемую по чётности.
LaTeX
$$GradedAlgebra.ι Q m = DirectSum.of(…) 1 ⟨ι Q m, ι_mem_evenOdd_one Q m⟩$$
Lean4
theorem iSup_ι_range_eq_top : ⨆ i : ℕ, LinearMap.range (ι Q) ^ i = ⊤ :=
by
rw [← (DirectSum.Decomposition.isInternal (evenOdd Q)).submodule_iSup_eq_top, eq_comm]
calc
-- Porting note: needs extra annotations, no longer unifies against the goal in the face of
-- ambiguity
⨆ (i : ZMod 2) (j : { n : ℕ // ↑n = i }), LinearMap.range (ι Q) ^ (j : ℕ) =
⨆ i : Σ i : ZMod 2, { n : ℕ // ↑n = i }, LinearMap.range (ι Q) ^ (i.2 : ℕ) :=
by rw [iSup_sigma]
_ = ⨆ i : ℕ, LinearMap.range (ι Q) ^ i :=
Function.Surjective.iSup_congr (fun i => i.2) (fun i => ⟨⟨_, i, rfl⟩, rfl⟩) fun _ => rfl
