Documentation

Atlas.AlgebraicGeometryI.code.AdjunctionSheaf

theorem conormal_ker_eq_ideal (R : Type u_1) [CommRing R] (I : Ideal R) :

The kernel of the canonical algebra map R → R/I is exactly I.

The cotangent module of ker(R → R/I) is the cotangent module I.Cotangent = I/I².

The canonical algebra map R → R/I is surjective.

Conormal exact sequence: for R → R/I over k, the maps I/I² → (R/I) ⊗_R Ω_{R/k} → Ω_{(R/I)/k} form an exact sequence at the middle term.

The base-change map (R/I) ⊗_R Ω_{R/k} → Ω_{(R/I)/k} is surjective.

theorem conormal_map_surjective_quotient (k : Type u) [CommRing k] (R : Type v) [CommRing R] [Algebra k R] (I : Ideal R) :

The induced map of Kähler differentials Ω_{R/k} → Ω_{(R/I)/(R/I)} is surjective.

First exact sequence of cotangent modules: (R/I) ⊗_R Ω_{R/k} → Ω_{(R/I)/(R/I)} → 0 is exact, where the second map sends to zero.

Ω_{k[x₀,x₁]/k} is a free module of rank 2 over k[x₀,x₁].

theorem kahler_mvpoly_rank (k : Type u_1) [Field k] (n : ) :

Ω_{k[x₁,…,xₙ]/k} is a free module of rank n over k[x₁,…,xₙ].

theorem kahler_mvpoly_free (k : Type u_1) [Field k] (n : ) :

Ω_{k[x₁,…,xₙ]/k} is a free module over k[x₁,…,xₙ].

Conormal exact sequence for a quotient of k[x₀,x₁] by an ideal I.

Surjectivity of the base-change map for a quotient of k[x₀,x₁].

Conormal exact sequence for a quotient of k[x₁,…,xₙ] by an ideal I.

theorem adjunction_formula_int (d : ) :
d * (d - 3) = (d - 1) * (d - 2) - 2

Numerical adjunction identity over the integers: d(d-3) = (d-1)(d-2) - 2, the algebraic content of the genus-degree formula for a smooth plane curve of degree d.

theorem adjunction_formula_genus_degree (d : ) (hd : 3 d) :
d * (d - 3) + 2 = (d - 1) * (d - 2)

Natural-number form of the adjunction identity for d ≥ 3.

theorem adjunction_formula_numerical (d : ) :
d * (d - 3) = 2 * ((d - 1) * (d - 2) / 2) - 2

Numerical form: d(d-3) = 2·[(d-1)(d-2)/2] - 2, recovering g = (d-1)(d-2)/2.

theorem finrank_le_of_surjective_lm {R : Type u_1} [CommRing R] [Nontrivial R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Surjective f) :

If f : M → N is a surjective R-linear map and M is finite, then finrank N ≤ finrank M.

The base change (R/I) ⊗_R Ω_{R/k} of the rank-n free module of differentials of R = k[x₁,…,xₙ] has (R/I)-rank n.

theorem conormal_rank_bound (k : Type u_1) [Field k] (n : ) (I : Ideal (MvPolynomial (Fin n) k)) [Nontrivial (MvPolynomial (Fin n) k I)] :

Rank bound: rank Ω_{(R/I)/k} ≤ n where R = k[x₁,…,xₙ].

Two-variable specialization: rank of Ω_{(R/I)/k} is at most 2 for R = k[x₀,x₁].

theorem adjunction_degree_from_exact_sequence (n : ) (d deg_ambient_cotangent_restricted deg_conormal : ) (h_euler : deg_ambient_cotangent_restricted = -(n + 1) * d) (h_conormal : deg_conormal = -(d * d)) :
deg_ambient_cotangent_restricted - deg_conormal = d * (d - (n + 1))

From the conormal exact sequence on a degree-d hypersurface in ℙⁿ, the degree of ω on the hypersurface is d(d - (n+1)).

