theorem PicardProjective.homogeneous_degree_unique {σ : Type u_1} {k : Type u_2} [Field k] {f : MvPolynomial σ k} {d₁ d₂ : ℕ} (hf : f ≠ 0) (h1 : f.IsHomogeneous d₁) (h2 : f.IsHomogeneous d₂) : d₁ = d₂

A nonzero homogeneous polynomial has a unique degree of homogeneity.

theorem PicardProjective.isUnit_isHomogeneous_zero {σ : Type u_1} {k : Type u_2} [Field k] {u : MvPolynomial σ k} (hu : IsUnit u) : u.IsHomogeneous 0

Every unit in k[x_1,...,x_n] is a constant, hence homogeneous of degree 0.

theorem PicardProjective.associated_homogeneous_same_degree {σ : Type u_1} {k : Type u_2} [Field k] {f g : MvPolynomial σ k} {d₁ d₂ : ℕ} (hg : g ≠ 0) (hfh : f.IsHomogeneous d₁) (hgh : g.IsHomogeneous d₂) (h : Associated f g) : d₁ = d₂

Associated homogeneous polynomials (i.e. differing by a unit) have the same degree.

theorem PicardProjective.mvPolynomial_fin_ufd (k : Type u_1) [Field k] (n : ℕ) : UniqueFactorizationMonoid (MvPolynomial (Fin n) k)

The polynomial ring k[x_1,...,x_n] is a UFD.

theorem PicardProjective.mvPolynomial_ufd_of_ufd (R : Type u_1) [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] (σ : Type u_2) : UniqueFactorizationMonoid (MvPolynomial σ R)

The polynomial ring R[x_σ] over a UFD R (with any number of variables) is a UFD.

instance PicardProjective.classGroup_mvPolynomial_subsingleton (k : Type u_1) [Field k] (σ : Type u_2) : Subsingleton (ClassGroup (MvPolynomial σ k))

The (divisor) class group of a polynomial ring over a field is trivial.

instance PicardProjective.classGroup_polynomial_subsingleton (k : Type u_1) [Field k] : Subsingleton (ClassGroup (Polynomial k))

The class group of the univariate polynomial ring k[x] is trivial.

@[implicit_reducible]

noncomputable instance PicardProjective.classGroup_mvPolynomial_unique (k : Type u_1) [Field k] (n : ℕ) : Unique (ClassGroup (MvPolynomial (Fin n) k))

The class group of k[x_1,...,x_n] is the trivial group with a unique element.

noncomputable def PicardProjective.classGroup_mvPolynomial_mulEquiv_unit (k : Type u_1) [Field k] (n : ℕ) : ClassGroup (MvPolynomial (Fin n) k) ≃* Unit

The class group of k[x_1,...,x_n] is isomorphic (as a group) to the trivial group Unit.

structure PicardProjective.HomogFraction (σ : Type u_1) (k : Type u_2) [Field k] : Type (max u_1 u_2)

A homogeneous fraction: a pair of nonzero homogeneous polynomials of recorded degrees, representing a section of a twist O(d) on projective space.

• num : MvPolynomial σ k
• den : MvPolynomial σ k
• num_ne : self.num ≠ 0
• den_ne : self.den ≠ 0
• ndeg : ℕ
• ddeg : ℕ
• nhom : self.num.IsHomogeneous self.ndeg
• dhom : self.den.IsHomogeneous self.ddeg

def PicardProjective.HomogFraction.degree (σ : Type u_1) (k : Type u_2) [Field k] (p : HomogFraction σ k) : ℤ

The degree of a homogeneous fraction: numerator degree minus denominator degree.

def PicardProjective.HomogFraction.PicEquiv (σ : Type u_1) (k : Type u_2) [Field k] (p q : HomogFraction σ k) : Prop

Equivalence relation on homogeneous fractions identifying those that represent the same line bundle class in Pic(P^n).

theorem PicardProjective.HomogFraction.PicEquiv.rfl' (σ : Type u_1) (k : Type u_2) [Field k] (p : HomogFraction σ k) : PicEquiv σ k p p

Reflexivity of the Pic equivalence relation on homogeneous fractions.

theorem PicardProjective.HomogFraction.PicEquiv.symm' (σ : Type u_1) (k : Type u_2) [Field k] {p q : HomogFraction σ k} (h : PicEquiv σ k p q) : PicEquiv σ k q p

