Fixed-rank descent for the relative cotangent sheaf

This file carries the affine Kähler calculation through sheafification. A standard-smooth chart supplies a basis of the objectwise differential module; localization on principal opens proves that the basis morphism is locally bijective, hence its sheafification is an isomorphism. These chart isomorphisms assemble into fixed-rank locally-free data for the cotangent sheaf.

structure AlgebraicGeometry.Scheme.Modules.FixedRankTrivializations {X : Scheme} (E : X.Modules) (n : ℕ) : Type (u + 1)

A cover on which a module sheaf is explicitly trivial of fixed rank n.

• I : Type u

  Indexing type of the chosen cover.

• chartOpen : self.I → X.Opens

  Opens in the trivializing cover.

• coversTop : (Opens.grothendieckTopology ↥X).CoversTop self.chartOpen

  The chosen opens cover the scheme.

• trivialization (i : self.I) : SheafOfModules.free (ULift.{u, 0} (Fin n)) ≅ SheafOfModules.over E (self.chartOpen i)

  A rank-n free trivialization on every cover member.

noncomputable def AlgebraicGeometry.Scheme.Modules.FixedRankTrivializations.localGenerators {X : Scheme} {E : X.Modules} {n : ℕ} (T : E.FixedRankTrivializations n) : (have this := E; this).LocalGeneratorsData

The local generating sections induced by the chosen free trivializations.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Modules.FixedRankTrivializations.localGenerators_isLocallyFreeData {X : Scheme} {E : X.Modules} {n : ℕ} (T : E.FixedRankTrivializations n) : T.localGenerators.IsLocallyFreeData

The induced local generators are bases rather than merely epimorphic generating families.

noncomputable def AlgebraicGeometry.Scheme.Modules.FixedRankTrivializations.finiteLocallyFree {X : Scheme} {E : X.Modules} {n : ℕ} (T : E.FixedRankTrivializations n) : E.FiniteLocallyFreeData n

Explicit rank-n trivializations produce fixed-rank locally-free data.

Equations

• T.finiteLocallyFree = { localGenerators := T.localGenerators, isLocallyFreeData := ⋯, rankEquiv := ⋯ }

noncomputable def AlgebraicGeometry.Scheme.Modules.FixedRankTrivializations.topExteriorTrivialization {X : Scheme} {E : X.Modules} {n : ℕ} (T : E.FixedRankTrivializations n) (i : T.I) : SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf (T.chartOpen i)) ≅ SheafOfModules.over (E.exteriorPower n) (T.chartOpen i)

The determinant trivialization induced on each member of the fixed-rank atlas.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Modules.FixedRankTrivializations.topExteriorPower_isInvertible {X : Scheme} {E : X.Modules} {n : ℕ} (T : E.FixedRankTrivializations n) : (have this := E.exteriorPower n; this).IsInvertible

The top exterior power of an explicitly fixed-rank locally-free sheaf is invertible.

noncomputable def AlgebraicGeometry.Scheme.Modules.FixedRankTrivializations.exteriorDeterminantData {X : Scheme} {E : X.Modules} {n : ℕ} (T : E.FixedRankTrivializations n) : E.ExteriorDeterminantData

Fixed-rank trivializations canonically package the constructed top exterior power as an explicit line bundle with its sheafified-dual tensor inverse.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Modules.FixedRankTrivializations.determinantData {X : Scheme} {E : X.Modules} {n : ℕ} (T : E.FixedRankTrivializations n) : E.DeterminantData

The determinant package underlying exteriorDeterminantData.

Equations

• T.determinantData = T.exteriorDeterminantData.determinantData

theorem AlgebraicGeometry.Scheme.Modules.FixedRankTrivializations.isLocallyFree {X : Scheme} {E : X.Modules} {n : ℕ} (T : E.FixedRankTrivializations n) : (have this := E; this).IsLocallyFree

In particular, an explicitly rank-n-trivialized sheaf is locally free.

structure AlgebraicGeometry.Variety.SmoothChart (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] (n : ℕ) (x : ↥X) : Type u

A standard-smooth affine chart of relative dimension n around a point.

• target : (Spec (CommRingCat.of k)).Opens
• targetAffine : IsAffineOpen self.target
• source : X.Opens
• sourceAffine : IsAffineOpen self.source
• mem_source : x ∈ self.source
• source_le_preimage : self.source ≤ (TopologicalSpace.Opens.map (X ↘ Spec (CommRingCat.of k)).base).obj self.target
• standardSmooth : RingHom.IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE (X ↘ Spec (CommRingCat.of k)) self.target self.source ⋯))

noncomputable def AlgebraicGeometry.Variety.SmoothChart.ofSmooth (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] {n : ℕ} (h : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))) (x : ↥X) : SmoothChart k X n x

Choose the standard-smooth chart supplied at a point by smooth pure relative dimension.

Equations

• AlgebraicGeometry.Variety.SmoothChart.ofSmooth k X h x = Classical.choice ⋯

theorem AlgebraicGeometry.Variety.SmoothChart.standardSmooth_baseField (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] {n : ℕ} {x : ↥X} (C : SmoothChart k X n x) : RingHom.IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom ((baseFieldToStructurePresheaf k X).app (Opposite.op C.source)))

