Module

RelEffCartierDiv_isInvertible_I_of_smoothOfRelativeDimension_one.lean

Nyll.JacobianVarieties.Picard.RelEffCartierDiv_isInvertible_I_of_smoothOfRelativeDimension_one

2 declarations indexed from sourceView source ↗

Module documentation

Invertibility of a relative effective divisor on a smooth curve

Imports6

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv
Nyll.AlgebraicCurves.RelativeDivisors.Cartier
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isInvertible_I
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_of_forall_comap_openCover

Imported by1

Nyll.JacobianVarieties.Picard.All

theorem

main

L44 ↗

JacobianVarieties.Picard.Proofs.SmoothCurveCartier.GenCartier.main

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SmoothCurveCartier
attribute [-instance]
  AlgebraicGeometry.RelEffCartierDiv.isIso_subschemeIota_snd_of_degree_one
  AlgebraicGeometry.isIso_ker_graphOver_subschemeIota_snd
  AlgebraicGeometry.isClosedImmersion_graphOver
attribute [-simp]
  AlgebraicGeometry.graphOver_fst_assoc AlgebraicGeometry.RelEffCartierDiv.toPoint_comp
  AlgebraicGeometry.RelEffCartierDiv.toPoint_comp_assoc AlgebraicGeometry.graphOver_fst
  AlgebraicGeometry.RelEffCartierDiv.ofPoint_I AlgebraicGeometry.graphOver_snd
  AlgebraicGeometry.graphOver_snd_assoc
universe u
namespace GenCartier
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry

Lean source · statement

theorem main
    {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {K : Type u} [Field K] {gK : Spec (CommRingCat.of K) ⟶ S}
    [IsSeparated (pullback.snd f gK)] [SmoothOfRelativeDimension 1 (pullback.snd f gK)]
    {r : ℕ} (E : RelEffCartierDiv f r gK) :
    E.I.IsInvertible

theorem

isInvertible_I_of_smoothOfRelativeDimension_one

L82 ↗

AlgebraicGeometry.RelEffCartierDiv.isInvertible_I_of_smoothOfRelativeDimension_one

Source context 6 commands