Symmetry of the Pic equivalence relation.

theorem PicardProjective.HomogFraction.PicEquiv.trans' (σ : Type u_1) (k : Type u_2) [Field k] {p q r : HomogFraction σ k} (h1 : PicEquiv σ k p q) (h2 : PicEquiv σ k q r) : PicEquiv σ k p r

Transitivity of the Pic equivalence relation.

@[implicit_reducible]

instance PicardProjective.homogFractionSetoid (σ : Type u_1) (k : Type u_2) [Field k] : Setoid (HomogFraction σ k)

The setoid on homogeneous fractions induced by the Pic equivalence relation.

def PicardProjective.GradedPicardGroup (σ : Type u_1) (k : Type u_2) [Field k] : Type (max u_1 u_2)

The graded Picard group: equivalence classes of homogeneous fractions, modeling Pic(P^n) by twisting sheaves up to isomorphism.

theorem PicardProjective.degree_compat (σ : Type u_1) (k : Type u_2) [Field k] (p q : HomogFraction σ k) (h : HomogFraction.PicEquiv σ k p q) : HomogFraction.degree σ k p = HomogFraction.degree σ k q

The degree function is compatible with the Pic equivalence relation: equivalent homogeneous fractions have the same degree.

def PicardProjective.GradedPicardGroup.degreeMap (σ : Type u_1) (k : Type u_2) [Field k] : GradedPicardGroup σ k → ℤ

The degree map Pic(P^n) → ℤ defined on equivalence classes.

noncomputable def PicardProjective.HomogFraction.mul (σ : Type u_1) (k : Type u_2) [Field k] (p q : HomogFraction σ k) : HomogFraction σ k

Multiplication of homogeneous fractions: corresponds to tensor product of twists in Pic(P^n).

noncomputable def PicardProjective.HomogFraction.one (σ : Type u_1) (k : Type u_2) [Field k] : HomogFraction σ k

The trivial homogeneous fraction 1/1, representing the structure sheaf O_{P^n}.

def PicardProjective.HomogFraction.inv (σ : Type u_1) (k : Type u_2) [Field k] (p : HomogFraction σ k) : HomogFraction σ k

Inverse of a homogeneous fraction: swap numerator and denominator, corresponding to the dual line bundle.

theorem PicardProjective.mul_compat (σ : Type u_1) (k : Type u_2) [Field k] {p₁ p₂ q₁ q₂ : HomogFraction σ k} (hp : HomogFraction.PicEquiv σ k p₁ p₂) (hq : HomogFraction.PicEquiv σ k q₁ q₂) : HomogFraction.PicEquiv σ k (HomogFraction.mul σ k p₁ q₁) (HomogFraction.mul σ k p₂ q₂)

Multiplication of homogeneous fractions respects the Pic equivalence relation.

theorem PicardProjective.inv_compat (σ : Type u_1) (k : Type u_2) [Field k] {p q : HomogFraction σ k} (h : HomogFraction.PicEquiv σ k p q) : HomogFraction.PicEquiv σ k (HomogFraction.inv σ k p) (HomogFraction.inv σ k q)

Inversion of homogeneous fractions respects the Pic equivalence relation.

@[implicit_reducible]

noncomputable instance PicardProjective.gradedPicardGroupZero (σ : Type u_1) (k : Type u_2) [Field k] : Zero (GradedPicardGroup σ k)

The zero element of the graded Picard group (additive notation): the class of the trivial fraction.

@[implicit_reducible]

noncomputable instance PicardProjective.gradedPicardGroupAdd (σ : Type u_1) (k : Type u_2) [Field k] : Add (GradedPicardGroup σ k)

Addition in the graded Picard group: induced from multiplication of fractions.

@[implicit_reducible]

instance PicardProjective.gradedPicardGroupNeg (σ : Type u_1) (k : Type u_2) [Field k] : Neg (GradedPicardGroup σ k)

Negation in the graded Picard group: induced from inversion of fractions.

theorem PicardProjective.ring_assoc_equiv (σ : Type u_1) (k : Type u_2) [Field k] (p q : HomogFraction σ k) (hn : p.num = q.num) (hd : p.den = q.den) : p.ndeg = q.ndeg → p.ddeg = q.ddeg → HomogFraction.PicEquiv σ k p q

