English
In a Dedekind domain setting, surjectivity of the range map persists along the ramification range, enabling a closed image description for quotient constructions.
Русский
В условиях Дедекиндового кольца суръекция образа сохраняется вдоль диапазона разветвления, что позволяет описать изображение квотиетных конструкторов.
LaTeX
$$quotientToQuotientRangePowQuotSucc_surjective p P hP hi a_mem a_notMem$$
Lean4
theorem quotientToQuotientRangePowQuotSucc_surjective [IsDedekindDomain S] (hP0 : P ≠ ⊥) [hP : P.IsPrime] {i : ℕ}
(hi : i < e) {a : S} (a_mem : a ∈ P ^ i) (a_notMem : a ∉ P ^ (i + 1)) :
Function.Surjective (quotientToQuotientRangePowQuotSucc p P a_mem) :=
by
rintro ⟨⟨⟨x⟩, hx⟩⟩
have Pe_le_Pi : P ^ e ≤ P ^ i := Ideal.pow_le_pow_right hi.le
rw [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, Ideal.mem_quotient_iff_mem_sup,
sup_eq_left.mpr Pe_le_Pi] at hx
suffices hx' : x ∈ Ideal.span { a } ⊔ P ^ (i + 1)
by
obtain ⟨y', hy', z, hz, rfl⟩ := Submodule.mem_sup.mp hx'
obtain ⟨y, rfl⟩ := Ideal.mem_span_singleton.mp hy'
refine ⟨Submodule.Quotient.mk y, ?_⟩
simp only [Submodule.Quotient.quot_mk_eq_mk, quotientToQuotientRangePowQuotSucc_mk, Submodule.Quotient.eq,
LinearMap.mem_range, Subtype.ext_iff, Submodule.coe_sub]
refine ⟨⟨_, Ideal.mem_map_of_mem _ (Submodule.neg_mem _ hz)⟩, ?_⟩
rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Ideal.Quotient.mk_eq_mk, map_add, sub_add_cancel_left, map_neg]
letI := Classical.decEq (Ideal S)
rw [sup_eq_prod_inf_factors _ (pow_ne_zero _ hP0), normalizedFactors_pow,
normalizedFactors_irreducible ((Ideal.prime_iff_isPrime hP0).mpr hP).irreducible, normalize_eq,
Multiset.nsmul_singleton, Multiset.inter_replicate, Multiset.prod_replicate]
· rw [← Submodule.span_singleton_le_iff_mem, Ideal.submodule_span_eq] at a_mem a_notMem
rwa [Ideal.count_normalizedFactors_eq a_mem a_notMem, min_eq_left i.le_succ]
· intro ha
rw [Ideal.span_singleton_eq_bot.mp ha] at a_notMem
have := (P ^ (i + 1)).zero_mem
contradiction
