Projective Space of a Module over a Ring

Main definitions

• ProjectiveSpace.functor: the functor R-Alg ⥤ Set that sends A to ℙ(A ⊗[R] M; A).

@[reducible, inline]

abbrev Module.ProjectiveSpace.AsType (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] : Type v

The projective space corresponding to the module M is the space of submodules N such that M⧸N is locally free of rank 1, i.e. invertible.

Equations

• Module.ProjectiveSpace.AsType R M = Module.Grassmannian R M 1

def Module.ProjectiveSpace.«termℙ(_;_)» : Lean.ParserDescr

The projective space corresponding to the module M is the space of submodules N such that M⧸N is locally free of rank 1, i.e. invertible.

Equations

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

@[reducible, inline]

noncomputable abbrev Module.ProjectiveSpace.functor (R : CommRingCat) (M : ModuleCat ↑R) : CategoryTheory.Functor (CategoryTheory.Under R) (Type (max u v))

The functor R-Alg ⥤ Set that sends A to ℙ(A ⊗[R] M; A).

Equations

• Module.ProjectiveSpace.functor R M = Module.Grassmannian.functor R M 1

def Module.ProjectiveSpace.ofSurjective {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (f : M →ₗ[R] R) (hf : Function.Surjective ⇑f) : AsType R M

The element of ℙ(M; R) given by a surjection M →ₗ[R] R.`

Equations

• Module.ProjectiveSpace.ofSurjective f hf = Module.Grassmannian.ofSurjective (↑(LinearEquiv.funUnique (Fin 1) R R).symm ∘ₗ f) ⋯

@[simp]

theorem Module.ProjectiveSpace.ofSurjective_carrier {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (f : M →ₗ[R] R) (hf : Function.Surjective ⇑f) : (ofSurjective f hf).carrier = uniqueElim ∘ ⇑f ⁻¹' {0}

noncomputable def Module.ProjectiveSpace.quotientOfSurjectiveLinearEquiv {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (f : M →ₗ[R] R) (hf : Function.Surjective ⇑f) : (M ⧸ (ofSurjective f hf).toSubmodule) ≃ₗ[R] R

Equations

• Module.ProjectiveSpace.quotientOfSurjectiveLinearEquiv f hf = ((Module.ProjectiveSpace.ofSurjective f hf).quotEquivOfEq (LinearMap.ker f) ⋯).trans (f.quotKerEquivOfSurjective hf)

@[simp]

theorem Module.ProjectiveSpace.quotientOfSurjectiveLinearEquiv_comp_mkQ {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (f : M →ₗ[R] R) (hf : Function.Surjective ⇑f) : ↑(quotientOfSurjectiveLinearEquiv f hf) ∘ₗ (ofSurjective f hf).mkQ = f

def Module.ProjectiveSpace.ofCoordinates {R : Type u} [CommRing R] {ι : Type u_4} [Fintype ι] (x : ι → R) (hx : Ideal.span (Set.range x) = ⊤) : AsType R (ι → R)

Special case for ℙⁿ: it suffices to give n + 1 coordinates.

Equations

• Module.ProjectiveSpace.ofCoordinates x hx = Module.ProjectiveSpace.ofSurjective (Fintype.linearCombination R x) ⋯

@[simp]

theorem Module.ProjectiveSpace.ofCoordinates_carrier {R : Type u} [CommRing R] {ι : Type u_4} [Fintype ι] (x : ι → R) (hx : Ideal.span (Set.range x) = ⊤) : (ofCoordinates x hx).carrier = uniqueElim ∘ ⇑(Fintype.linearCombination R x) ⁻¹' {0}

noncomputable def Module.ProjectiveSpace.quotientOfCoordinatesLinearEquiv {R : Type u} [CommRing R] {ι : Type u_4} [Fintype ι] (x : ι → R) (hx : Ideal.span (Set.range x) = ⊤) : ((ι → R) ⧸ (ofCoordinates x hx).toSubmodule) ≃ₗ[R] R

Equations

• Module.ProjectiveSpace.quotientOfCoordinatesLinearEquiv x hx = Module.ProjectiveSpace.quotientOfSurjectiveLinearEquiv (Fintype.linearCombination R x) ⋯

@[simp]

theorem Module.ProjectiveSpace.quotientOfCoordinatesLinearEquiv_comp_mkQ {R : Type u} [CommRing R] {ι : Type u_4} [Fintype ι] (x : ι → R) (hx : Ideal.span (Set.range x) = ⊤) : ↑(quotientOfCoordinatesLinearEquiv x hx) ∘ₗ (ofCoordinates x hx).mkQ = Fintype.linearCombination R x

@[reducible, inline]

abbrev Module.ProjectiveSpace.chart (R : Type u) [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (x : M) : Set (AsType R M)

The affine chart indexed by x : M, consisting of those N such that there is an isomorphism M⧸N ≃ₗ[R] R, sending ⟦x⟧ to 1. Morally, this says "x is invertible".

Equations

• Module.ProjectiveSpace.chart R x = Module.Grassmannian.chart R fun (x_1 : Fin 1) => x

noncomputable def Module.ProjectiveSpace.equivOfChart {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (x : M) {N : AsType R M} (hn : N ∈ chart R x) : (M ⧸ N.toSubmodule) ≃ₗ[R] R

Given N ∈ chart R M x, we have an isomorphism M ⧸ N ≃ₗ[R] R sending x to 1.

Equations

• Module.ProjectiveSpace.equivOfChart x hn = (Module.Grassmannian.equivOfChart hn).trans (LinearEquiv.funUnique (Fin 1) R R)

theorem Module.ProjectiveSpace.equivOfChart_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (x : M) {N : AsType R M} (hn : N ∈ chart R x) : (equivOfChart x hn) (Submodule.Quotient.mk x) = 1

noncomputable def Module.ProjectiveSpace.div {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (y x : M) (p : ↑(chart R x)) : R

"Division by x" is well-defined on the chart where "x is invertible".

Equations

• Module.ProjectiveSpace.div y x p = (Module.ProjectiveSpace.equivOfChart x ⋯) (Submodule.Quotient.mk y)

theorem Module.ProjectiveSpace.add_div {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (y z x : M) : div (y + z) x = div y x + div z x

theorem Module.ProjectiveSpace.add_div_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (y z x : M) (p : ↑(chart R x)) : div (y + z) x p = div y x p + div z x p

theorem Module.ProjectiveSpace.smul_div {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (r : R) (y x : M) : div (r • y) x = r • div y x

theorem Module.ProjectiveSpace.smul_div_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (r : R) (y x : M) (p : ↑(chart R x)) : div (r • y) x p = r * div y x p

theorem Module.ProjectiveSpace.div_smul_self {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (y x : M) (p : ↑(chart R x)) : div y x p • Submodule.Quotient.mk x = Submodule.Quotient.mk y

theorem Module.ProjectiveSpace.div_self {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (x : M) : div x x = 1

theorem Module.ProjectiveSpace.div_self_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (x : M) (p : ↑(chart R x)) : div x x p = 1

theorem Module.ProjectiveSpace.div_mul_div_cancel {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (x y z : M) (p : ↑(chart R y ∩ chart R z)) : div x y ⟨↑p, ⋯⟩ * div y z ⟨↑p, ⋯⟩ = div x z ⟨↑p, ⋯⟩

theorem Module.ProjectiveSpace.div_mul_div_symm {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (x y : M) (p : ↑(chart R x ∩ chart R y)) : div x y ⟨↑p, ⋯⟩ * div y x ⟨↑p, ⋯⟩ = 1

@[reducible, inline]

noncomputable abbrev Module.ProjectiveSpace.chartFunctor (R : CommRingCat) (M : ModuleCat ↑R) (x : ↑M) : CategoryTheory.Functor (CategoryTheory.Under R) (Type (max u v))

chart x as a functor. A is sent to chart A (A ⊗[R] M) (1 ⊗ₜ x).

Equations

• Module.ProjectiveSpace.chartFunctor R M x = Module.Grassmannian.chartFunctor R M 1 fun (x_1 : Fin 1) => x

theorem Module.ProjectiveSpace.chartFunctor_obj (R : CommRingCat) (M : ModuleCat ↑R) (x : ↑M) (A : CategoryTheory.Under R) : (chartFunctor R M x).obj A = ↑(chart (↑A.right) (1 ⊗ₜ[↑R] x))

@[reducible, inline]

noncomputable abbrev Module.ProjectiveSpace.chartToFunctor (R : CommRingCat) (M : ModuleCat ↑R) (x : ↑M) : chartFunctor R M x ⟶ functor R M

chartFunctor as a subfunctor of ProjectiveSpace.functor.

Equations

• Module.ProjectiveSpace.chartToFunctor R M x = Module.Grassmannian.chartToFunctor R M 1 fun (x_1 : Fin 1) => x

def Module.ProjectiveSpace.zeros {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {n : ℕ} (f : SymmetricPower R M n) : Set (AsType R M)

V(f) the set of zeroes of the homogeneous polynomial f of degree n.

Equations

• Module.ProjectiveSpace.zeros f = {N : Module.ProjectiveSpace.AsType R M | (SymmetricPower.map n N.mkQ) f = 0}

theorem Module.ProjectiveSpace.zeros_def {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {n : ℕ} (f : SymmetricPower R M n) (p : AsType R M) : p ∈ zeros f ↔ (SymmetricPower.map n p.mkQ) f = 0

def Module.ProjectiveSpace.zerosOfCoordinates {R : Type u} [CommRing R] {ι : Type u_4} [Fintype ι] {n : ℕ} (f : SymmetricPower R (ι → R) n) (x : ι → R) (hx : Ideal.span (Set.range x) = ⊤) (hfx : (SymmetricPower.evalSelf R n) ((SymmetricPower.map n (Fintype.linearCombination R x)) f) = 0) : ↑(zeros f)

Equations

• Module.ProjectiveSpace.zerosOfCoordinates f x hx hfx = ⟨Module.ProjectiveSpace.ofCoordinates x hx, ⋯⟩

theorem Module.ProjectiveSpace.ofLinearEquiv_mem_zeros {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {M₁ : Type u_1} [AddCommGroup M₁] [Module R M₁] {n : ℕ} {f : SymmetricPower R M n} (e : M ≃ₗ[R] M₁) (p : AsType R M) (hp : p ∈ zeros f) : (Grassmannian.ofLinearEquiv e) p ∈ zeros ((SymmetricPower.mapLinearEquiv n e) f)

theorem Module.ProjectiveSpace.baseChange_mem_zeros {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (A : Type w₁) [CommRing A] [Algebra R A] {n : ℕ} {f : SymmetricPower R M n} (p : AsType R M) (hp : p ∈ zeros f) : Grassmannian.baseChange A p ∈ zeros ((SymmetricPower.toBaseChange R M A n) f)

theorem Module.ProjectiveSpace.map_mem_zeros {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] {n : ℕ} {f : SymmetricPower R M n} (p : AsType A (TensorProduct R A M)) (hp : p ∈ zeros ((SymmetricPower.toBaseChange R M A n) f)) (φ : A →ₐ[R] B) : Grassmannian.map φ p ∈ zeros ((SymmetricPower.toBaseChange R M B n) f)

noncomputable def Module.ProjectiveSpace.map_zeros {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] {n : ℕ} {f : SymmetricPower R M n} (φ : A →ₐ[R] B) (p : ↑(zeros ((SymmetricPower.toBaseChange R M A n) f))) : ↑(zeros ((SymmetricPower.toBaseChange R M B n) f))

Equations

• Module.ProjectiveSpace.map_zeros φ p = ⟨Module.Grassmannian.map φ ↑p, ⋯⟩

@[simp]

theorem Module.ProjectiveSpace.map_zeros_coe {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] {n : ℕ} {f : SymmetricPower R M n} (φ : A →ₐ[R] B) (p : ↑(zeros ((SymmetricPower.toBaseChange R M A n) f))) : ↑(map_zeros φ p) = Grassmannian.map φ ↑p

noncomputable def Module.ProjectiveSpace.zerosFunctor (R : CommRingCat) (M : ModuleCat ↑R) {n : ℕ} (f : SymmetricPower (↑R) (↑M) n) : CategoryTheory.Functor (CategoryTheory.Under R) (Type (max u v))

zeros as a functor.

Equations

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

@[simp]

theorem Module.ProjectiveSpace.zerosFunctor_obj (R : CommRingCat) (M : ModuleCat ↑R) {n : ℕ} (f : SymmetricPower (↑R) (↑M) n) (A : CategoryTheory.Under R) : (zerosFunctor R M f).obj A = ↑(zeros ((SymmetricPower.toBaseChange (↑R) (↑M) (↑A.right) n) f))

@[simp]

theorem Module.ProjectiveSpace.zerosFunctor_map (R : CommRingCat) (M : ModuleCat ↑R) {n : ℕ} (f : SymmetricPower (↑R) (↑M) n) {X✝ Y✝ : CategoryTheory.Under R} (φ : X✝ ⟶ Y✝) (p : ↑(zeros ((SymmetricPower.toBaseChange (↑R) (↑M) (↑X✝.right) n) f))) : (zerosFunctor R M f).map φ p = map_zeros (CommRingCat.toAlgHom φ) p