@[reducible, inline]

abbrev CanonicalSheafDef.IsSmoothMorphismOfRelDim (n : ℕ) (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Prop

The property of being a standard smooth R-algebra of relative dimension n.

theorem CanonicalSheafDef.smooth_relDim_rank_kaehler (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [Nontrivial S] (n : ℕ) [Algebra.IsStandardSmoothOfRelativeDimension n R S] : Module.rank S Ω[S⁄R] = ↑n

If S is a standard smooth R-algebra of relative dimension n, then the module of Kähler differentials Ω[S⁄R] has rank n over S.

theorem CanonicalSheafDef.smooth_kaehler_free (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsStandardSmooth R S] : Module.Free S Ω[S⁄R]

For a standard smooth R-algebra S, the Kähler differential module Ω[S⁄R] is free.

class CanonicalSheafDef.IsSmoothOfDimension (k : Type u) (A : Type v) [CommRing k] [CommRing A] [Algebra k A] (d : ℕ) : Prop

An Algebra k A is smooth of dimension d when its module of Kähler differentials Ω[A⁄k] is free, finite, and has rank d over A.

• free : Module.Free A Ω[A⁄k]
• finite : Module.Finite A Ω[A⁄k]
• finrank_eq : Module.finrank A Ω[A⁄k] = d

noncomputable def CanonicalSheafDef.canonicalModule (k : Type u) (A : Type v) [CommRing k] [CommRing A] [Algebra k A] (d : ℕ) : Submodule A (ExteriorAlgebra A Ω[A⁄k])

The canonical module ω_X = ∧^d Ω_X (Def 37, Lec 19): the d-th exterior power of the module of Kähler differentials.

theorem CanonicalSheafDef.canonicalModule_free (k : Type u) (A : Type v) [CommRing k] [CommRing A] [Algebra k A] (d : ℕ) [h : IsSmoothOfDimension k A d] : Module.Free A ↥(canonicalModule k A d)

The canonical module of a smooth k-algebra of dimension d is free over A.

theorem CanonicalSheafDef.canonicalModule_finrank_eq_one (k : Type u) (A : Type v) [CommRing k] [CommRing A] [Algebra k A] [Nontrivial A] (d : ℕ) [h : IsSmoothOfDimension k A d] : Module.finrank A ↥(canonicalModule k A d) = 1

The canonical module of a smooth k-algebra of dimension d is locally free of rank one, matching the line bundle interpretation of ω_X.

@[reducible, inline]

abbrev CanonicalSheafDef.conormalModule (A : Type u) [CommRing A] (I : Ideal A) : Type u

The conormal module of an ideal I ⊆ A, namely I / I².

theorem CanonicalSheafDef.conormalModule_isNoetherian (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A) : IsNoetherian A (conormalModule A I)

The conormal module of an ideal in a Noetherian ring is Noetherian.

theorem CanonicalSheafDef.conormalModule_finite_of_noetherian (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A) : Module.Finite A (conormalModule A I)

The conormal module of an ideal in a Noetherian ring is finitely generated.