English
The quotient-range inclusion equates domains after factoring out ramification, giving an isomorphism between certain quotient domains and residue-fields quotients.
Русский
Квота-диапазон включения совпадает после разложения, образуя изоморфизм между соответствующими квартиентами и остаточными полями.
LaTeX
$$quotientRangePowQuotSuccInclusionEquiv p P i hi ≃ₗ[R/p] S/P$$
Lean4
/-- `S ⧸ P` embeds into the quotient by `P^(i+1) ⧸ P^e` as a subspace of `P^i ⧸ P^e`. -/
noncomputable def quotientToQuotientRangePowQuotSucc {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) :
S ⧸ P →ₗ[R ⧸ p] (P ^ i).map (Ideal.Quotient.mk (P ^ e)) ⧸ LinearMap.range (powQuotSuccInclusion p P i)
where
toFun := quotientToQuotientRangePowQuotSuccAux p P a_mem
map_add' := by
intro x y; refine Quotient.inductionOn' x fun x => Quotient.inductionOn' y fun y => ?_
simp only [Submodule.Quotient.mk''_eq_mk, ← Submodule.Quotient.mk_add, quotientToQuotientRangePowQuotSuccAux_mk,
mul_add]
exact congr_arg Submodule.Quotient.mk rfl
map_smul' := by
intro x y; refine Quotient.inductionOn' x fun x => Quotient.inductionOn' y fun y => ?_
simp only [Submodule.Quotient.mk''_eq_mk, RingHom.id_apply, quotientToQuotientRangePowQuotSuccAux_mk]
refine congr_arg Submodule.Quotient.mk ?_
ext
simp only [map_mul, Quotient.mk_eq_mk, Submodule.coe_smul_of_tower, Algebra.smul_def,
Quotient.algebraMap_quotient_pow_ramificationIdx]
ring
