Module

Scheme_Modules_finrank_baseChange_sections_eq_one_of_locallyTrivial.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_finrank_baseChange_sections_eq_one_of_locallyTrivial

1 declaration indexed from sourceView source ↗

Module documentation

Rank-one fibers of locally trivial module sections

Shows that sections of a locally trivial module have rank-one fibers after field base change.

Imports4

Imported by5

theorem

finrank_baseChange_sections_eq_one_of_locallyTrivial

L36 ↗

AlgebraicGeometry.Scheme.Modules.finrank_baseChange_sections_eq_one_of_locallyTrivial

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_finrank_baseChange_sections_eq_one_of_locallyTrivial
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
noncomputable section

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.finrank_baseChange_sections_eq_one_of_locallyTrivial
    {X : Scheme.{u}} (M : X.Modules)
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
    (U : X.affineOpens) (K : Type u) [Field K] [Algebra Γ(X, U.1) K] :
    Module.finrank K (K ⊗[Γ(X, U.1)] Γ(M, U.1)) = 1

Module documentation

Rank-one fibers of locally trivial module sections

Declarations

finrank_baseChange_sections_eq_one_of_locallyTrivial