Theorems · Definition · algebraic geometry

Module.Grassmannian.functor

{R : Type u} →
  [inst : CommRing R] →
    {M : Type v} → [inst_1 : AddCommGroup M] → [Module R M] → ℕ → CategoryTheory.Functor (CommAlgCat R) (Type (max v w))

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

Defined in

Mathlib.RingTheory.Grassmannian

Cited by

2 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModule