smoothLocus_eq_compl_support_inter

English

For EssFiniteType algebras, the smooth locus equals the intersection of the complement of the support of the H1Cotangent module and the free locus of the Kaehler differential module.

Русский

Для алгебр EssFiniteType гладкий локус равен пересечению комплемента поддержки модуля H1Cotangent и свободного локуса Kaehler различности.

LaTeX

$$$\mathrm{smoothLocus}(R,A) = \Big(\mathrm{Module.support}(A, \mathrm{H1Cotangent}(R,A))\Big)^{c} \cap \mathrm{Module.freeLocus}(A, \Omega_{A/R})$$$

Lean4

theorem smoothLocus_eq_compl_support_inter [EssFiniteType R A] :
    smoothLocus R A = (Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A Ω[A⁄R] :=
  by
  ext p
  simp only [Set.mem_inter_iff, Set.mem_compl_iff, Module.notMem_support_iff, Module.mem_freeLocus]
  refine Algebra.FormallySmooth.iff_subsingleton_and_projective.trans ?_
  congr! 1
  · have := IsLocalizedModule.iso p.asIdeal.primeCompl (H1Cotangent.map R R A (Localization.AtPrime p.asIdeal))
    exact this.subsingleton_congr.symm
  · trans Module.Free (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R]
    · have : EssFiniteType A (Localization.AtPrime p.asIdeal) := .of_isLocalization _ p.asIdeal.primeCompl
      have : EssFiniteType R (Localization.AtPrime p.asIdeal) := .comp _ A _
      exact ⟨fun _ ↦ Module.free_of_flat_of_isLocalRing, fun _ ↦ inferInstance⟩
    · have :=
        IsLocalizedModule.iso p.asIdeal.primeCompl (KaehlerDifferential.map R R A (Localization.AtPrime p.asIdeal))
      have := this.extendScalarsOfIsLocalization p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal)
      exact ⟨fun H ↦ H.of_equiv' this.symm, fun H ↦ H.of_equiv' this⟩

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