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.

• Module.Grassmannian.functor: The Grassmannian functor that sends an R-algebra A to the set G(k, A ⊗[R] M; A).

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 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.

@[implicit_reducible]

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

def Module.Grassmannian.baseChangeMkQ {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {A : Type w} [CommRing A] [Algebra R A] (B : Type w) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (N : Submodule A (TensorProduct R A M)) : TensorProduct R B M →ₗ[B] TensorProduct A B (TensorProduct R A M ⧸ N)

The surjective B-linear map B ⊗[R] M → B ⊗[A] ((A ⊗[R] M) ⧸ N) obtained as the base change of N.mkQ along A → B

Equations

• Module.Grassmannian.baseChangeMkQ B N = LinearMap.baseChange B N.mkQ ∘ₗ ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B M).symm

theorem Module.Grassmannian.baseChangeMkQ_surjective {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {A : Type w} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (N : Submodule A (TensorProduct R A M)) : Function.Surjective ⇑(baseChangeMkQ B N)

noncomputable def Module.Grassmannian.baseChangeMkQEquiv {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {A : Type w} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (N : Submodule A (TensorProduct R A M)) : (TensorProduct R B M ⧸ (baseChangeMkQ B N).ker) ≃ₗ[B] TensorProduct A B (TensorProduct R A M ⧸ N)

The B-linear equivalence (B ⊗[R] M) ⧸ ker (baseChangeMkQ N) ≃ₗ[B] B ⊗[A] ((A ⊗[R] M) ⧸ N) underlying Module.Grassmannian.map.

Equations

• Module.Grassmannian.baseChangeMkQEquiv N = (Module.Grassmannian.baseChangeMkQ B N).quotKerEquivOfSurjective ⋯

def Module.Grassmannian.map {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {k : ℕ} {A : Type w} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (f : A →ₐ[R] B) (N : Grassmannian A (TensorProduct R A M) k) : Grassmannian B (TensorProduct R B M) k

The map on Grassmannians induced by base change along an algebra map A → B. Given a submodule N of A ⊗[R] M, the image is the kernel of the composition B ⊗[R] M ≃ B ⊗[A] (A ⊗[R] M) → B ⊗[A] ((A ⊗[R] M) ⧸ N)`.

Equations

• Module.Grassmannian.map f N = { toSubmodule := (Module.Grassmannian.baseChangeMkQ B N.toSubmodule).ker, finite_quotient := ⋯, projective_quotient := ⋯, rankAtStalk_eq := ⋯ }

theorem Module.Grassmannian.map_toSubmodule {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {k : ℕ} {A : Type w} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (f : A →ₐ[R] B) (N : Grassmannian A (TensorProduct R A M) k) : (map f N).toSubmodule = (baseChangeMkQ B N.toSubmodule).ker

@[simp]

theorem Module.Grassmannian.map_id {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (k : ℕ) (A : CommAlgCat R) (N : Grassmannian (↑A) (TensorProduct R (↑A) M) k) : map (AlgHom.id R ↑A) N = N

theorem Module.Grassmannian.map_comp {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (k : ℕ) {A : Type w} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (f : A →ₐ[R] B) {C : Type w} [CommRing C] [Algebra R C] (g : B →ₐ[R] C) (N : Grassmannian A (TensorProduct R A M) k) : map (g.comp f) N = map g (map f N)

def Module.Grassmannian.functor {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (k : ℕ) : CategoryTheory.Functor (CommAlgCat R) (Type (max v w))

The Grassmannian functor sends an R-algebra A to G(k, A ⊗[R] M; A).

Equations

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

@[simp]

theorem Module.Grassmannian.functor_map {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (k : ℕ) {X✝ Y✝ : CommAlgCat R} (f : X✝ ⟶ Y✝) : (functor k).map f = TypeCat.ofHom (map (CommAlgCat.Hom.hom f))

@[simp]

theorem Module.Grassmannian.functor_obj {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (k : ℕ) (A : CommAlgCat R) : (functor k).obj A = Grassmannian (↑A) (TensorProduct R (↑A) M) k