NYLL
Module

Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank
7 declarations indexed from sourceView source ↗

Module documentation

Vanishing of exterior powers above the rank

Exterior powers of a locally free module sheaf vanish in degrees greater than its rank.

Imports4
Imported by2

Declarations

lemma

isEmpty_powersetCard_fin_of_lt

L41 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank.exteriorPower.isEmpty_powersetCard_fin_of_lt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
    PresheafOfModules.pushforwardNatTrans_app_app_apply
    PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace exteriorPower
open _root_.exteriorPower
open _root_.exteriorPower
Lean source · statement
lemma isEmpty_powersetCard_fin_of_lt {n m : ℕ} (h : n < m) : IsEmpty (Set.powersetCard (Fin n) m)
lemma

subsingleton_pi_of_lt

L48 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank.exteriorPower.subsingleton_pi_of_lt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
    PresheafOfModules.pushforwardNatTrans_app_app_apply
    PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace exteriorPower
open _root_.exteriorPower
open _root_.exteriorPower
Lean source · statement
lemma subsingleton_pi_of_lt (A : Type u) [CommRing A] {n m : ℕ} (h : n < m) :
    Subsingleton (⋀[A]^m (Fin n → A))
lemma

isZero_of_subsingleton

L61 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank.PresheafOfModules.isZero_of_subsingleton
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
    PresheafOfModules.pushforwardNatTrans_app_app_apply
    PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u})
Lean source · statement
lemma isZero_of_subsingleton {S : Cᵒᵖ ⥤ RingCat.{u}} (P : PresheafOfModules.{u} S)
    (h : ∀ X : Cᵒᵖ, Subsingleton (P.obj X)) : IsZero P
lemma

isZero_exteriorPower_piPow

L68 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank.PresheafOfModules.isZero_exteriorPower_piPow
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
    PresheafOfModules.pushforwardNatTrans_app_app_apply
    PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u})
Lean source · statement
lemma isZero_exteriorPower_piPow {n m : ℕ} (h : n < m) :
    IsZero ((exteriorPowerFunctor R m).obj ((open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
        Scheme_Modules_nonempty_exteriorPower_free_iso_unit.PresheafOfModules.piPow R n)))
lemma

isZero_exteriorPower_free_of_lt

L89 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank.AlgebraicGeometry.Scheme.Modules.isZero_exteriorPower_free_of_lt
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
    PresheafOfModules.pushforwardNatTrans_app_app_apply
    PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace
variable (X : Scheme.{u})
Lean source · statement
lemma isZero_exteriorPower_free_of_lt {n m : ℕ} (h : n < m) :
    IsZero ((exteriorPower X m).obj (SheafOfModules.free.{u} (ULift.{u} (Fin n))))
theorem

isZero_exteriorPower_of_isLocallyFreeOfRank

L105 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank.AlgebraicGeometry.Scheme.Modules.isZero_exteriorPower_of_isLocallyFreeOfRank
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
    PresheafOfModules.pushforwardNatTrans_app_app_apply
    PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace
variable (X : Scheme.{u})
variable {X}
Lean source · statement
theorem isZero_exteriorPower_of_isLocallyFreeOfRank {n m : ℕ} {M : X.Modules}
    (hM : IsLocallyFreeOfRank n M) (h : n < m) : IsZero ((exteriorPower X m).obj M)
theorem

isZero_exteriorPower_of_isLocallyFreeOfRank

L117 ↗
AlgebraicGeometry.Scheme.Modules.isZero_exteriorPower_of_isLocallyFreeOfRank
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
    PresheafOfModules.pushforwardNatTrans_app_app_apply
    PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry in
open Scheme_Modules_isZero_exteriorPower_of_isLocallyFreeOfRank.AlgebraicGeometry.Scheme in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.isZero_exteriorPower_of_isLocallyFreeOfRank
    {X : Scheme.{u}} {n m : ℕ} {M : X.Modules}
    (hM : Scheme.Modules.IsLocallyFreeOfRank n M) (h : n < m) :
    Limits.IsZero ((Scheme.Modules.exteriorPower X m).obj M)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.