Grassmannians #
Main definitions #
Module.Grassmannian:G(k, M; R)is thekᵗʰ Grassmannian of theR-moduleM. It is defined to be the set of submodules ofMwhose quotient is locally free of rankk. Note that this indexing is the opposite of some indexing in literature, where this rank would ben-kinstead, whereM=R^n.
TODO #
- Grassmannians for schemes and quasi-coherent sheaf of modules.
- Representability.
@[simp]
theorem
Module.Grassmannian.coe_mk
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
(N : Submodule R M)
{h₁ : Module.Finite R (M ⧸ N)}
{h₂ : Projective R (M ⧸ N)}
{h₃ : ∀ (p : PrimeSpectrum R), rankAtStalk (M ⧸ N) p = k}
:
{ toSubmodule := N, finite_quotient := h₁, projective_quotient := h₂, rankAtStalk_eq := h₃ }.toSubmodule = N
def
Module.Grassmannian.mk'
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
(N : Submodule R M)
(P : Type u_1)
[AddCommGroup P]
[Module R P]
(e : (M ⧸ N) ≃ₗ[R] P)
[Module.Finite R P]
[Projective R P]
(h : ∀ (p : PrimeSpectrum R), rankAtStalk P p = k := by intro p; haveI := PrimeSpectrum.nontrivial p; simp)
:
Grassmannian R M k
An easier constructor that uses a linear equiv and instances.
Equations
- Module.Grassmannian.mk' N P e h = { toSubmodule := N, finite_quotient := ⋯, projective_quotient := ⋯, rankAtStalk_eq := ⋯ }
Instances For
@[simp]
theorem
Module.Grassmannian.coe_mk'
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
(N : Submodule R M)
(P : Type u_1)
[AddCommGroup P]
[Module R P]
[Module.Finite R P]
[Projective R P]
(e : (M ⧸ N) ≃ₗ[R] P)
(h : ∀ (p : PrimeSpectrum R), rankAtStalk P p = k)
:
def
Module.Grassmannian.copy
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
(N : Grassmannian R M k)
(N' : Set M)
(h : N' = ↑N.toSubmodule)
:
Grassmannian R M k
Copy of an element of the Grassmannian, with a new carrier equal to the old one. Useful to fix definitional equalities.
Equations
- N.copy N' h = Module.Grassmannian.mk' (N.copy N' h) (M ⧸ N.toSubmodule) ((N.copy N' h).quotEquivOfEq N.toSubmodule ⋯) ⋯
Instances For
def
Module.Grassmannian.ofEquiv
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
(N : Submodule R M)
(e : (M ⧸ N) ≃ₗ[R] Fin k → R)
:
Grassmannian R M k
Given an isomorphism M⧸N ↠ R^k, return an element of G(k, M; R).
Equations
- Module.Grassmannian.ofEquiv N e = Module.Grassmannian.mk' N (Fin k → R) e ⋯
Instances For
def
Module.Grassmannian.ofSurjective
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
(f : M →ₗ[R] Fin k → R)
(hf : Function.Surjective ⇑f)
:
Grassmannian R M k
Given a surjection M ↠ R^k, return an element of G(k, M; R).
Equations
Instances For
@[simp]
theorem
Module.Grassmannian.coe_ofSurjective
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
(f : M →ₗ[R] Fin k → R)
(hf : Function.Surjective ⇑f)
:
def
Module.Grassmannian.ofLinearMap
{R : Type u}
[CommRing R]
{k : ℕ}
{M₁ : Type u_1}
{M₂ : Type u_2}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
(f : M₁ →ₗ[R] M₂)
(hf : Function.Surjective ⇑f)
(N : Grassmannian R M₂ k)
:
Grassmannian R M₁ k
If M₁ surjects to M₂, then there is an induced map G(k, M₂; R) → G(k, M₁; R) by
"pulling back" a submodule.
Equations
- Module.Grassmannian.ofLinearMap f hf N = Module.Grassmannian.mk' (Submodule.comap f N.toSubmodule) (M₂ ⧸ N.toSubmodule) (Submodule.quotientComapLinearEquiv f hf N.toSubmodule) ⋯
Instances For
@[simp]
theorem
Module.Grassmannian.coe_ofLinearMap
{R : Type u}
[CommRing R]
{k : ℕ}
{M₁ : Type u_1}
{M₂ : Type u_2}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
(f : M₁ →ₗ[R] M₂)
(hf : Function.Surjective ⇑f)
(N : Grassmannian R M₂ k)
:
def
Module.Grassmannian.ofLinearEquiv
{R : Type u}
[CommRing R]
{k : ℕ}
{M₁ : Type u_1}
{M₂ : Type u_2}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
(e : M₁ ≃ₗ[R] M₂)
:
If M₁ and M₂ are isomorphic, then G(k, M₁; R) ≃ G(k, M₂; R).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Module.Grassmannian.coe_ofLinearEquiv
{R : Type u}
[CommRing R]
{k : ℕ}
{M₁ : Type u_1}
{M₂ : Type u_2}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
(e : M₁ ≃ₗ[R] M₂)
(N : Grassmannian R M₁ k)
:
def
Module.Grassmannian.ofLinearEquivEquiv
{R : Type u}
[CommRing R]
{k : ℕ}
{M₁ : Type u_1}
{M₂ : Type u_2}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
(e : M₁ ≃ₗ[R] M₂)
(N : Grassmannian R M₁ k)
:
The quotients of ofLinearEquiv are isomorphic.
Equations
Instances For
def
Module.Grassmannian.chart
(R : Type u)
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
(x : Fin k → M)
:
Set (Grassmannian R M k)
The affine chart corresponding to a chosen x : R^k → M, represented by k elements in M.
It is the quotients q : M ↠ V such that the composition x ∘ q : R^k → V is an isomorphism.
Equations
- Module.Grassmannian.chart R x = {N : Module.Grassmannian R M k | Function.Bijective (⇑N.mkQ ∘ ⇑(Fintype.linearCombination R x))}
Instances For
noncomputable def
Module.Grassmannian.equivOfChart
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
{x : Fin k → M}
{N : Grassmannian R M k}
(hn : N ∈ chart R x)
:
An element N ∈ chart R f produces an isomorphism M ⧸ N ≃ₗ[R] R^k.
Equations
Instances For
@[simp]
theorem
Module.Grassmannian.equivOfChart_apply
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
{x : Fin k → M}
{N : Grassmannian R M k}
(hn : N ∈ chart R x)
(i : Fin k)
:
@[simp]
theorem
Module.Grassmannian.equivOfChart_apply_apply
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
{x : Fin k → M}
{N : Grassmannian R M k}
(hn : N ∈ chart R x)
(i j : Fin k)
:
theorem
Module.Grassmannian.ofSurjective_mem_chart
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
{q : M →ₗ[R] Fin k → R}
(hq : Function.Surjective ⇑q)
(f : Fin k → M)
(hf : ∀ (i : Fin k), q (f i) = Pi.single i 1)
:
theorem
Module.Grassmannian.exists_ofSurjective_mem_chart
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
{q : M →ₗ[R] Fin k → R}
(hq : Function.Surjective ⇑q)
:
∃ (f : Fin k → M), ofSurjective q hq ∈ chart R f
noncomputable def
Module.Grassmannian.baseChange
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
(A : Type u_4)
[CommRing A]
[Algebra R A]
(N : Grassmannian R M k)
:
Grassmannian A (TensorProduct R A M) k
Base change to an R-algebra A, where M is replaced with A ⊗[R] M.
Equations
- Module.Grassmannian.baseChange A N = Module.Grassmannian.mk' (Submodule.baseChange A N.toSubmodule) (TensorProduct R A (M ⧸ N.toSubmodule)) (Submodule.quotientBaseChange A N.toSubmodule) ⋯
Instances For
@[simp]
theorem
Module.Grassmannian.coe_baseChange
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
(A : Type u_4)
[CommRing A]
[Algebra R A]
(N : Grassmannian R M k)
:
noncomputable def
Module.Grassmannian.quotientBaseChangeEquiv
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
(A : Type u_4)
[CommRing A]
[Algebra R A]
(N : Grassmannian R M k)
:
The quotient of baseChange is isomorphic to the base change of the quotient.
Equations
Instances For
noncomputable def
Module.Grassmannian.map
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
{A : Type u_4}
[CommRing A]
[Algebra R A]
{B : Type u_5}
[CommRing B]
[Algebra R B]
(f : A →ₐ[R] B)
(N : Grassmannian A (TensorProduct R A M) k)
:
Grassmannian B (TensorProduct R B M) k
Functoriality of Grassmannian in the category of R-algebras. Note that given an R-algebra
A, we replace M with A ⊗[R] M. The map f : A →ₐ[R] B should technically provide an instance
[Algebra A B], but this might cause problems later down the line, so we do not require this
instance in the type signature of the function. Instead, given any instance [Algebra A B], we
later prove that the map is equal to the one induced by IsScalarTower.toAlgHom R A B : A →ₐ[R] B.
See map_val and map_eq.
Equations
Instances For
theorem
Module.Grassmannian.coe_map
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
{A : Type u_4}
[CommRing A]
[Algebra R A]
{B : Type u_5}
[CommRing B]
[Algebra R B]
(f : A →ₐ[R] B)
(N : Grassmannian A (TensorProduct R A M) k)
:
theorem
Module.Grassmannian.coe_map'
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
{A : Type u_4}
[CommRing A]
[Algebra R A]
{B : Type u_5}
[CommRing B]
[Algebra R B]
(f : A →ₐ[R] B)
(N : Grassmannian A (TensorProduct R A M) k)
:
(map f N).toSubmodule = Submodule.span B ↑(Submodule.map (LinearMap.rTensor M f.toLinearMap) (Submodule.restrictScalars R N.toSubmodule))
theorem
Module.Grassmannian.map_eq
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
{A : Type u_4}
[CommRing A]
[Algebra R A]
{B : Type u_5}
[CommRing B]
[Algebra R B]
[Algebra A B]
[IsScalarTower R A B]
(N : Grassmannian A (TensorProduct R A M) k)
:
map (IsScalarTower.toAlgHom R A B) N = (ofLinearEquiv (TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B M)) (baseChange B N)
theorem
Module.Grassmannian.map_id
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
{A : Type u_4}
[CommRing A]
[Algebra R A]
(N : Grassmannian A (TensorProduct R A M) k)
:
theorem
Module.Grassmannian.map_comp
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
{A : Type u_4}
[CommRing A]
[Algebra R A]
{B : Type u_5}
[CommRing B]
[Algebra R B]
{C : Type u_6}
[CommRing C]
[Algebra R C]
(f : A →ₐ[R] B)
(g : B →ₐ[R] C)
(N : Grassmannian A (TensorProduct R A M) k)
:
noncomputable def
Module.Grassmannian.functor
(R : CommRingCat)
(M : ModuleCat ↑R)
(k : ℕ)
:
CategoryTheory.Functor (CategoryTheory.Under R) (Type (max u v))
The Grassmannian functor given a ring R, an R-module M, and a natural number k.
Given an R-algebra A, we return the set G(k, A ⊗[R] M; A).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Module.Grassmannian.functor_obj
(R : CommRingCat)
(M : ModuleCat ↑R)
(k : ℕ)
(A : CategoryTheory.Under R)
:
@[simp]
theorem
Module.Grassmannian.functor_map_carrier
(R : CommRingCat)
(M : ModuleCat ↑R)
(k : ℕ)
{X✝ Y✝ : CategoryTheory.Under R}
(f : X✝ ⟶ Y✝)
(N : Grassmannian (↑X✝.right) (TensorProduct ↑R ↑X✝.right ↑M) k)
:
((functor R M k).map f N).carrier = ⇑(TensorProduct.AlgebraTensorModule.cancelBaseChange ↑R ↑X✝.right ↑Y✝.right ↑Y✝.right ↑M).symm ⁻¹' ↑(Submodule.baseChange (↑Y✝.right) N.toSubmodule)
theorem
Module.Grassmannian.baseChange_mem_chart
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
{A : Type u_4}
[CommRing A]
[Algebra R A]
(f : Fin k → M)
{N : Grassmannian R M k}
(hn : N ∈ chart R f)
:
Functoriality of chart.
theorem
Module.Grassmannian.map_mem_chart
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
{A : Type u_4}
[CommRing A]
[Algebra R A]
{B : Type u_5}
[CommRing B]
[Algebra R B]
(f : A →ₐ[R] B)
(x : Fin k → M)
{N : Grassmannian A (TensorProduct R A M) k}
(hn : N ∈ chart A (⇑((TensorProduct.mk R A M) 1) ∘ x))
:
Functoriality of chart.
noncomputable def
Module.Grassmannian.chartFunctor
(R : CommRingCat)
(M : ModuleCat ↑R)
(k : ℕ)
(x : Fin k → ↑M)
:
CategoryTheory.Functor (CategoryTheory.Under R) (Type (max u v))
A subfunctor of the Grassmannian, given an indexing x : Fin k → M, chart x selects the
elements N ∈ G(k, A ⊗[R] M; A) such that the composition A^k → A ⊗[R] M → (A ⊗[R] M)/N.val is
an isomorphism. This is called chart because it corresponds to an affine open chart in the
Grassmannian.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Module.Grassmannian.chartFunctor_obj
(R : CommRingCat)
(M : ModuleCat ↑R)
(k : ℕ)
(x : Fin k → ↑M)
(A : CategoryTheory.Under R)
:
@[simp]
theorem
Module.Grassmannian.chartFunctor_map_coe_carrier
(R : CommRingCat)
(M : ModuleCat ↑R)
(k : ℕ)
(x : Fin k → ↑M)
{X✝ Y✝ : CategoryTheory.Under R}
(f : X✝ ⟶ Y✝)
(N : ↑(chart (↑X✝.right) (⇑((TensorProduct.mk ↑R ↑X✝.right ↑M) 1) ∘ x)))
:
(↑((chartFunctor R M k x).map f N)).carrier = ⇑(TensorProduct.AlgebraTensorModule.cancelBaseChange ↑R ↑X✝.right ↑Y✝.right ↑Y✝.right ↑M).symm ⁻¹' ↑(Submodule.baseChange (↑Y✝.right) (↑N).toSubmodule)
noncomputable def
Module.Grassmannian.chartToFunctor
(R : CommRingCat)
(M : ModuleCat ↑R)
(k : ℕ)
(x : Fin k → ↑M)
:
chartFunctor R M k x is a subfunctor of Grassmannian.functor R M k.
Equations
- Module.Grassmannian.chartToFunctor R M k x = { app := fun (A : CategoryTheory.Under R) => Subtype.val, naturality := ⋯ }
Instances For
Corepresentability of chart #
We show that chart x is the equalizer of Hom[R](M, R^k) ⥤ Hom[R](R^k, R^k).
We call Hom[R](M, R^k) "left" and Hom[R](R^k, R^k) "right".
@[reducible, inline]
abbrev
Module.Grassmannian.Corepresentable.left
(R : Type u)
[CommRing R]
(M : Type v)
[AddCommGroup M]
[Module R M]
(k : ℕ)
:
Type (max u v)
The first module in the equaliser diagram.
Equations
- Module.Grassmannian.Corepresentable.left R M k = (M →ₗ[R] Fin k → R)
Instances For
def
Module.Grassmannian.Corepresentable.compose
(R : Type u)
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
(x : Fin k → M)
:
Equations
Instances For
def
Module.Grassmannian.Corepresentable.const1
(R : Type u)
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
:
Equations
Instances For
noncomputable def
Module.Grassmannian.Corepresentable.chartEquivEq
(R : Type u)
[CommRing R]
(M : Type v)
[AddCommGroup M]
[Module R M]
(k : ℕ)
(x : Fin k → M)
:
The isomorphism between chart x and the equaliser of compose, const1 : left ⟶ right.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Module.Grassmannian.Corepresentable.leftBaseChange
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
(A : Type u_4)
[CommRing A]
[Algebra R A]
(f : left R M k)
:
left A (TensorProduct R A M) k
Base change of left from R to A.
Equations
Instances For
def
Module.Grassmannian.Corepresentable.leftMap
(R : Type u)
[CommRing R]
(M : Type v)
[AddCommGroup M]
[Module R M]
(k : ℕ)
{A : Type u_4}
[CommRing A]
[Algebra R A]
{B : Type u_5}
[CommRing B]
[Algebra R B]
(φ : A →ₐ[R] B)
(f : left A (TensorProduct R A M) k)
:
left B (TensorProduct R B M) k
Base change of left from A to B.
Equations
Instances For
@[simp]
theorem
Module.Grassmannian.Corepresentable.leftMap_tmul
{R : Type u}
[CommRing R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{k : ℕ}
{A : Type u_4}
[CommRing A]
[Algebra R A]
{B : Type u_5}
[CommRing B]
[Algebra R B]
(φ : A →ₐ[R] B)
(f : left A (TensorProduct R A M) k)
(a : A)
(m : M)
(i : Fin k)
:
@[simp]
@[simp]
def
Module.Grassmannian.Corepresentable.leftFunctor
(R : CommRingCat)
(M : ModuleCat ↑R)
(k : ℕ)
:
CategoryTheory.Functor (CategoryTheory.Under R) (Type (max u v))
left as a functor.
Equations
- One or more equations did not get rendered due to their size.