The ring map on a standard-smooth chart is standard smooth after identifying the unique affine open of Spec k containing the image point with the whole spectrum.

noncomputable def AlgebraicGeometry.Variety.relativeDifferentialsChartIso (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {n : ℕ} {x : ↥X} (C : SmoothChart k X n x) : SheafOfModules.free (ULift.{u, 0} (Fin n)) ≅ SheafOfModules.over (relativeDifferentials k X) C.source

On a standard-smooth affine chart of relative dimension n, the relative cotangent sheaf is the free sheaf of rank n.

Equations

• One or more equations did not get rendered due to their size.

structure AlgebraicGeometry.Variety.SmoothCotangentTrivializations (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] {n : ℕ} (h : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))) : Type u

Rank-n cotangent trivializations on the canonical standard-smooth chart cover.

• trivialization (x : ↥X) : SheafOfModules.free (ULift.{u, 0} (Fin n)) ≅ SheafOfModules.over (relativeDifferentials k X) (SmoothChart.ofSmooth k X h x).source

noncomputable def AlgebraicGeometry.Variety.SmoothCotangentTrivializations.ofSmooth {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {n : ℕ} {h : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))} : SmoothCotangentTrivializations k X h

Smoothness of pure relative dimension canonically supplies the cotangent chart trivializations.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Variety.SmoothCotangentTrivializations.chartSources_coversTop {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} {h : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))} (_T : SmoothCotangentTrivializations k X h) : (Opens.grothendieckTopology ↥X).CoversTop fun (x : ↥X) => (SmoothChart.ofSmooth k X h x).source

The source opens of the chosen smooth charts cover the variety.

noncomputable def AlgebraicGeometry.Variety.SmoothCotangentTrivializations.fixedRankTrivializations {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} {h : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))} (T : SmoothCotangentTrivializations k X h) : (relativeDifferentials k X).FixedRankTrivializations n

Package the smooth-chart comparisons as fixed-rank trivializations of Ω¹_{X/k}.

Equations

• T.fixedRankTrivializations = { I := ↥X, chartOpen := fun (x : ↥X) => (AlgebraicGeometry.Variety.SmoothChart.ofSmooth k X h x).source, coversTop := ⋯, trivialization := T.trivialization }

noncomputable def AlgebraicGeometry.Variety.SmoothCotangentTrivializations.finiteLocallyFree {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} {h : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))} (T : SmoothCotangentTrivializations k X h) : (relativeDifferentials k X).FiniteLocallyFreeData n

The chartwise sheafification comparisons globalize to fixed-rank locally-free cotangent data.

Equations

• T.finiteLocallyFree = T.fixedRankTrivializations.finiteLocallyFree

theorem AlgebraicGeometry.Variety.SmoothCotangentTrivializations.relativeDifferentials_isLocallyFree {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} {h : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))} (T : SmoothCotangentTrivializations k X h) : (have this := relativeDifferentials k X; this).IsLocallyFree

The constructed relative cotangent sheaf is locally free once the chart comparisons are supplied.

noncomputable def AlgebraicGeometry.Variety.relativeDifferentialsFiniteLocallyFree (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {n : ℕ} (h : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))) : (relativeDifferentials k X).FiniteLocallyFreeData n

The relative cotangent sheaf of a smooth pure-dimensional variety is finite locally free of the relative dimension.

Equations

• AlgebraicGeometry.Variety.relativeDifferentialsFiniteLocallyFree k X h = AlgebraicGeometry.Variety.SmoothCotangentTrivializations.ofSmooth.finiteLocallyFree

theorem AlgebraicGeometry.Variety.relativeDifferentials_isLocallyFree_of_smooth (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {n : ℕ} (h : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))) : (have this := relativeDifferentials k X; this).IsLocallyFree

The relative cotangent sheaf of a smooth pure-dimensional variety is locally free.

noncomputable def AlgebraicGeometry.Variety.relativeDifferentialsExteriorDeterminantData (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {n : ℕ} (h : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))) : (relativeDifferentials k X).ExteriorDeterminantData

Smooth pure relative dimension supplies determinant descent for the relative cotangent sheaf, including the constructed top exterior power and its explicit tensor inverse.

Equations

• AlgebraicGeometry.Variety.relativeDifferentialsExteriorDeterminantData k X h = AlgebraicGeometry.Variety.SmoothCotangentTrivializations.ofSmooth.fixedRankTrivializations.exteriorDeterminantData

noncomputable def AlgebraicGeometry.Variety.relativeDifferentialsDeterminantData (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {n : ℕ} (h : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))) : (relativeDifferentials k X).DeterminantData

The determinant data underlying relativeDifferentialsExteriorDeterminantData.

Equations

• AlgebraicGeometry.Variety.relativeDifferentialsDeterminantData k X h = (AlgebraicGeometry.Variety.relativeDifferentialsExteriorDeterminantData k X h).determinantData

noncomputable def AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.ofSmoothRelativeDifferentials {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} (h : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))) : CanonicalSheafData k X n

The automatic canonical-sheaf package of a smooth proper variety of pure relative dimension n.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.ofSmoothRelativeDifferentials_cotangent {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} (h : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))) : (ofSmoothRelativeDifferentials h).cotangent = Variety.relativeDifferentials k X