ideal_fg — Mathlib

English

Let R and S be commutative rings with an R-algebra structure, and assume S is essentially of finite type over R. Then the Kaehler differential ideal (R,S) is finitely generated.

Русский

Пусть R и S — коммутативные кольца, есть структура алгебры R→S, и S является конечнопорождённым по отношению к R. Тогда идеал KaehlerDifferential(R,S) является конечно порождаемым.

LaTeX

$$$\\text{I} = \\mathrm{KaehlerDifferential.ideal}(R,S) \quad\\Rightarrow\\quad \\mathrm{I} = \\mathrm{span}\\{f_1,\\dots,f_n\\} \\text{ for some } n\\in\\mathbb{N}, f_i \\in S\\otimes_R S$$$

Lean4

theorem ideal_fg [EssFiniteType R S] : (KaehlerDifferential.ideal R S).FG := by
  classical
  use (EssFiniteType.finset R S).image (fun s ↦ (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S))
  apply le_antisymm
  · rw [Finset.coe_image, Ideal.span_le]
    rintro _ ⟨x, _, rfl⟩
    exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x
  · rw [← KaehlerDifferential.span_range_eq_ideal, Ideal.span_le]
    rintro _ ⟨x, rfl⟩
    let I : Ideal (S ⊗[R] S) :=
      Ideal.span ((EssFiniteType.finset R S).image (fun s ↦ (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)))
    change _ - _ ∈ I
    have :
      (IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeRight =
        (IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeLeft :=
      by
      apply EssFiniteType.algHom_ext
      intro a ha
      simp only [AlgHom.coe_comp, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq, Function.comp_apply,
        TensorProduct.includeLeft_apply, TensorProduct.includeRight_apply, Ideal.Quotient.mk_eq_mk_iff_sub_mem]
      refine Ideal.subset_span ?_
      simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe]
      exact ⟨a, ha, rfl⟩
    simpa [Ideal.Quotient.mk_eq_mk_iff_sub_mem] using AlgHom.congr_fun this x

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