Module

Scheme_Modules_IsInvertible_nonempty_pullback_rigidify_iso.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_pullback_rigidify_iso

1 declaration indexed from sourceView source ↗

Module documentation

Base change of rigidification

Rigidification of an invertible module commutes with pullback along a compatible square of structure morphisms and sections.

Imports4

Imported by10

theorem

nonempty_pullback_rigidify_iso

L36 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.nonempty_pullback_rigidify_iso

Source context 7 commands

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

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

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.nonempty_pullback_rigidify_iso
    {T P T' P' : Scheme.{u}} {σ : T ⟶ P} {q : P ⟶ T} {σ' : T' ⟶ P'} {q' : P' ⟶ T'}
    (ψ : T' ⟶ T) (Ψ : P' ⟶ P) (hσ : σ' ≫ Ψ = ψ ≫ σ) (hq : Ψ ≫ q = q' ≫ ψ)
    {L : P.Modules} (hL : Scheme.Modules.IsInvertible L) :
    Nonempty ((Scheme.Modules.pullback Ψ).obj (Scheme.Modules.rigidify σ q L) ≅
      Scheme.Modules.rigidify σ' q' ((Scheme.Modules.pullback Ψ).obj L))

Module documentation

Base change of rigidification

Declarations

nonempty_pullback_rigidify_iso