Module

isInvertible_sectionIdeal_of_range_subset.lean

Nyll.AlgebraicCurves.Geometry.Picard.isInvertible_sectionIdeal_of_range_subset

2 declarations indexed from sourceView source ↗

Module documentation

is Invertible section Ideal of range subset

Imports9

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.CategoryTheory.MorphismProperty.Limits
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Nyll.AlgebraicCurves.RelativeDivisors.Cartier
Nyll.AlgebraicCurves.Geometry.Sheaves.RelativeSectionTwist
Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_isInvertible_ker_of_comp_eq_id
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_of_comap_of_support_subset_range

Imported by20

theorem

main

L39 ↗

JacobianVarieties.Picard.Proofs.S_AlgebraicGeometry_RelPicard_isInvertible_sectionIdeal_of_range_subset.SInvSection.main

Source context 6 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace S_AlgebraicGeometry_RelPicard_isInvertible_sectionIdeal_of_range_subset
universe u
namespace SInvSection
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra

Lean source · statement

theorem main
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsSeparated c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (U : C.Opens) [SmoothOfRelativeDimension 1 (U.ι ≫ c)] (hεU : Set.range ε.1 ⊆ (U : Set C))
    {V : Scheme.{u}} (u : V ⟶ Spec (CommRingCat.of R)) :
    (sectionIdeal c ε u).IsInvertible

theorem

isInvertible_sectionIdeal_of_range_subset

L104 ↗

AlgebraicGeometry.RelPicard.isInvertible_sectionIdeal_of_range_subset

Source context 5 commands