AlgebraicGeometry.Scheme.TwoAffineOpenCover.sectionsOf_isInvertible_projective_finite_finrank
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_sectionsOf_isInvertible_projective_finite_finrank
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
noncomputable sectionLean source · statement
theorem
_root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.sectionsOf_isInvertible_projective_finite_finrank
{R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
(M : X.Modules) (hM : Scheme.Modules.IsInvertible M) :
Module.Projective (𝒱.cover c).A0 (𝒱.sectionsOf c M).M0 ∧
Module.Finite (𝒱.cover c).A0 (𝒱.sectionsOf c M).M0 ∧
(∀ (K : Type u) [Field K] [Algebra (𝒱.cover c).A0 K],
Module.finrank K (K ⊗[(𝒱.cover c).A0] (𝒱.sectionsOf c M).M0) = 1) ∧
Module.Projective (𝒱.cover c).A1 (𝒱.sectionsOf c M).M1 ∧
Module.Finite (𝒱.cover c).A1 (𝒱.sectionsOf c M).M1 ∧
(∀ (K : Type u) [Field K] [Algebra (𝒱.cover c).A1 K],
Module.finrank K (K ⊗[(𝒱.cover c).A1] (𝒱.sectionsOf c M).M1) = 1) ∧
Module.Projective (𝒱.cover c).A01 (𝒱.sectionsOf c M).M01 ∧
Module.Finite (𝒱.cover c).A01 (𝒱.sectionsOf c M).M01 ∧
(∀ (K : Type u) [Field K] [Algebra (𝒱.cover c).A01 K],
Module.finrank K (K ⊗[(𝒱.cover c).A01] (𝒱.sectionsOf c M).M01) = 1)