@[reducible, inline]

abbrev PolyRing (k : Type u) [Field k] (n : ℕ) : Type u

Abbreviation for the polynomial ring k[x₀, …, x_n] over k in n + 1 variables.

noncomputable def kahlerBasis_mvPolynomial (k : Type u) [Field k] (n : ℕ) : Module.Basis (Fin (n + 1)) (PolyRing k n) Ω[PolyRing k n⁄k]

Canonical basis of Ω[k[x₀,…,x_n]⁄k] given by the dxᵢ.

theorem kahler_mvPolynomial_free (k : Type u) [Field k] (n : ℕ) : Module.Free (PolyRing k n) Ω[PolyRing k n⁄k]

The Kähler differential module of a polynomial ring is free.

theorem kahler_mvPolynomial_finrank (k : Type u) [Field k] (n : ℕ) : Module.finrank (PolyRing k n) Ω[PolyRing k n⁄k] = n + 1

The rank of the Kähler differential module of k[x₀,…,x_n] is n + 1.

instance kahler_mvPolynomial_finite (k : Type u) [Field k] (n : ℕ) : Module.Finite (PolyRing k n) Ω[PolyRing k n⁄k]

The Kähler differential module of k[x₀,…,x_n] is finitely generated.

noncomputable def kahler_mvPolynomial_equivFun (k : Type u) [Field k] (n : ℕ) : Ω[PolyRing k n⁄k] ≃ₗ[PolyRing k n] Fin (n + 1) → PolyRing k n

Coordinate isomorphism between Kähler differentials of k[x₀,…,x_n] and the rank-(n+1) free module.

instance polyRing_isSmoothOfDimension (k : Type u) [Field k] (n : ℕ) : CanonicalSheafDef.IsSmoothOfDimension k (PolyRing k n) (n + 1)

A polynomial ring k[x₀, …, x_n] is smooth of dimension n + 1 over k.

theorem canonicalModule_polyRing_eq (k : Type u) [Field k] (n : ℕ) : CanonicalSheafDef.canonicalModule k (PolyRing k n) (n + 1) = ⋀[PolyRing k n]^(n + 1) Ω[PolyRing k n⁄k]

The canonical module of k[x₀,…,x_n] in dimension n + 1 is the top exterior power of the Kähler differentials.

theorem canonicalModule_polyRing_finrank (k : Type u) [Field k] (n : ℕ) : Module.finrank (PolyRing k n) ↥(CanonicalSheafDef.canonicalModule k (PolyRing k n) (n + 1)) = 1

The canonical module of k[x₀,…,x_n] in dimension n + 1 has rank 1.

theorem canonicalModule_polyRing_free (k : Type u) [Field k] (n : ℕ) : Module.Free (PolyRing k n) ↥(CanonicalSheafDef.canonicalModule k (PolyRing k n) (n + 1))

The canonical module of k[x₀,…,x_n] is a free module.

theorem topExteriorPower_kahler_finrank (k : Type u) [Field k] (n : ℕ) : Module.finrank (PolyRing k n) ↥(⋀[PolyRing k n]^(n + 1) Ω[PolyRing k n⁄k]) = 1

The top exterior power of Kähler differentials has rank 1.

theorem topExteriorPower_kahler_free (k : Type u) [Field k] (n : ℕ) : Module.Free (PolyRing k n) ↥(⋀[PolyRing k n]^(n + 1) Ω[PolyRing k n⁄k])

The top exterior power of Kähler differentials is a free module.

theorem exteriorPower_kahler_finrank_zero (k : Type u) [Field k] (n p : ℕ) (hp : n + 1 < p) : Module.finrank (PolyRing k n) ↥(⋀[PolyRing k n]^p Ω[PolyRing k n⁄k]) = 0

Exterior powers above the dimension vanish: Λ^p Ω = 0 for p > n + 1.

theorem exteriorPower_kahler_finrank (k : Type u) [Field k] (n p : ℕ) : Module.finrank (PolyRing k n) ↥(⋀[PolyRing k n]^p Ω[PolyRing k n⁄k]) = (n + 1).choose p

Rank of the p-th exterior power of Kähler differentials: (n + 1 choose p).

theorem finrank_direct_sum_free (R : Type u) [CommRing R] [Nontrivial R] (n : ℕ) : Module.finrank R (Fin (n + 1) → R) = n + 1

The free R-module Fin (n + 1) → R has rank n + 1.

theorem finrank_top_exterior_direct_sum (R : Type u) [CommRing R] [Nontrivial R] (n : ℕ) : Module.finrank R ↥(⋀[R]^(n + 1) (Fin (n + 1) → R)) = 1

