Module

Scheme_Modules_IsInvertible_nonempty_iso_unit_of_dualNumber_of_reduction.lean

Nyll.JacobianVarieties.Picard.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_dualNumber_of_reduction

1 declaration indexed from sourceView source ↗

Module documentation

Triviality of an invertible module over dual numbers

A trivial reduction lifts across the square-zero kernel of the dual-number projection.

Imports5

Mathlib.Algebra.DualNumber
Mathlib.Util.WithWeakNamespace
Mathlib.RingTheory.Ideal.Quotient.Operations
Nyll.AlgebraicCurves.Geometry.Picard.Functor
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_pullback_squareZero

Imported by5

theorem

nonempty_iso_unit_of_dualNumber_of_reduction

L37 ↗

AlgebraicGeometry.RelPicard.Scheme.Modules.IsInvertible.nonempty_iso_unit_of_dualNumber_of_reduction

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DualNumberReduction
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible
  (nonempty_iso_unit_of_pullback_squareZero) in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.Scheme.Modules.IsInvertible

Lean source · statement

theorem nonempty_iso_unit_of_dualNumber_of_reduction
    (Cr : Type u) [CommRing Cr] (M : (Spec (.of (DualNumber Cr))).Modules)
    (hM : Scheme.Modules.IsInvertible M)
    (h0 : Nonempty ((Scheme.Modules.pullback
      (Spec.map (CommRingCat.ofHom (TrivSqZeroExt.fstHom Cr Cr Cr).toRingHom))).obj M ≅
        SheafOfModules.unit.{u} (Spec (.of Cr)).ringCatSheaf)) :
    Nonempty (M ≅ SheafOfModules.unit.{u} (Spec (.of (DualNumber Cr))).ringCatSheaf)

Module documentation

Triviality of an invertible module over dual numbers

Declarations

nonempty_iso_unit_of_dualNumber_of_reduction