noncomputable def Grassmannian.chart {F : Type u_1} [Field F] {W : Type u_2} [AddCommGroup W] [Module F W] (V V' : Submodule F W) (hc : IsCompl V V') (φ : ↥V →ₗ[F] ↥V') : Submodule F W

Grassmannian chart at a point V with chosen complement V': a linear map V → V' is sent to its graph, viewed as a subspace of W via the splitting W ≃ V × V'.

theorem Grassmannian.chart_zero {F : Type u_1} [Field F] {W : Type u_2} [AddCommGroup W] [Module F W] (V V' : Submodule F W) (hc : IsCompl V V') : chart V V' hc 0 = V

The chart sends the zero map to the basepoint V itself.

theorem Grassmannian.chart_injective {F : Type u_1} [Field F] {W : Type u_2} [AddCommGroup W] [Module F W] (V V' : Submodule F W) (hc : IsCompl V V') : Function.Injective (chart V V' hc)

Chart injectivity: distinct linear maps yield distinct graph subspaces.

noncomputable def Grassmannian.tangentSpaceIso {F : Type u_1} [Field F] {W : Type u_2} [AddCommGroup W] [Module F W] (V V' : Submodule F W) (hc : IsCompl V V') : (↥V →ₗ[F] ↥V') ≃ₗ[F] ↥V →ₗ[F] W ⧸ V

Tangent-space identification at V (Prop 37, Lec 20): Hom(V, V') ≃ Hom(V, W / V).

noncomputable def Grassmannian.cotangentSpaceIso {F : Type u_1} [Field F] {W : Type u_2} [AddCommGroup W] [Module F W] (V V' : Submodule F W) (hc : IsCompl V V') : (↥V' →ₗ[F] ↥V) ≃ₗ[F] W ⧸ V →ₗ[F] ↥V

Cotangent-space identification at V: Hom(V', V) ≃ Hom(W / V, V) (dual of tangentSpaceIso).

theorem Grassmannian.tangentSpaceIso_apply {F : Type u_1} [Field F] {W : Type u_2} [AddCommGroup W] [Module F W] (V V' : Submodule F W) (hc : IsCompl V V') (φ : ↥V →ₗ[F] ↥V') (v : ↥V) : ((tangentSpaceIso V V' hc) φ) v = V.mkQ ↑(φ v)

Explicit formula: tangentSpaceIso sends φ to the map v ↦ [φ v] ∈ W / V.

theorem Grassmannian.tangentSpaceIso_independent {F : Type u_1} [Field F] {W : Type u_2} [AddCommGroup W] [Module F W] (V V'₁ V'₂ : Submodule F W) (h₁ : IsCompl V V'₁) (h₂ : IsCompl V V'₂) (φ₁ : ↥V →ₗ[F] ↥V'₁) (φ₂ : ↥V →ₗ[F] ↥V'₂) (hcompat : ∀ (v : ↥V), V.mkQ ↑(φ₁ v) = V.mkQ ↑(φ₂ v)) : (tangentSpaceIso V V'₁ h₁) φ₁ = (tangentSpaceIso V V'₂ h₂) φ₂

The tangent-space identification is independent of the chosen complement: maps φ₁, φ₂ that agree modulo V produce the same element of Hom(V, W / V).

noncomputable def Grassmannian.complementChangeIso {F : Type u_1} [Field F] {W : Type u_2} [AddCommGroup W] [Module F W] (V V'₁ V'₂ : Submodule F W) (h₁ : IsCompl V V'₁) (h₂ : IsCompl V V'₂) : (↥V →ₗ[F] ↥V'₁) ≃ₗ[F] ↥V →ₗ[F] ↥V'₂

Comparison isomorphism between tangent-space models for two different complements V'₁, V'₂.

theorem Grassmannian.complementChangeIso_factors {F : Type u_1} [Field F] {W : Type u_2} [AddCommGroup W] [Module F W] (V V'₁ V'₂ : Submodule F W) (h₁ : IsCompl V V'₁) (h₂ : IsCompl V V'₂) (φ : ↥V →ₗ[F] ↥V'₁) : (tangentSpaceIso V V'₂ h₂) ((complementChangeIso V V'₁ V'₂ h₁ h₂) φ) = (tangentSpaceIso V V'₁ h₁) φ

The change-of-complement isomorphism factors through the common quotient model.

theorem Grassmannian.tangent_finrank_eq (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] [Module.Finite k V] (Sub : Submodule k V) : Module.finrank k (↥Sub →ₗ[k] V ⧸ Sub) = Module.finrank k ↥Sub * Module.finrank k (V ⧸ Sub)

Dimension of Hom(Sub, V/Sub) is (dim Sub) · (dim V/Sub).

theorem Grassmannian.tangent_finrank_formula (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] [Module.Finite k V] (Sub : Submodule k V) : Module.finrank k (↥Sub →ₗ[k] V ⧸ Sub) = Module.finrank k ↥Sub * (Module.finrank k V - Module.finrank k ↥Sub)

Dimension of Hom(Sub, V/Sub) as (dim Sub) · (dim V - dim Sub).

theorem Grassmannian.tangent_finrank_explicit {d n : ℕ} (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] [Module.Finite k V] (Sub : Submodule k V) (hd : Module.finrank k ↥Sub = d) (hn : Module.finrank k V = n) : Module.finrank k (↥Sub →ₗ[k] V ⧸ Sub) = d * (n - d)

Explicit tangent-dimension formula dim T_V Gr(d, n) = d(n - d).

theorem ideal_pow_succ_le {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : I ^ (n + 1) ≤ I ^ n

I^{n+1} ⊆ I^n for any ideal I and natural number n.

@[reducible, inline]

abbrev associatedGradedComponent (R : Type u_1) [CommRing R] (I : Ideal R) (n : ℕ) : Type u_1

The n-th graded piece I^n / I^{n+1} of the associated graded of I.

def associatedGradedComponent.mk {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : ↥(I ^ n) →ₗ[R] associatedGradedComponent R I n

The canonical map I^n → I^n / I^{n+1} projecting onto the n-th graded piece.

theorem associatedGradedComponent.mk_surjective {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : Function.Surjective ⇑(mk I n)

The quotient map onto each graded piece is surjective.