height_le_of_krullDim_preimage_le

English

Let f be a lattice homomorphism from α to β, and suppose there exists a bound m on the Krull dimension of all preimages f⁻¹({x}) for x in β. Then for every x in α, the height satisfies height(x) ≤ (m+1)·height(f(x)) + m.

Русский

Пусть f — объёмий гомоморфизм решёток α → β и существует верхняя граница m для κрull Dim предобразов f⁻¹({x}) по всем x ∈ β. Тогда для любого x ∈ α высота satisfies height(x) ≤ (m+1)·height(f(x)) + m.

LaTeX

$$$\\forall x\\in\\alpha,\\; \\operatorname{height}(x) \\le (m+1)\\cdot \\operatorname{height}(f(x)) + m$ под условием, что $\\forall x\\in\\beta,\\; \\operatorname{krullDim}(f^{-1}\\{x\\}) \\le m$.$$

Lean4

theorem height_le_of_krullDim_preimage_le (x : α) : Order.height x ≤ (m + 1) * Order.height (f x) + m :=
  by
  generalize h' : Order.height (f x) = n
  cases n with
  | top => simp
  | coe n =>
    induction n using Nat.strong_induction_on generalizing x with
    | h n ih =>
      refine height_le_iff.mpr fun p hp ↦ le_of_not_gt fun h_len ↦ ?_
      let i : Fin (p.length + 1) := ⟨p.length - (m + 1), Nat.sub_lt_succ p.length _⟩
      suffices h'' : f (p i) < f x
        by
        obtain ⟨n', hn'⟩ : ∃ (n' : ℕ), n' = height (f (p i)) :=
          ENat.ne_top_iff_exists.mp ((height_mono h''.le).trans_lt (h' ▸ ENat.coe_lt_top _)).ne
        have h_lt : n' < n := ENat.coe_lt_coe.mp (h' ▸ hn' ▸ height_strictMono h'' (hn' ▸ ENat.coe_lt_top _))
        have := (length_le_height_last (p := p.take i)).trans <| ih n' h_lt (p i) hn'.symm
        rw [RelSeries.take_length, ENat.coe_sub, Nat.cast_add, Nat.cast_one, tsub_le_iff_right, add_assoc,
          add_comm _ (_ + 1), ← add_assoc, ← mul_add_one] at this
        refine not_lt_of_ge ?_ (h_len.trans_le this)
        gcongr
        rwa [← ENat.coe_one, ← ENat.coe_add, ENat.coe_le_coe]
      refine (f.monotone ((p.monotone (Fin.le_last _)).trans hp)).lt_of_not_ge fun h'' ↦ ?_
      let q' : LTSeries α := p.drop i
      let q : LTSeries (f ⁻¹' {f x}) :=
        ⟨q'.length, fun j ↦
          ⟨q' j,
            le_antisymm (f.monotone (le_trans (b := q'.last) (q'.monotone (Fin.le_last _)) (p.last_drop _ ▸ hp)))
              (le_trans (b := f q'.head) (p.head_drop _ ▸ h'') (f.monotone (q'.monotone (Fin.zero_le _))))⟩,
          fun i ↦ q'.step i⟩
      have := (LTSeries.length_le_krullDim q).trans (h (f x))
      simp only [RelSeries.drop_length, Nat.cast_le, tsub_le_iff_right, q', i, q] at this
      have : p.length > m := ENat.coe_lt_coe.mp ((le_add_left le_rfl).trans_lt h_len)
      cutsat

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