Module

RigidifiedLineBundle_nonempty_ofInvertible_L_iso_of_field.lean

Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_nonempty_ofInvertible_L_iso_of_field

3 declarations indexed from sourceView source ↗

Module documentation

Over a field, rigidifying an invertible module preserves its underlying line bundle up to isomorphism.

Imports16

Mathlib.CategoryTheory.Iso
Mathlib.CategoryTheory.Functor.Basic
Mathlib.CategoryTheory.Monoidal.Category
Mathlib.CategoryTheory.Monoidal.Closed.Basic
Mathlib.CategoryTheory.Category.Preorder
Mathlib.CategoryTheory.Opposites
Mathlib.Topology.Sets.Opens
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.Order.CompleteLattice.Basic
Mathlib.Tactic.Ext
Nyll.AlgebraicCurves.Geometry.Schemes.RigidifiedLineBundleOfInvertible
Nyll.SchemeTheory.Modules.TensorSections
Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesIhomSections
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_isFrameOn
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_of_isFrameOn_of_iSup_eq_top

Imported by1

Nyll.JacobianVarieties.Picard.All

theorem

nonempty_iso_unit_of_isFrameOn_top

L56 ↗

JacobianVarieties.Picard.Proofs.RigidificationOverField.R2Aux.nonempty_iso_unit_of_isFrameOn_top

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RigidificationOverField
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.RelPicard NeronModelInfra
namespace R2Aux
open AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem nonempty_iso_unit_of_isFrameOn_top {X : Scheme.{u}} {N : X.Modules} (s : Γ(N, ⊤))
    (hs : IsFrameOn s ⊤) : Nonempty (N ≅ 𝟙_ X.Modules)

theorem

nonempty_iso_unit_of_field

L76 ↗

JacobianVarieties.Picard.Proofs.RigidificationOverField.R2Aux.nonempty_iso_unit_of_field

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RigidificationOverField
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.RelPicard NeronModelInfra
namespace R2Aux
open AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem nonempty_iso_unit_of_field {K : Type u} [Field K] {N : (Spec (CommRingCat.of K)).Modules}
    (hN : IsInvertible N) : Nonempty (N ≅ 𝟙_ (Spec (CommRingCat.of K)).Modules)

theorem

nonempty_ofInvertible_L_iso_of_field

L89 ↗

AlgebraicGeometry.RelPicard.RigidifiedLineBundle.nonempty_ofInvertible_L_iso_of_field

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RigidificationOverField
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.RelPicard NeronModelInfra

Lean source · statement

theorem _root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundle.nonempty_ofInvertible_L_iso_of_field
    {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
    {K : Type u} [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of R))
    {L : (pullback c t).Modules} (hL : Scheme.Modules.IsInvertible L) :
    Nonempty ((RigidifiedLineBundle.ofInvertible (ε := ε) L hL).L ≅ L)

Module documentation

Declarations

nonempty_iso_unit_of_isFrameOn_top

nonempty_iso_unit_of_field

nonempty_ofInvertible_L_iso_of_field