Module

Scheme_Modules_IsInvertible_rigidify.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_rigidify

1 declaration indexed from sourceView source ↗

Module documentation

Rigidifying an invertible module

Rigidification along a section preserves invertibility and identifies the original module with the rigidified module tensored with the pullback of its value along the section.

Imports5

Imported by5

theorem

rigidify

L36 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.rigidify

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_rigidify
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.rigidify
    {T P : Scheme.{u}} {σ : T ⟶ P} {q : P ⟶ T} (hσq : σ ≫ q = 𝟙 T) {L : P.Modules}
    (hL : Scheme.Modules.IsInvertible L) :
    Scheme.Modules.IsInvertible (Scheme.Modules.rigidify σ q L) ∧
      Nonempty ((Scheme.Modules.pullback σ).obj (Scheme.Modules.rigidify σ q L) ≅ 𝟙_ T.Modules)

Module documentation

Rigidifying an invertible module

Declarations

rigidify