theorem adjunction_formula_from_sequence_and_genus (d : ) :
(∀ (deg_Ω_P2_C deg_conormal : ), deg_Ω_P2_C = -3 * ddeg_conormal = -(d * d) → deg_Ω_P2_C - deg_conormal = d * (d - 3)) d * (d - 3) = (d - 1) * (d - 2) - 2

For a plane curve C ⊂ ℙ² of degree d, the adjunction formula gives deg ω_C = d(d-3) = (d-1)(d-2) - 2.

Proposition 35: the conormal sequence I/I² → (R/I) ⊗_R Ω_{R/k} → Ω_{(R/I)/k} → 0 is exact at the middle term and the right map is surjective.

When R is formally smooth over k, injectivity of I/I² → (R/I) ⊗_R Ω_{R/k} is equivalent to the vanishing of of the cotangent complex of R/I over k.

When both R and R/I are formally smooth over k, the conormal map I/I² → (R/I) ⊗ Ω_{R/k} is injective.

When both R and R/I are formally smooth over k, the conormal map is split-injective.

Corollary 26: when both R and R/I are formally smooth over k, the conormal sequence 0 → I/I² → (R/I) ⊗ Ω_{R/k} → Ω_{(R/I)/k} → 0 is short exact and split.

theorem corollary_26_adjunction_formula (d : ) :
(∀ (deg_Ω_P2_C deg_conormal : ), deg_Ω_P2_C = -(2 + 1) * ddeg_conormal = -(d * d) → deg_Ω_P2_C - deg_conormal = d * (d - 3)) d * (d - 3) = (d - 1) * (d - 2) - 2

Specialization of the adjunction-formula numerics to plane curves: the genus-degree formula g = (d-1)(d-2)/2 emerges from d(d-3) = (d-1)(d-2) - 2.

Adjunction formula for a principal divisor: ω_D ≃ ω_X(-D)|_D. In algebraic terms, ⋀^{n-1} Ω_{(R/I)/k} ≃ ((R/I) ⊗ ⋀^n Ω_{R/k}) ⊗ (I/I²)* when I is principal and both R and R/I are formally smooth (Cor 24, Lec 19).

theorem exteriorPower_baseChange_equiv (R : Type u_1) [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] (M : Type u_3) [AddCommGroup M] [Module R M] [Module.Free R M] (n : ) :
Nonempty (TensorProduct R S (⋀[R]^n M) ≃ₗ[S] (⋀[S]^n (TensorProduct R S M)))

Exterior powers commute with base change for free modules: S ⊗_R ⋀^n M ≃ ⋀^n_S (S ⊗_R M).

theorem exteriorPower_of_prod (S : Type u_1) [CommRing S] (A : Type u_2) (C : Type u_3) [AddCommGroup A] [Module S A] [AddCommGroup C] [Module S C] (n : ) :
Nonempty ((⋀[S]^n (A × C)) ≃ₗ[S] TensorProduct S (↥(⋀[S]^(n - 1) C)) A × (⋀[S]^n C))

Decomposition of the top exterior power of a direct sum: ⋀^n (A ⊕ C) ≃ (⋀^{n-1} C ⊗ A) × ⋀^n C (used in the proof of the adjunction formula).

theorem adjunctionFormula (k : Type u) [CommRing k] (R : Type v) [CommRing R] [Algebra k R] (I : Ideal R) (n : ) [Algebra.FormallySmooth k R] [Algebra.FormallySmooth k (R I)] [Module.Free R Ω[Rk]] :
Nonempty (TensorProduct R (R I) (⋀[R]^n Ω[Rk]) ≃ₗ[R I] TensorProduct (R I) (↥(⋀[R I]^(n - 1) Ω[R Ik])) I.Cotangent)

Algebraic adjunction formula: when both R and R/I are formally smooth over k and Ω_{R/k} is free, the restriction of the top exterior power of Ω_{R/k} to R/I is isomorphic to ⋀^{n-1} Ω_{(R/I)/k} ⊗ (I/I²). This is the algebraic form of ω_X|_D ≃ ω_D ⊗ N_{D/X}.