English
Let S be a Dedekind domain and P a prime ideal with P ≠ ⊥. Then cardQuot(P^i) = cardQuot(P)^i for all i ∈ ℕ.
Русский
Пусть S — область Дедекнда, P — простой идеал. Тогда для каждого i ∈ ℕ выполняется cardQuot(P^i) = cardQuot(P)^i.
LaTeX
$$$[\\text{IsDedekindDomain } S]\\; (hP : P \\neq \\bottom) \\rightarrow \\forall i\\in\\mathbb{N},\\; \\operatorname{cardQuot}(P^i) = \\operatorname{cardQuot}(P)^i$$$
Lean4
/-- Multiplicity of the ideal norm, for powers of prime ideals. -/
theorem cardQuot_pow_of_prime [IsDedekindDomain S] (hP : P ≠ ⊥) {i : ℕ} : cardQuot (P ^ i) = cardQuot P ^ i :=
by
induction i with
| zero => simp
| succ i ih => ?_
have : P ^ (i + 1) < P ^ i := Ideal.pow_succ_lt_pow hP i
suffices hquot : map (P ^ i.succ).mkQ (P ^ i) ≃ S ⧸ P by
rw [pow_succ' (cardQuot P), ← ih, cardQuot_apply (P ^ i.succ), ←
card_quotient_mul_card_quotient (P ^ i) (P ^ i.succ) this.le, cardQuot_apply (P ^ i), cardQuot_apply P,
Nat.card_congr hquot]
choose a a_mem a_notMem using SetLike.exists_of_lt this
choose f g hg hf using fun c (hc : c ∈ P ^ i) => Ideal.exists_mul_add_mem_pow_succ hP a c a_mem a_notMem hc
choose k hk_mem hk_eq using fun c' (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)) => Submodule.mem_map.mp hc'
refine Equiv.ofBijective (fun c' => Quotient.mk'' (f (k c' c'.prop) (hk_mem c' c'.prop))) ⟨?_, ?_⟩
· rintro ⟨c₁', hc₁'⟩ ⟨c₂', hc₂'⟩ h
rw [Subtype.mk_eq_mk, ← hk_eq _ hc₁', ← hk_eq _ hc₂', mkQ_apply, mkQ_apply, Submodule.Quotient.eq, ←
hf _ (hk_mem _ hc₁'), ← hf _ (hk_mem _ hc₂')]
refine Ideal.mul_add_mem_pow_succ_inj _ _ _ _ _ _ a_mem (hg _ _) (hg _ _) ?_
simpa only [Submodule.Quotient.mk''_eq_mk, Submodule.Quotient.mk''_eq_mk, Submodule.Quotient.eq] using h
· intro d'
refine Quotient.inductionOn' d' fun d => ?_
have hd' := (mem_map (f := mkQ (P ^ i.succ))).mpr ⟨a * d, Ideal.mul_mem_right d _ a_mem, rfl⟩
refine ⟨⟨_, hd'⟩, ?_⟩
simp only [Submodule.Quotient.mk''_eq_mk, Ideal.Quotient.mk_eq_mk, Ideal.Quotient.eq]
refine Ideal.mul_add_mem_pow_succ_unique hP a _ _ _ _ a_notMem (hg _ (hk_mem _ hd')) (zero_mem _) ?_
rw [hf, add_zero]
exact (Submodule.Quotient.eq _).mp (hk_eq _ hd')
