NYLL
Module

RelEffCartierDiv_eq_of_isAlgEquivZero_of_nonempty_tensor_lineBundle_iso_lineBundle.lean

Nyll.JacobianVarieties.Picard.RelEffCartierDiv_eq_of_isAlgEquivZero_of_nonempty_tensor_lineBundle_iso_lineBundle
1 declaration indexed from sourceView source ↗

Module documentation

Degrees of algebraically equivalent effective Cartier divisors

A tensor comparison with an algebraically trivial line bundle preserves the divisor degree.

Imports20
Imported by2

Declarations

theorem

eq_of_isAlgEquivZero_of_nonempty_tensor_lineBundle_iso_lineBundle

L323 ↗
AlgebraicGeometry.RelEffCartierDiv.eq_of_isAlgEquivZero_of_nonempty_tensor_lineBundle_iso_lineBundle
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicGeometry.RelEffCartierDiv
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
Lean source · statement
theorem eq_of_isAlgEquivZero_of_nonempty_tensor_lineBundle_iso_lineBundle
    {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] [SmoothOfRelativeDimension 1 f]
      [GeometricallyIntegral f]
    {k : Type u} [Field k] [IsAlgClosed k] (x : Spec (CommRingCat.of k) ⟶ S) [IsProper
      (pullback.snd f x)]
    (𝒱 : (pullback f x).TwoAffineOpenCover)
    {r₁ r₂ : ℕ} (E₁ : RelEffCartierDiv f r₁ x) (E₂ : RelEffCartierDiv f r₂ x)
    (ℒ : (pullback f x).Modules) (hℒ : Scheme.Modules.IsInvertible ℒ)
    (h0 : IsAlgEquivZero (pullback.snd f x) ℒ)
    (e : Nonempty (ℒ ⊗ E₂.lineBundle ≅ E₁.lineBundle)) :
    r₁ = r₂

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.