ker_fg_of_mvPolynomial — Mathlib

English

This lemma shows the FG property of the kernel for a surjective mvPolynomial map f, assuming A is finitely presented.

Русский

Лемма демонстрирует FG-свойство ядра отображения mvPolynomial, если A имеет конечную презентацию.

LaTeX

$$$\\forall f : \\mathrm{MvPolynomial} (\\mathrm{Fin } n) R \\to A,\\; f\\text{ surjective} \\Rightarrow (\\ker f).FG$$$

Lean4

/-- This is used to prove the strictly stronger `ker_fg_of_surjective`. Use it instead. -/
theorem ker_fg_of_mvPolynomial {n : ℕ} (f : MvPolynomial (Fin n) R →ₐ[R] A) (hf : Function.Surjective f)
    [FinitePresentation R A] : (RingHom.ker f.toRingHom).FG := by
  classical
  obtain ⟨m, f', hf', s, hs⟩ := FinitePresentation.out (R := R) (A := A)
  let RXn := MvPolynomial (Fin n) R
  let RXm := MvPolynomial (Fin m) R
  have := fun i : Fin n => hf' (f <| X i)
  choose g hg using this
  have := fun i : Fin m => hf (f' <| X i)
  choose h hh using this
  let aeval_h : RXm →ₐ[R] RXn := aeval h
  let g' : Fin n → RXn := fun i => X i - aeval_h (g i)
  refine ⟨Finset.univ.image g' ∪ s.image aeval_h, ?_⟩
  simp only [Finset.coe_image, Finset.coe_union, Finset.coe_univ, Set.image_univ]
  have hh' : ∀ x, f (aeval_h x) = f' x := by
    intro x
    rw [← f.coe_toRingHom, map_aeval]
    simp_rw [AlgHom.coe_toRingHom, hh]
    rw [AlgHom.comp_algebraMap, ← aeval_eq_eval₂Hom,
      -- Porting note: added line below
      ← funext fun i => Function.comp_apply (f := ↑f') (g := MvPolynomial.X), ← aeval_unique]
  let s' := Set.range g' ∪ aeval_h '' s
  have leI : Ideal.span s' ≤ RingHom.ker f.toRingHom :=
    by
    rw [Ideal.span_le]
    rintro _ (⟨i, rfl⟩ | ⟨x, hx, rfl⟩)
    · change f (g' i) = 0
      rw [map_sub, ← hg, hh', sub_self]
    · change f (aeval_h x) = 0
      rw [hh']
      change x ∈ RingHom.ker f'.toRingHom
      rw [← hs]
      exact Ideal.subset_span hx
  apply leI.antisymm
  intro x hx
  have : x ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid :=
    by
    have : x ∈ adjoin R (Set.range X : Set RXn) := by
      rw [adjoin_range_X]
      trivial
    refine adjoin_induction ?_ ?_ ?_ ?_ this
    · rintro _ ⟨i, rfl⟩
      rw [← sub_add_cancel (X i) (aeval h (g i)), add_comm]
      apply AddSubmonoid.add_mem_sup
      · exact Set.mem_range_self _
      · apply Submodule.subset_span
        apply Set.mem_union_left
        exact Set.mem_range_self _
    · intro r
      apply AddSubmonoid.mem_sup_left
      exact ⟨C r, aeval_C _ _⟩
    · intro _ _ _ _ h₁ h₂
      exact add_mem h₁ h₂
    · intro p₁ p₂ _ _ h₁ h₂
      obtain ⟨_, ⟨x₁, rfl⟩, y₁, hy₁, rfl⟩ := AddSubmonoid.mem_sup.mp h₁
      obtain ⟨_, ⟨x₂, rfl⟩, y₂, hy₂, rfl⟩ := AddSubmonoid.mem_sup.mp h₂
      rw [mul_add, add_mul, add_assoc, ← map_mul]
      apply AddSubmonoid.add_mem_sup
      · exact Set.mem_range_self _
      · exact add_mem (Ideal.mul_mem_right _ _ hy₁) (Ideal.mul_mem_left _ _ hy₂)
  obtain ⟨_, ⟨x, rfl⟩, y, hy, rfl⟩ := AddSubmonoid.mem_sup.mp this
  refine add_mem ?_ hy
  simp only [RXn, RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, map_add, show f y = 0 from leI hy,
    add_zero, hh'] at hx
  suffices Ideal.span (s : Set RXm) ≤ (Ideal.span s').comap aeval_h
    by
    apply this
    rwa [hs]
  rw [Ideal.span_le]
  intro x hx
  apply Submodule.subset_span
  apply Set.mem_union_right
  exact Set.mem_image_of_mem _ hx

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