Grassmannians

Main definitions

• Module.Grassmannian: G(k, M; R) is the kᵗʰ Grassmannian of the R-module M. It is defined to be the set of submodules of M whose quotient is locally free of rank k. Note that there is another convention in literature where the kᵗʰ Grassmannian would instead be k-dimensional subspaces of a given vector space over a field. See implementation notes below.

Implementation notes

In the literature, two conventions exist:

1. The kᵗʰ Grassmannian parametrises k-dimensional subspaces of a given finite dimensional vector space over a field.
2. The kᵗʰ Grassmannian parametrises quotients that are locally free of rank k, of a given module over a ring.

For the purposes of Algebraic Geometry, the first definition here cannot be generalised to obtain a scheme to represent the functor, which is why the second definition is the one chosen by Grothendieck, EGA I.9.7.3 (Springer edition only), and in EGA V.11 (unpublished).

The first definition in the stated generality (i.e. over a field F, and finite dimensional vector space V) can be recovered from the second definition by noting that k-dimensional subspaces of V are canonically equivalent to (n-k)-dimensional quotients of V, and also to k-dimensional quotients of V*, the dual of V. In symbols, this means that the first definition is equivalent to G(n - k, V; F) and also to G(k, V →ₗ[F] F; F), where n is the dimension of V.

TODO

• Define and recover the subspace-definition (i.e. the first definition above).
• Define the functor Module.Grassmannian.functor R M k that sends an R-algebra A to the set G(k, A ⊗[R] M; A).
• Define chart x indexed by x : Fin k → M as a subtype consisting of those N ∈ G(k, A ⊗[R] M; A) such that the composition R^k → M → M⧸N is an isomorphism.
• Define chartFunctor x to turn chart x into a subfunctor of Module.Grassmannian.functor. This will correspond to an affine open chart in the Grassmannian.
• Grassmannians for schemes and quasi-coherent sheaf of modules.
• Representability of Module.Grassmannian.functor R M k.

structure Module.Grassmannian (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] (k : ℕ) extends Submodule R M : Type v

G(k, M; R) is the kᵗʰ Grassmannian of the R-module M. It is defined to be the set of submodules of M whose quotient is locally free of rank k. Note that there is another convention in literature where instead the submodule is required to have rank k. See the module docstring of RingTheory.Grassmannian.

• carrier : Set M
• add_mem' {a b : M} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• smul_mem' (c : R) {x : M} : x ∈ self.carrier → c • x ∈ self.carrier
• finite_quotient : Module.Finite R (M ⧸ self.toSubmodule)
• projective_quotient : Projective R (M ⧸ self.toSubmodule)
• rankAtStalk_eq (p : PrimeSpectrum R) : rankAtStalk (M ⧸ self.toSubmodule) p = k

def Module.Grassmannian.«termG(_,_;_)» : Lean.ParserDescr

G(k, M; R) is the kᵗʰ Grassmannian of the R-module M. It is defined to be the set of submodules of M whose quotient is locally free of rank k. Note that there is another convention in literature where instead the submodule is required to have rank k. See the module docstring of RingTheory.Grassmannian.

Equations

• One or more equations did not get rendered due to their size.

instance Module.Grassmannian.instCoeOutSubmodule {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {k : ℕ} : CoeOut (Grassmannian R M k) (Submodule R M)

Equations

• Module.Grassmannian.instCoeOutSubmodule = { coe := Module.Grassmannian.toSubmodule }

theorem Module.Grassmannian.ext {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {k : ℕ} {N₁ N₂ : Grassmannian R M k} (h : N₁.toSubmodule = N₂.toSubmodule) : N₁ = N₂

theorem Module.Grassmannian.ext_iff {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {k : ℕ} {N₁ N₂ : Grassmannian R M k} : N₁ = N₂ ↔ N₁.toSubmodule = N₂.toSubmodule