Module

Scheme_Modules_epi_whiskerRight_wedgeVec_of_shortExact.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_epi_whiskerRight_wedgeVec_of_shortExact

3 declarations indexed from sourceView source ↗

Module documentation

Exterior powers of a short exact sequence

Shows that wedging the exterior power of the first map with the middle module is epimorphic when the quotient is invertible.

Imports12

Imported by2

lemma

ιMulti_comp_mem

L59 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_epi_whiskerRight_wedgeVec_of_shortExact.AlgebraicGeometry.Scheme.Modules.ιMulti_comp_mem

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_epi_whiskerRight_wedgeVec_of_shortExact
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory.MonoidalCategory
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
variable {X : Scheme.{u}}

Lean source · statement

lemma ιMulti_comp_mem {A : Type u} [CommRing A] {M : Type u} [AddCommGroup M] [Module A M] {m : ℕ}
    (w : Fin m → M) (P : Submodule A (⋀[A]^m M)) (hP : exteriorPower.ιMulti A m w ∈ P)
    (φ : Fin m → Fin m) : exteriorPower.ιMulti A m (w ∘ φ) ∈ P

lemma

exteriorPower_le_of_span_eq_top

L76 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_epi_whiskerRight_wedgeVec_of_shortExact.AlgebraicGeometry.Scheme.Modules.exteriorPower_le_of_span_eq_top

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_epi_whiskerRight_wedgeVec_of_shortExact
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory.MonoidalCategory
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
variable {X : Scheme.{u}}

Lean source · statement

lemma exteriorPower_le_of_span_eq_top {A : Type u} [CommRing A] {M : Type u} [AddCommGroup M]
  [Module A M] {m : ℕ}
    (w : Fin m → M) (hw : Submodule.span A (Set.range w) = ⊤) (P : Submodule A (⋀[A]^m M))
    (hP : exteriorPower.ιMulti A m w ∈ P) : ⊤ ≤ P

theorem

epi_whiskerRight_wedgeVec_of_shortExact

L88 ↗

AlgebraicGeometry.Scheme.Modules.epi_whiskerRight_wedgeVec_of_shortExact

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_epi_whiskerRight_wedgeVec_of_shortExact
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry.Scheme.Modules in
with_weak_namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.epi_whiskerRight_wedgeVec_of_shortExact {X :
  Scheme.{u}} {n : ℕ} (S : ShortComplex X.Modules) (hS : S.ShortExact)
    (h₁ : Scheme.Modules.IsLocallyFreeOfRank n S.X₁) (h₃ : Scheme.Modules.IsInvertible S.X₃) :
    Epi (((Scheme.Modules.exteriorPower X n).map S.f ▷ S.X₂) ≫ Scheme.Modules.wedgeVec n S.X₂)

Module documentation

Exterior powers of a short exact sequence

Declarations

ιMulti_comp_mem

exteriorPower_le_of_span_eq_top

epi_whiskerRight_wedgeVec_of_shortExact