English
For mk and hp, piQuotientEquiv applied to the mk homomorphism equals the mk on the target, reflecting the canonical lift.
Русский
Для mk и hp, применение piQuotientEquiv к mk‑гомоморфизму даёт mk на цели, что отражает канонический подъем.
LaTeX
$$$\\\\text{piQuotientEquiv} p hp (\\\\operatorname{Ideal.Quotient.mk} _ x) = (\\\\text{mk}) x$$$
Lean4
/-- **Chinese remainder theorem** for a ring of integers: if the prime ideal `p : Ideal R`
factors in `S` as `∏ i, P i ^ e i`,
then `S ⧸ I` factors `R ⧸ I`-linearly as `Π i, R ⧸ (P i ^ e i)`. -/
noncomputable def piQuotientLinearEquiv (p : Ideal R) (hp : map (algebraMap R S) p ≠ ⊥) :
(S ⧸ map (algebraMap R S) p) ≃ₗ[R ⧸ p]
∀ P : (factors (map (algebraMap R S) p)).toFinset, S ⧸ (P : Ideal S) ^ ramificationIdx (algebraMap R S) p P :=
{ Factors.piQuotientEquiv p hp with
map_smul' := by
rintro ⟨c⟩ ⟨x⟩; ext P
simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, Algebra.smul_def,
Quotient.algebraMap_quotient_map_quotient, Quotient.mk_algebraMap, RingHomCompTriple.comp_apply, Pi.mul_apply,
Pi.algebraMap_apply]
congr }
