WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Cotangent space

Revision #1128 → #2464 · back to history

modifiedCotangent space57e9fc9d1164
FieldFrom #1128To #2464
mathlib.decl—IsLocalRing.CotangentSpace
mathlib.match_kind——
mathlib.module—Mathlib.RingTheory.Ideal.Cotangent
note—Mathlib has the algebraic cotangent space `m/m²` for local rings but no dedicated cotangent space on smooth manifolds (only `TangentSpace`/`TangentBundle`).
status—partial
modifiedCotangent vectorsee94f2bf1860
FieldFrom #1128To #2464
mathlib.decl—IsLocalRing.CotangentSpace
mathlib.match_kind——
mathlib.module—Mathlib.RingTheory.Ideal.Cotangent
note—Elements of `IsLocalRing.CotangentSpace R` are algebraic cotangent vectors; no manifold-level covector type exists.
status—partial
modifiedDimension of cotangent spacescf459a725494
FieldFrom #1128To #2464
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No cotangent space is defined on smooth manifolds in Mathlib, so this constancy-of-dimension statement is not present.
status—not_formalized
modifiedCotangent bundle3de5f53d4a17
FieldFrom #1128To #2464
kindpropositiondefinition
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Changed kind from proposition to definition — the sentence introduces the cotangent bundle as a new differentiable manifold.
provenanceai-agent1ai-moderated
status—not_formalized
modifiedNatural isomorphism from metric/symplectic formfb870856c8b6
FieldFrom #1128To #2464
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No cotangent bundle on manifolds and no musical isomorphism between tangent and cotangent bundles is defined.
status—not_formalized
modifiedCotangent space as dual of tangent space19eddb7864be
FieldFrom #1128To #2464
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has `TangentSpace I x` for manifolds but does not define its dual as a named cotangent-space construction.
status—not_formalized
modifiedCotangent vectors as linear functionalsd5063de4e5f0
FieldFrom #1128To #2464
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No manifold cotangent-vector type in Mathlib to characterise as linear functionals on the tangent space.
status—not_formalized
modifiedAlternative definition via equivalence classese4aac75630e9
FieldFrom #1128To #2464
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib does not have germs of smooth functions modulo the square of the vanishing ideal as a cotangent-space construction.
status—not_formalized
modifiedCotangent space as quotient I/I^283475da6bcfb
FieldFrom #1128To #2464
mathlib.decl—IsLocalRing.CotangentSpace
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.Ideal.Cotangent
note—`IsLocalRing.CotangentSpace R := (maximalIdeal R).Cotangent` is exactly `m/m²` as an `R/m`-vector space (renamed from the older `LocalRing.CotangentSpace`).
status—formalized
addedAnalogy with Zariski tangent space4ea468ae9467
modifiedDifferential of a function3477e37953a9
FieldFrom #1128To #2464
mathlib.decl—mfderiv
mathlib.match_kind—generalization
mathlib.module—Mathlib.Geometry.Manifold.MFDeriv.Defs
note—For `f : M → 𝕜`, `mfderiv I 𝓘(𝕜) f x : TangentSpace I x →L[𝕜] 𝕜` is the differential at `x`, though it is not labelled `df` and cotangent-space typing is absent.
status—partial
modifiedDifferential is a tangent covector12cb8ee453d7
FieldFrom #1128To #2464
mathlib.decl—mfderiv
mathlib.match_kind—generalization
mathlib.module—Mathlib.Geometry.Manifold.MFDeriv.Defs
note—`mfderiv I 𝓘(𝕜) f x` is by construction a continuous linear map on the tangent space, but the tangent-covector interpretation is not spelled out.
status—partial
modifiedDifferential mapca9a0044d4ce
FieldFrom #1128To #2464
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The map `f ↦ df` from smooth functions to sections of the cotangent bundle is not defined in Mathlib (no cotangent bundle).
status—not_formalized
addedLinearity of the differential mapc6514288d730
modifiedEquivalence of the two cotangent space definitionsac67b10167e9
FieldFrom #1128To #2464
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No isomorphism between the dual-of-tangent and the germs-modulo-`I²` definitions of the manifold cotangent space is available.
status—not_formalized
addedPushforward (derivative) between tangent spaces52c04273b14b
modifiedPullback of a smooth map9ce119271228
FieldFrom #1128To #2464
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The pullback of cotangent vectors under a smooth map is not defined in Mathlib; `VectorField.mpullback` is for vector fields, not covectors.
status—not_formalized
modifiedPullback as dual of pushforward0cdb1afe42e4
FieldFrom #1128To #2464
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Without a cotangent-space pullback in Mathlib, its characterization as the transpose of `mfderiv` is not stated.
status—not_formalized
modifiedPullback via equivalence classesa5ea2fbfefe6
FieldFrom #1128To #2464
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No germ-based cotangent-pullback construction is present in Mathlib.
status—not_formalized
addedk-th exterior power of the cotangent space08a8d607db09
modifiedDifferential k-formsd5f7d63da2fd
FieldFrom #1128To #2464
mathlib.decl——
mathlib.match_kind——
mathlib.module—Mathlib.Analysis.Calculus.DifferentialForm.Basic
note—Mathlib represents a differential `k`-form on a normed space as `E → E [⋀^Fin k]→L[𝕜] F` and defines its exterior derivative, but has no bundled type or manifold-level version yet.
status—partial
modifiedOne-forms6c723033e84d
FieldFrom #1128To #2464
mathlib.decl——
mathlib.match_kind——
mathlib.module—Mathlib.Analysis.Calculus.DifferentialForm.Basic
note—One-forms fit in the same normed-space differential-form framework (`E → E [⋀^Fin 1]→L[𝕜] F`) but are not given a dedicated name or manifold definition.
status—partial