noncomputable def grassmannianChart {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 V with complement V': sends φ : V → V' to its graph in W.

theorem grassmannianChart_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') : grassmannianChart V V' hc 0 = V

The chart maps the zero linear map to the basepoint V of the Grassmannian.

theorem grassmannianChart_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 (grassmannianChart V V' hc)

Chart injectivity: distinct linear maps yield distinct graphs in W.

noncomputable def grassmannianTangentIso {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 isomorphism for the Grassmannian: Hom(V, V') ≃ Hom(V, W / V).

noncomputable def grassmannianCotangentIso {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 isomorphism for the Grassmannian: Hom(V', V) ≃ Hom(W / V, V).

theorem proposition_37_tangent_space {F : Type u_1} [Field F] {W : Type u_2} [AddCommGroup W] [Module F W] (V V' : Submodule F W) (hc : IsCompl V V') : Nonempty ((↥V →ₗ[F] ↥V') ≃ₗ[F] ↥V →ₗ[F] W ⧸ V)

Prop 37 (Lec 20), tangent part: T_V Gr ≃ Hom(V, W / V), expressed via the splitting V'.

theorem proposition_37_cotangent_space {F : Type u_1} [Field F] {W : Type u_2} [AddCommGroup W] [Module F W] (V V' : Submodule F W) (hc : IsCompl V V') : Nonempty ((↥V' →ₗ[F] ↥V) ≃ₗ[F] W ⧸ V →ₗ[F] ↥V)

Prop 37 (Lec 20), cotangent part: Ω_V Gr ≃ Hom(W / V, V).

noncomputable def grassmannianTangentIso_independence {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 the tangent space at V computed via complement V'₁ vs V'₂.

theorem proposition_37_complement_independence {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'₂) : Nonempty ((↥V →ₗ[F] ↥V'₁) ≃ₗ[F] ↥V →ₗ[F] ↥V'₂)

The tangent space identification does not depend on the choice of complement (Prop 37).