English
The map powQuotSuccInclusion p P i is injective for every i, reflecting stability across successive quotient steps.
Русский
Отображение powQuotSuccInclusion инъективно для каждого i.
LaTeX
$$$\\\\operatorname{powQuotSuccInclusion} \\, p \\, P \\, i \\, \\text{ injective}$$$
Lean4
/-- `S ⧸ P` embeds into the quotient by `P^(i+1) ⧸ P^e` as a subspace of `P^i ⧸ P^e`.
See `quotientToQuotientRangePowQuotSucc` for this as a linear map,
and `quotientRangePowQuotSuccInclusionEquiv` for this as a linear equivalence.
-/
noncomputable def quotientToQuotientRangePowQuotSuccAux {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) :
S ⧸ P → (P ^ i).map (Ideal.Quotient.mk (P ^ e)) ⧸ LinearMap.range (powQuotSuccInclusion p P i) :=
Quotient.map' (fun x : S => ⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_right x _ a_mem)⟩) fun x y h =>
by
rw [Submodule.quotientRel_def] at h ⊢
simp only [map_mul, LinearMap.mem_range]
refine ⟨⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_mul a_mem h)⟩, ?_⟩
ext
rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Submodule.coe_sub, Subtype.coe_mk, Subtype.coe_mk, map_mul,
map_sub, mul_sub]