Two homogeneous fractions with identical components are equivalent.

@[implicit_reducible]

noncomputable instance PicardProjective.gradedPicardGroupAddCommGroup (σ : Type u_1) (k : Type u_2) [Field k] : AddCommGroup (GradedPicardGroup σ k)

The graded Picard group is an additive commutative group.

theorem PicardProjective.degreeMap_add (σ : Type u_1) (k : Type u_2) [Field k] (a b : GradedPicardGroup σ k) : GradedPicardGroup.degreeMap σ k (a + b) = GradedPicardGroup.degreeMap σ k a + GradedPicardGroup.degreeMap σ k b

The degree map is additive: deg(L ⊗ M) = deg(L) + deg(M).

def PicardProjective.GradedPicardGroup.degreeHom (σ : Type u_1) (k : Type u_2) [Field k] : GradedPicardGroup σ k →+ ℤ

The degree map as an additive group homomorphism Pic(P^n) → ℤ.

noncomputable def PicardProjective.twistFraction (n : ℕ) (k : Type u_1) [Field k] (d : ℤ) : HomogFraction (Fin (n + 1)) k

The homogeneous fraction representing the d-th twist O(d) on P^n.

theorem PicardProjective.twistFraction_degree (n : ℕ) (k : Type u_1) [Field k] (d : ℤ) : HomogFraction.degree (Fin (n + 1)) k (twistFraction n k d) = d

The twist O(d) has degree d.

noncomputable def PicardProjective.twistingSheafPow (n : ℕ) (k : Type u_1) [Field k] (d : ℤ) : GradedPicardGroup (Fin (n + 1)) k

The twisting sheaf O(d) in Pic(P^n), as the class of the d-th twist fraction.

noncomputable def PicardProjective.twistingSheaf (n : ℕ) (k : Type u_1) [Field k] : GradedPicardGroup (Fin (n + 1)) k

The Serre twisting sheaf O(1) generating Pic(P^n) ≅ ℤ.

theorem PicardProjective.degreeHom_surjective (n : ℕ) (k : Type u_1) [Field k] : Function.Surjective ⇑(GradedPicardGroup.degreeHom (Fin (n + 1)) k)

The degree homomorphism Pic(P^n) → ℤ is surjective (every integer is realized by some O(d)).

theorem PicardProjective.degree_zero_equiv_one (σ : Type u_1) (k : Type u_2) [Field k] (p : HomogFraction σ k) (hdeg : HomogFraction.degree σ k p = 0) : HomogFraction.PicEquiv σ k p (HomogFraction.one σ k)

A homogeneous fraction of degree 0 is equivalent to the trivial fraction.

theorem PicardProjective.degreeHom_injective (σ : Type u_1) (k : Type u_2) [Field k] : Function.Injective ⇑(GradedPicardGroup.degreeHom σ k)

The degree homomorphism is injective: any line bundle of degree 0 is trivial.

noncomputable def PicardProjective.gradedPicardGroup_equiv_int (k : Type u_1) [Field k] (n : ℕ) : GradedPicardGroup (Fin (n + 1)) k ≃+ ℤ

The fundamental identification Pic(P^n) ≅ ℤ as additive groups, via the degree map.

theorem PicardProjective.degree_twistingSheafPow (k : Type u_1) [Field k] (n : ℕ) (d : ℤ) : (gradedPicardGroup_equiv_int k n) (twistingSheafPow n k d) = d

Under the equivalence Pic(P^n) ≅ ℤ, the twist O(d) corresponds to the integer d.

theorem PicardProjective.degree_twistingSheaf (k : Type u_1) [Field k] (n : ℕ) : (gradedPicardGroup_equiv_int k n) (twistingSheaf n k) = 1

The Serre twisting sheaf O(1) corresponds to the integer 1 under Pic(P^n) ≅ ℤ.

theorem PicardProjective.picardGroup_generated_by_O1 (k : Type u_1) [Field k] (n : ℕ) (L : GradedPicardGroup (Fin (n + 1)) k) : ∃ (d : ℤ), L = twistingSheafPow n k d

Pic(P^n) is generated by O(1): every line bundle on P^n is some O(d).