Module

CotangentFinite.lean

Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.CotangentFinite

4 declarations indexed from sourceView source ↗

Module documentation

Finite cotangent modules for special local purity

For a module-finite algebra over a Noetherian ring, both relative Kähler differentials and first cotangent homology are finite over the target. The second assertion does not require projectivity of the differential module: the target is Noetherian, so the kernel in a finite presentation of the cotangent complex is finite.

This supplies the finiteness needed to replace minimal points of either cotangent support by associated primes. No purity or support-vanishing hypothesis is used.

Imports4

Mathlib.RingTheory.Extension.Cotangent.Basic
Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.Spectrum.Prime.Module

Imported by2

theorem

image_comap_support_eq_support_of_finite

L35 ↗

EtaleFundamentalGroups.SpecialLocalPurity.image_comap_support_eq_support_of_finite

Documentation

Under a finite algebra, the support after restriction of scalars is exactly the image of the original support on prime spectra. The reverse inclusion uses that an integral map is closed on spectra.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u v

Lean source · statement

theorem image_comap_support_eq_support_of_finite
    {R : Type u} {S : Type v} {M : Type*}
    [CommRing R] [CommRing S] [Algebra R S]
    [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [Module.Finite R S] [Module.Finite S M] :
    PrimeSpectrum.comap (algebraMap R S) '' Module.support S M =
      Module.support R M

theorem

kaehlerDifferential_finite_of_finite_over_noetherian

L64 ↗

EtaleFundamentalGroups.SpecialLocalPurity.kaehlerDifferential_finite_of_finite_over_noetherian

Documentation

Relative Kähler differentials of a finite algebra over a Noetherian ring are finite over the target.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u v

Lean source · statement

theorem kaehlerDifferential_finite_of_finite_over_noetherian
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [Algebra R S] [IsNoetherianRing R] [Module.Finite R S] :
    Module.Finite S Ω[S⁄R]

theorem

h1Cotangent_finite_of_finite_over_noetherian

L74 ↗

EtaleFundamentalGroups.SpecialLocalPurity.h1Cotangent_finite_of_finite_over_noetherian

Documentation

First cotangent homology of a finite algebra over a Noetherian ring is finite over the target. No projectivity assumption on Ω[S⁄R] is needed.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u v

Lean source · statement

theorem h1Cotangent_finite_of_finite_over_noetherian
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [Algebra R S] [IsNoetherianRing R] [Module.Finite R S] :
    Module.Finite S (Algebra.H1Cotangent R S)

theorem

cotangent_minimalPrimes_subset_associatedPrimes_of_finite_over_noetherian

L91 ↗

EtaleFundamentalGroups.SpecialLocalPurity.cotangent_minimalPrimes_subset_associatedPrimes_of_finite_over_noetherian

Documentation

Minimal primes in the annihilators of the two cotangent modules are associated primes once the algebra is finite over a Noetherian base.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u v

Lean source · statement

theorem cotangent_minimalPrimes_subset_associatedPrimes_of_finite_over_noetherian
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [Algebra R S] [IsNoetherianRing R] [Module.Finite R S] :
    (Module.annihilator S Ω[S⁄R]).minimalPrimes ⊆
        associatedPrimes S Ω[S⁄R] ∧
      (Module.annihilator S (Algebra.H1Cotangent R S)).minimalPrimes ⊆
        associatedPrimes S (Algebra.H1Cotangent R S)

Module documentation

Finite cotangent modules for special local purity

Declarations

image_comap_support_eq_support_of_finite

kaehlerDifferential_finite_of_finite_over_noetherian

h1Cotangent_finite_of_finite_over_noetherian

cotangent_minimalPrimes_subset_associatedPrimes_of_finite_over_noetherian