English
If we apply the lift to an element that is nontrivially supported in only the i-th component (Pi.single i x), the result is exactly the component-wise mapQ of the i-th map f_i applied to x, i.e., the i-th coordinate of the product is f_i(x) modulo p_i.
Русский
Если применить лифтинг к элементу, поддерживаемому только в i-м компоненте (Pi.single i x), то результат равен mapQ на этом компоненте, то есть i-й координатной части соответствует f_i(x) по модулю p_i.
LaTeX
$$$(\\pi\\text{-QuotientLift}\\ p\\ q\\ f\\ hf)(\\Pi_i\\,\\text{Quotient.mk}(x_i))$ на единичном элементе в позиции i равен $\\text{mapQ} _ {f_i} (x_i)$.$$
Lean4
@[simp]
theorem piQuotientLift_single [Fintype ι] [DecidableEq ι] (p : ∀ i, Submodule R (Ms i)) (q : Submodule R N)
(f : ∀ i, Ms i →ₗ[R] N) (hf : ∀ i, p i ≤ q.comap (f i)) (i) (x : Ms i ⧸ p i) :
piQuotientLift p q f hf (Pi.single i x) = mapQ _ _ (f i) (hf i) x :=
by
simp_rw [piQuotientLift, lsum_apply, sum_apply, comp_apply, proj_apply]
rw [Finset.sum_eq_single i]
· rw [Pi.single_eq_same]
· rintro j - hj
rw [Pi.single_eq_of_ne hj, map_zero]
· intros
have := Finset.mem_univ i
contradiction
