Module

Scheme_Modules_isInvertible_tilde_of_projective_rankOne.lean

Nyll.AlgebraicCurves.Geometry.Projective.Scheme_Modules_isInvertible_tilde_of_projective_rankOne

1 declaration indexed from sourceView source ↗

Module documentation

Scheme Modules is Invertible tilde of projective rank One

Imports4

Imported by2

theorem

isInvertible_tilde_of_projective_rankOne

L32 ↗

AlgebraicGeometry.Scheme.Modules.isInvertible_tilde_of_projective_rankOne

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_Modules_isInvertible_tilde_of_projective_rankOne
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory AlgebraicGeometry TensorProduct

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.isInvertible_tilde_of_projective_rankOne {R :
  CommRingCat.{u}} (P : ModuleCat.{u} R) [Module.Finite R P] [Module.Projective R P]
    (hrk : ∀ (K : Type u) [Field K] [Algebra R K], Module.finrank K (K ⊗[R] P) = 1) :
    Scheme.Modules.IsInvertible (tilde P)

Module documentation

Scheme Modules is Invertible tilde of projective rank One

Declarations

isInvertible_tilde_of_projective_rankOne