finite_setOf_absNorm_eq — Mathlib

English

For any n, the set of ideals I with absNorm(I) = n is finite (noetherian finiteness phenomenon in a Dedekind domain).

Русский

Для любого n множество идеалов I с absNorm(I) = n конечно (конечность выпуклого класса в области Дедекепа).

LaTeX

$$$$\forall n\in \mathbb{N},\; \{ I\in \mathrm{Ideal}(S) \mid \operatorname{absNorm}(I)=n\} \text{finite}. $$$$

Lean4

theorem finite_setOf_absNorm_eq [CharZero S] (n : ℕ) : {I : Ideal S | Ideal.absNorm I = n}.Finite :=
  by
  obtain hn | hn := Nat.eq_zero_or_pos n
  · simp only [hn, absNorm_eq_zero_iff, Set.setOf_eq_eq_singleton, Set.finite_singleton]
  · let f := fun I : Ideal S => Ideal.map (Ideal.Quotient.mk (@Ideal.span S _ {↑n})) I
    refine Set.Finite.of_finite_image (f := f) ?_ ?_
    · suffices Finite (S ⧸ @Ideal.span S _ {↑n})
        by
        let g := ((↑) : Ideal (S ⧸ @Ideal.span S _ {↑n}) → Set (S ⧸ @Ideal.span S _ {↑n}))
        refine Set.Finite.of_finite_image (f := g) ?_ SetLike.coe_injective.injOn
        exact Set.Finite.subset Set.finite_univ (Set.subset_univ _)
      rw [← absNorm_ne_zero_iff, absNorm_span_singleton]
      simpa only [Ne, Int.natAbs_eq_zero, Algebra.norm_eq_zero_iff, Nat.cast_eq_zero] using ne_of_gt hn
    · intro I hI J hJ h
      rw [← comap_map_mk (span_singleton_absNorm_le I), ← hI.symm, ← comap_map_mk (span_singleton_absNorm_le J), ←
        hJ.symm]
      congr

Похожие утверждения