The top exterior power of the rank-(n+1) free R-module has rank 1.

@[reducible, inline]

abbrev CanonicalBundleProj.GrLinMap (k : Type u) [Field k] (n : ℕ) (M N : QCohProjective.GradedModuleData k n) (d : ℤ) : Type u

Type of graded k-linear maps in fixed degree d between two graded modules M, N.

@[reducible, inline]

abbrev CanonicalBundleProj.GrLinEquiv (k : Type u) [Field k] (n : ℕ) (M N : QCohProjective.GradedModuleData k n) (d : ℤ) : Type u

Type of graded k-linear equivalences in degree d between two graded modules M, N.

structure CanonicalBundleProj.GradedSES (k : Type u) [Field k] (n : ℕ) : Type (u + 1)

A short exact sequence of graded k-modules on P^n, given by maps in every degree together with proofs of injectivity, surjectivity and exactness in the middle.

• left : QCohProjective.GradedModuleData k n
• middle : QCohProjective.GradedModuleData k n
• right : QCohProjective.GradedModuleData k n
• f (d : ℤ) : GrLinMap k n self.left self.middle d
• g (d : ℤ) : GrLinMap k n self.middle self.right d
• f_injective (d : ℤ) : Function.Injective ⇑(self.f d)
• g_surjective (d : ℤ) : Function.Surjective ⇑(self.g d)
• exact_middle (d : ℤ) (x : self.middle.component d) : (self.g d) x = Zero.zero ↔ ∃ (a : self.left.component d), (self.f d) a = x

noncomputable def CanonicalBundleProj.directSumTwist (k : Type u) [Field k] (n : ℕ) : QCohProjective.GradedModuleData k n

Middle term of the Euler sequence on P^n: the direct sum O(-1)^{n+1}.

instance CanonicalBundleProj.instNonemptyGradedModuleData (k : Type u) [Field k] (n : ℕ) : Nonempty (QCohProjective.GradedModuleData k n)

The structure sheaf provides a default graded module on P^n, giving inhabitedness.

opaque CanonicalBundleProj.cotangentSheafGM (k : Type u) [Field k] (n : ℕ) : QCohProjective.GradedModuleData k n

The cotangent (Kähler differentials) sheaf on P^n, presented as a graded module.

opaque CanonicalBundleProj.canonicalBundleGM (k : Type u) [Field k] (n : ℕ) : QCohProjective.GradedModuleData k n

The canonical bundle of P^n (top exterior power of the cotangent sheaf), as a graded module. By Prop 36 (Lec 20) this equals O(-(n+1)).

theorem CanonicalBundleProj.eulerSES (k : Type u) [Field k] (n : ℕ) : ∃ (S : GradedSES k n), S.left = cotangentSheafGM k n ∧ S.middle = directSumTwist k n ∧ S.right = TwistSheaf.structureSheafData k n

The Euler sequence on P^n: 0 → Ω → O(-1)^{n+1} → O → 0.

theorem CanonicalBundleProj.det_direct_sum_twist (n : ℕ) : (↑n + 1) * -1 = -(↑n + 1)

Determinant of O(-1)^{n+1} is O(-(n+1)): the integer identity (n+1) · (-1) = -(n+1).

theorem CanonicalBundleProj.canonical_bundle_eq_twist (k : Type u) [Field k] (n : ℕ) (d : ℤ) : Nonempty (GrLinEquiv k n (canonicalBundleGM k n) (TwistSheaf.serreTwist k n (-(↑n + 1))) d)

Canonical bundle of P^n is O(-(n+1)) (Prop 36, Lec 20).

theorem CanonicalBundleProj.canonical_twist_eq (n : ℕ) : -(↑n + 1) = -↑(n + 1)

Numerical identity -(n + 1) = -(↑(n + 1)) used when rewriting the canonical twist.

theorem CanonicalBundleProj.canonical_bundle_P1_eq_twist (k : Type u) [Field k] (d : ℤ) : Nonempty (GrLinEquiv k 1 (canonicalBundleGM k 1) (TwistSheaf.serreTwist k 1 (-2)) d)

Specialisation to P^1: K_{P^1} = O(-2).

def CanonicalBundleProj.HasTwistDegree (k : Type u) [Field k] (n : ℕ) (M : QCohProjective.GradedModuleData k n) (d : ℤ) : Prop

Predicate: a graded module M on P^n is isomorphic to the twisted sheaf O(d).

theorem CanonicalBundleProj.deg_canonical_P1 (k : Type u) [Field k] : HasTwistDegree k 1 (canonicalBundleGM k 1) (-2)

The canonical bundle of P^1 has twist degree -2, i.e. K_{P^1} ≅ O(-2).