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

Diff — Duality (mathematics)

Revision #1173 → #2729 · back to history

modifiedDuality (informal)f127aea95e08
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Informal umbrella description of duality; no single Mathlib declaration captures it.
status—not_formalized
addedFixed point of a duality involution (self-dual object)a4e9c70b874b
addedPairing (bilinear function realizing a duality)0588c11e0314
modifiedDesargues' theorem is self-duala2696776d52d
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Desargues' theorem and its self-duality under projective duality are not formalized in Mathlib.
status—not_formalized
addedDual functor on vector spaces909b1e3d81a5
modifiedComplement of a subsete6dfd9adb9ee
FieldFrom #1173To #2729
mathlib.decl—Set.compl
mathlib.match_kind—exact
mathlib.module—Mathlib.Data.Set.Defs
note—The set-theoretic complement is `Set.compl`, with notation `sᶜ` via `HasCompl`.
status—formalized
modifiedComplement is an involution5a90bbbec388
FieldFrom #1173To #2729
mathlib.decl—compl_compl
mathlib.match_kind—exact
mathlib.module—Mathlib.Order.BooleanAlgebra.Basic
note—`compl_compl` proves `xᶜᶜ = x` in any Boolean algebra, in particular for sets.
status—formalized
modifiedComplement reverses inclusionfd2a280d8089
FieldFrom #1173To #2729
mathlib.decl—Set.compl_subset_compl
mathlib.match_kind—exact
mathlib.module—Mathlib.Order.BooleanAlgebra.Set
note—`Set.compl_subset_compl` states `sᶜ ⊆ tᶜ ↔ t ⊆ s`.
status—formalized
modifiedContrapositive containment via complement1da0099551fc
FieldFrom #1173To #2729
anchor.snippetis contained inGiven two subsets A and B of S
mathlib.decl—Set.compl_subset_compl
mathlib.match_kind—exact
mathlib.module—Mathlib.Order.BooleanAlgebra.Set
note—Anchor tightened: original 'is contained in' matched multiple positions in the sentence.
provenanceai-agent1ai-moderated
status—formalized
modifiedOpen–closed duality in topologyd6615e7deefd
FieldFrom #1173To #2729
mathlib.decl—isClosed_compl_iff
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Basic
note—`isClosed_compl_iff` gives `IsClosed sᶜ ↔ IsOpen s`.
status—formalized
modifiedInterior–closure duality31a185736037
FieldFrom #1173To #2729
mathlib.decl—closure_compl
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Closure
note—`closure_compl` and `interior_compl` capture the interior/closure duality via complement.
status—formalized
addedUnion of opens / intersection of closeds554abf0443f8
modifiedDual cone8a92e53a5a1c
FieldFrom #1173To #2729
mathlib.decl—PointedCone.dual
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Convex.Cone.Dual
note—`PointedCone.dual` defines the dual cone with respect to a bilinear pairing.
status—formalized
modifiedDouble dual cone contains original7b505b2e26b7
FieldFrom #1173To #2729
mathlib.decl—PointedCone.subset_dual_dual
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Convex.Cone.Dual
note—`PointedCone.subset_dual_dual` proves `s ⊆ dual (dual s)`.
status—formalized
modifiedDual cone reverses inclusiond6a0b77a6b98
FieldFrom #1173To #2729
mathlib.decl—PointedCone.dual_antitone
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Convex.Cone.Dual
note—`PointedCone.dual_antitone` states the dual operation is antitone under inclusion.
status—formalized
modifiedDual vector space138d1b7763c0
FieldFrom #1173To #2729
mathlib.decl—Module.Dual
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Dual.Defs
note—`Module.Dual R M` is the space of linear functionals `M →ₗ[R] R`.
status—formalized
modifiedFinite-dimensional double dual isomorphism1e338c2c450c
FieldFrom #1173To #2729
mathlib.decl—Module.evalEquiv
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Dual.Defs
note—`Module.evalEquiv` gives `V ≃ₗ[R] Dual R (Dual R V)` under `Module.IsReflexive`, which holds for finite-dimensional spaces.
status—formalized
modifiedHom adjunction for dual spacesf8c3823a93af
FieldFrom #1173To #2729
mathlib.decl—LinearMap.BilinMap
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.BilinearMap
note—`Hom(V,W*) ≃ Hom(V ⊗ W, K)` type currying exists for bilinear maps via `LinearMap.BilinMap` / `TensorProduct.lift`, but no single decl matches this exact statement.
status—partial
modifiedRiesz representation in Hilbert spaces22ce3e3bf5cd
FieldFrom #1173To #2729
mathlib.decl—InnerProductSpace.toDual
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.InnerProductSpace.Dual
note—`InnerProductSpace.toDual` is the Riesz isometric isomorphism `E ≃ₗᵢ⋆[𝕜] StrongDual 𝕜 E` for Hilbert spaces.
status—formalized
modifiedGalois group of intermediate fielda258ebb90a9d
FieldFrom #1173To #2729
mathlib.decl—IntermediateField.fixingSubgroup
mathlib.match_kind—exact
mathlib.module—Mathlib.FieldTheory.Galois.Basic
note—`IntermediateField.fixingSubgroup` is the subgroup of automorphisms fixing an intermediate field.
status—formalized
modifiedFixed field of subgroupae69379a70a6
FieldFrom #1173To #2729
mathlib.decl—FixedPoints.intermediateField
mathlib.match_kind—exact
mathlib.module—Mathlib.FieldTheory.Galois.Basic
note—`FixedPoints.intermediateField` gives the intermediate field fixed by a subgroup.
status—formalized
modifiedFundamental theorem of Galois theorya6915ce35307
FieldFrom #1173To #2729
mathlib.decl—IsGalois.intermediateFieldEquivSubgroup
mathlib.match_kind—exact
mathlib.module—Mathlib.FieldTheory.Galois.Basic
note—`IsGalois.intermediateFieldEquivSubgroup` states the order-reversing bijection between intermediate fields and subgroups.
status—formalized
modifiedDual posetc353a7308bd7
FieldFrom #1173To #2729
mathlib.decl—OrderDual
mathlib.match_kind—exact
mathlib.module—Mathlib.Order.OrderDual
note—`OrderDual α` is the type synonym with reversed order, i.e. the dual poset.
status—formalized
modifiedSubset/superset dual order820af226fa8b
FieldFrom #1173To #2729
mathlib.decl—OrderDual
mathlib.match_kind—invocation
mathlib.module—Mathlib.Order.OrderDual
note—The general phenomenon is captured by `OrderDual` on the powerset, though no dedicated lemma names this example.
status—partial
modifiedDivides/multiple-of dual order9d60285426f1
FieldFrom #1173To #2729
mathlib.decl—OrderDual
mathlib.match_kind—invocation
mathlib.module—Mathlib.Order.OrderDual
note—The divides order (`Dvd.dvd`) exists but its explicit identification as the dual is not named.
status—partial
modifiedDescendant/ancestor dual orderab55d4f80005
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Informal biological example not present in Mathlib.
status—not_formalized
modifiedDuality transform23d9a3e26120
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The concept of an involutive order antiautomorphism is not packaged in Mathlib as a named structure.
status—not_formalized
modifiedComposition of duality transformsc8d6360358c2
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Mathlib decl formalizes composition of order antiautomorphisms as an automorphism at this named level.
status—not_formalized
modifiedDual concepts in posetsc21fa35044b1
FieldFrom #1173To #2729
mathlib.decl—OrderDual
mathlib.match_kind—generalization
mathlib.module—Mathlib.Order.OrderDual
note—Minimal/maximal, sup/inf, etc. are systematically dualized through `OrderDual` type synonyms in Mathlib.
status—partial
modifiedDual matroid7a2d62efad1f
FieldFrom #1173To #2729
mathlib.decl—Matroid.dual
mathlib.match_kind—exact
mathlib.module—Mathlib.Combinatorics.Matroid.Dual
note—`Matroid.dual` (postfix `✶`) defines the dual matroid.
status—formalized
modifiedDuality of Platonic solids5b8a46c3fd5f
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Platonic solids and their duality are not formalized in Mathlib.
status—not_formalized
modifiedDual polyhedron via face centers7ce498dde660
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no theory of polyhedra with faces or dualization via face centers.
status—not_formalized
modifiedPolar reciprocation / dual polytope126d21529364
FieldFrom #1173To #2729
mathlib.decl—polar
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.LocallyConvex.Polar
note—The polar set of a subset (`polar`) is defined in Mathlib but not specialised to polytopes.
status—partial
modifiedPolytope duality is an involutionf2742356c8e7
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Polytope duality and its involution property are not formalized in Mathlib.
status—not_formalized
modifiedDual graph of a polyhedronc74183e332ac
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Neither polyhedra nor their dual graphs are formalized in Mathlib.
status—not_formalized
modifiedPlanar graph duality (embeddings)314575539527
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no theory of planar graph embeddings or their duality.
status—not_formalized
modifiedDelaunay–Voronoi duality8b4b7c16a197
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Delaunay triangulations and Voronoi diagrams are not formalized in Mathlib.
status—not_formalized
modifiedMatroid duality extends planar graph duality67920e5b634c
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—While `Matroid.dual` exists, the identification with planar graph duality is not in Mathlib.
status—not_formalized
modifiedLinear program and dual problem52f38b11b2f3
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Linear programming and LP duality are not formalized in Mathlib.
status—not_formalized
modifiedLogical dualityd31466d30390
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The informal notion of `logical duality' has no dedicated Mathlib decl.
status—not_formalized
modifiedDuality of quantifiers4955fa5d9ae4
FieldFrom #1173To #2729
mathlib.decl—not_exists
mathlib.match_kind—exact
mathlib.module—Init.PropLemmas
note—`not_exists` gives `¬(∃ x, p x) ↔ ∀ x, ¬p x`, and `Classical.not_forall` gives the dual, expressing quantifier duality.
status—formalized
modifiedSatisfiability–validity duality7fa5213c43f3
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Satisfiability/validity as first-order logical notions are not treated in Mathlib.
status—not_formalized
modifiedDuality of conjunction and disjunction393c49d2ed08
FieldFrom #1173To #2729
anchor.snippettheoperators are dual in this sense
mathlib.decl—compl_sup
mathlib.match_kind—exact
mathlib.module—Mathlib.Order.Heyting.Basic
note—Anchor tightened from bare 'the' to the unique phrase pointing at ∧/∨ duality.
provenanceai-agent1ai-moderated
status—formalized
modifiedDe Morgan's laws5d06f93c846d
FieldFrom #1173To #2729
mathlib.decl—compl_inf
mathlib.match_kind—exact
mathlib.module—Mathlib.Order.BooleanAlgebra.Basic
note—`compl_inf` (and `compl_sup`, `Set.compl_union`, `Set.compl_inter`) formalize De Morgan's laws in Boolean algebras.
status—formalized
modifiedModal duality of necessity and possibilityfd5b2b9581fb
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Modal logic and its box/diamond duality are not in Mathlib.
status—not_formalized
modifiedUnion–intersection duality via complement891da940c465
FieldFrom #1173To #2729
mathlib.decl—Set.compl_union
mathlib.match_kind—exact
mathlib.module—Mathlib.Order.BooleanAlgebra.Set
note—`Set.compl_union` (and `Set.compl_inter`, `Set.compl_iUnion`) express set De Morgan / union–intersection duality.
status—formalized
modifiedBidual66de5daeebdf
FieldFrom #1173To #2729
mathlib.decl—Module.Dual
mathlib.match_kind—invocation
mathlib.module—Mathlib.LinearAlgebra.Dual.Defs
note—The bidual is `Module.Dual R (Module.Dual R M)`, a double application of `Module.Dual`.
status—formalized
modifiedDual poset of dual poset is original3583863d81df
FieldFrom #1173To #2729
mathlib.decl—OrderDual
mathlib.match_kind—invocation
mathlib.module—Mathlib.Order.OrderDual
note—`OrderDual (OrderDual α)` is definitionally α; the fact is implicit rather than a named lemma.
status—partial
modifiedDouble dual conec939287f4698
FieldFrom #1173To #2729
mathlib.decl—PointedCone.subset_dual_dual
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Convex.Cone.Dual
note—`PointedCone.subset_dual_dual` proves the primal is contained in the double dual cone.
status—formalized
modifiedCanonical evaluation mape0e4d23911f3
FieldFrom #1173To #2729
mathlib.decl—Module.Dual.eval
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Dual.Defs
note—`Module.Dual.eval` is the canonical `M →ₗ[R] Dual R (Dual R M)`.
status—formalized
modifiedAlgebraic double dual is injective84569cb4d387
FieldFrom #1173To #2729
mathlib.decl—Module.eval_ker
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Dual.Lemmas
note—`Module.eval_ker` shows the evaluation map has trivial kernel over a field, so it is injective (`Basis.eval_injective` for the basis version).
status—formalized
modifiedTorsionless and reflexive modulesc99aa5ba0ce4
FieldFrom #1173To #2729
mathlib.decl—Module.IsReflexive
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Dual.Defs
note—`Module.IsReflexive` is the property that `Module.Dual.eval` is bijective; torsionless is not separately named.
status—formalized
modifiedTopological dual and reflexive space82427e3d0742
FieldFrom #1173To #2729
mathlib.decl—StrongDual
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.Normed.Module.Dual
note—The topological dual is `StrongDual`; a general 'reflexive normed space' class exists in Mathlib but is not named as such at this abstraction.
status—partial
modifiedPontryagin duality (bidual)9dd1609e3375
FieldFrom #1173To #2729
mathlib.decl—PontryaginDual
mathlib.match_kind—generalization
mathlib.module—Mathlib.Topology.Algebra.PontryaginDual
note—`PontryaginDual` is defined for locally compact abelian groups, and `doubleDualEquiv` for finite abelian groups exists, but the full LCA bidual isomorphism is not yet in Mathlib.
status—partial
modifiedInternal Hom dual object5423f90d6d5b
FieldFrom #1173To #2729
mathlib.decl—CategoryTheory.MonoidalClosed
mathlib.match_kind—generalization
mathlib.module—Mathlib.CategoryTheory.Monoidal.Closed.Basic
note—`MonoidalClosed` gives the internal Hom in a monoidal category; the categorical notion of dualizable object exists in Mathlib in the rigid monoidal framework.
status—partial
modifiedCanonical map to bidual (category-theoretic)f768f6b0a2a1
FieldFrom #1173To #2729
mathlib.decl—Module.Dual.eval
mathlib.match_kind—special_case
mathlib.module—Mathlib.LinearAlgebra.Dual.Defs
note—The vector-space version `Module.Dual.eval` is formalized; a purely category-theoretic 'map to bidual' is not stated at that abstraction.
status—partial
modifiedDual vector space as duality example37081f7de789
FieldFrom #1173To #2729
mathlib.decl—Module.Dual
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Dual.Defs
note—The dual-space contravariant assignment is `Module.Dual` with `Module.Dual.transpose` for maps.
status—formalized
modifiedCharacterization of finite-dimensional vector spaces449373c0224e
FieldFrom #1173To #2729
mathlib.decl—Basis.linearEquiv_dual_iff_finiteDimensional
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Dual.Lemmas
note—`Basis.linearEquiv_dual_iff_finiteDimensional` characterizes finite-dimensionality via V ≃ₗ V*.
status—formalized
modifiedIsomorphism V ≅ V* iff finite-dimensional0d47cda3cf96
FieldFrom #1173To #2729
mathlib.decl—Basis.linearEquiv_dual_iff_finiteDimensional
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Dual.Lemmas
note—Same lemma establishes V ≃ₗ Dual K V ↔ FiniteDimensional K V.
status—formalized
modifiedInner product space8c3c843a5813
FieldFrom #1173To #2729
mathlib.decl—InnerProductSpace
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.InnerProductSpace.Defs
note—`InnerProductSpace` is the standard Mathlib class.
status—formalized
modifiedRiemannian metricb7997d068819
FieldFrom #1173To #2729
mathlib.decl—IsContMDiffRiemannianBundle
mathlib.match_kind—generalization
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.Riemannian
note—Smooth Riemannian metrics on vector bundles / manifolds are formalized via `IsContMDiffRiemannianBundle` and `PseudoEMetricSpace.ofRiemannianMetric`.
status—partial
modifiedHodge star operatorf6edb20a307c
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Hodge star operator is not formalized in Mathlib.
status—not_formalized
modifiedPrinciple of duality in projective planese038c499ab0d
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no formal treatment of the projective plane duality principle.
status—not_formalized
modifiedTwo points determine a line (dual)00701969d125
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Axioms of projective planes and their dual pair are not formalized.
status—not_formalized
modifiedProjective points/lines via subspacesf51784d5cd92
FieldFrom #1173To #2729
mathlib.decl—Projectivization
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.Projectivization.Basic
note—Mathlib has `Projectivization` giving 1-dimensional subspaces as points, but no development identifying lines with 2-dim subspaces at the duality level.
status—partial
modifiedBilinear form identifies projective plane with dual117128ee9e3b
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The identification of a projective plane with the dual projective plane via a bilinear form is not formalized.
status—not_formalized
modifiedReflexive (topological) spacecde64d9c3ef9
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib does not yet have a general 'reflexive normed/TVS' class capturing V ≃ V**.
status—not_formalized
modifiedRiesz representation for Hilbert spacesbb08b742d86a
FieldFrom #1173To #2729
mathlib.decl—InnerProductSpace.toDual
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.InnerProductSpace.Dual
note—`InnerProductSpace.toDual` is the Riesz surjective isometry from a Hilbert space to its dual.
status—formalized
modifiedHilbert spaces are reflexive Banach spacesfd8c88560ce5
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Banach 'reflexive space' concept and the resulting statement are not formalized in Mathlib.
status—not_formalized
modifiedDual of Lp is Lq542b8b430bdd
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The duality (Lp)* ≃ Lq for 1 ≤ p < ∞ is not stated as a named theorem in Mathlib.
status—not_formalized
modifiedL1 is not reflexive2687056e403f
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib, as 'reflexive Banach space' itself is not.
status—not_formalized
modifiedDistributions as linear functionals19bdf3c28642
FieldFrom #1173To #2729
mathlib.decl—SchwartzMap
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.Distribution.SchwartzSpace.Basic
note—The Schwartz space is formalized (`SchwartzMap`); tempered distributions are treated as its continuous dual, but no explicit `Distribution` type is defined.
status—partial
modifiedStandard distribution spaces are reflexive0a856b72de5d
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Reflexivity of standard distribution spaces is not formalized.
status—not_formalized
modifiedDual latticee88c7cb7e596
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Z-dual lattice construction is not present as a named Mathlib decl.
status—not_formalized
modifiedPontryagin dual of locally compact groupd4393cb8e2ea
FieldFrom #1173To #2729
mathlib.decl—PontryaginDual
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Algebra.PontryaginDual
note—`PontryaginDual A` is defined as continuous homomorphisms `A →* Circle`.
status—formalized
modifiedContravariant functor duality510316f102fd
FieldFrom #1173To #2729
mathlib.decl—CategoryTheory.Category.opposite
mathlib.match_kind—exact
mathlib.module—Mathlib.CategoryTheory.Opposites
note—Contravariant functors are functors out of the opposite category (`Opposite`, `Category.opposite`).
status—formalized
modifiedSelf-dual category5cfe24c08d2d
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No dedicated `SelfDualCategory` predicate/class exists in Mathlib.
status—not_formalized
modifiedCategory of Hilbert spaces is self-dual18549dc5e0bd
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Self-duality of the category of Hilbert spaces is not formalized in Mathlib.
status—not_formalized
modifiedProducts and coproducts as dual989581ea61fd
FieldFrom #1173To #2729
mathlib.decl—CategoryTheory.Limits.HasProducts
mathlib.match_kind—exact
mathlib.module—Mathlib.CategoryTheory.Limits.Shapes.Products
note—`HasProducts`/`HasCoproducts` are dual under `Opposite`; their opposite-category correspondence is set up in `Limits/Shapes/Opposites/Products.lean`.
status—formalized
modifiedLimits dual to colimitseb22b8ff4488
FieldFrom #1173To #2729
mathlib.decl—CategoryTheory.Limits.limit
mathlib.match_kind—exact
mathlib.module—Mathlib.CategoryTheory.Limits.HasLimits
note—`Limits.limit` and `Limits.colimit` are dualized via the opposite-category API.
status—formalized
modifiedAdjoint functorse1c901081235
FieldFrom #1173To #2729
mathlib.decl—CategoryTheory.Adjunction
mathlib.match_kind—exact
mathlib.module—Mathlib.CategoryTheory.Adjunction.Basic
note—`CategoryTheory.Adjunction F G` is the standard adjunction structure.
status—formalized
modifiedColimit/diagonal adjunctiona601e2e40cbe
FieldFrom #1173To #2729
mathlib.decl—CategoryTheory.Limits.colimConstAdj
mathlib.match_kind—exact
mathlib.module—Mathlib.CategoryTheory.Limits.HasLimits
note—`colimConstAdj` gives the adjunction between the colimit functor and the constant (diagonal) diagram functor.
status—formalized
modifiedGelfand duality46e0ecee1991
FieldFrom #1173To #2729
mathlib.decl—gelfandStarTransform
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.CStarAlgebra.GelfandDuality
note—`gelfandStarTransform` realizes the Gelfand duality star-isomorphism.
status—formalized
modifiedAffine schemes ↔ commutative rings3948b9cd228c
FieldFrom #1173To #2729
mathlib.decl—AlgebraicGeometry.AffineScheme.equivCommRingCat
mathlib.match_kind—exact
mathlib.module—Mathlib.AlgebraicGeometry.AffineScheme
note—`AffineScheme.equivCommRingCat` is the equivalence between affine schemes and (opposite of) commutative rings.
status—formalized
modifiedTannaka–Krein duality792f32cd2f0d
FieldFrom #1173To #2729
mathlib.decl—ModuleCat.tannakaDuality
mathlib.match_kind—generalization
mathlib.module—Mathlib.Algebra.Category.ModuleCat.Tannaka
note—Mathlib has a Tannaka-style reconstruction for module categories (`ModuleCat.Tannaka`); full Tannaka–Krein duality for compact groups is not present.
status—partial
modifiedGalois connection0acc28e3b5fe
FieldFrom #1173To #2729
mathlib.decl—GaloisConnection
mathlib.match_kind—exact
mathlib.module—Mathlib.Order.GaloisConnection.Defs
note—`GaloisConnection l u` is defined as the standard adjunction on preorders.
status—formalized
modifiedOpen sets form complete Heyting algebra4045140dfa97
FieldFrom #1173To #2729
mathlib.decl—TopologicalSpace.Opens.instFrame
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Sets.Opens
note—`Opens.instFrame` gives the frame (complete Heyting algebra) structure on the lattice of open sets.
status—formalized
modifiedStone duality7a44fd571ec0
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Full Stone duality between sober spaces and spatial frames/locales is not formalized in Mathlib.
status—not_formalized
modifiedBirkhoff's representation theorem661746560d5b
FieldFrom #1173To #2729
mathlib.decl—OrderIso.lowerSetSupIrred
mathlib.match_kind—generalization
mathlib.module—Mathlib.Order.Birkhoff
note—`Mathlib.Order.Birkhoff` develops Birkhoff's representation for finite distributive lattices.
status—partial
modifiedCharacter group9c8db6a518d9
FieldFrom #1173To #2729
mathlib.decl—PontryaginDual
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Algebra.PontryaginDual
note—`PontryaginDual A` is the group of continuous characters `A →* Circle`.
status—formalized
modifiedPontryagin duality theorem27df9079cfeb
FieldFrom #1173To #2729
mathlib.decl—PontryaginDual
mathlib.match_kind—generalization
mathlib.module—Mathlib.Topology.Algebra.PontryaginDual
note—The `PontryaginDual` inherits `LocallyCompactSpace`, but the full duality (double-dual isomorphism) is only formalized in the finite abelian case (`doubleDualEquiv`).
status—partial
modifiedDiscrete ↔ compact under Pontryagin014f75832cd7
FieldFrom #1173To #2729
mathlib.decl—PontryaginDual.instDiscreteTopology
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Algebra.PontryaginDual
note—Mathlib has instances making `PontryaginDual` discrete when the source is compact (and vice versa).
status—formalized
modifiedFourier transform593ca2502238
FieldFrom #1173To #2729
mathlib.decl—VectorFourier.fourierIntegral
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Fourier.FourierTransform
note—`VectorFourier.fourierIntegral` defines the Fourier transform between a vector space and its dual using an additive character.
status—formalized
modifiedFourier transform on L202feaaee6454
FieldFrom #1173To #2729
mathlib.decl—VectorFourier.fourierIntegral
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.Fourier.FourierTransform
note—Fourier transform is defined and Fourier inversion is proved, but Plancherel/L² isometry on ℝⁿ is only partial in Mathlib.
status—partial
modifiedFourier exchanges multiplication and convolution12ba62efe718
FieldFrom #1173To #2729
mathlib.decl—Real.fourier_bilin_convolution_eq
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Fourier.Convolution
note—`Real.fourier_bilin_convolution_eq` shows the Fourier transform sends convolution to (pointwise) product.
status—formalized
modifiedLaplace transform duality966498445ae9
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Laplace transform is not formalized in Mathlib.
status—not_formalized
modifiedLegendre transformationbb362aa69032
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Legendre / Legendre–Fenchel transform is not formalized in Mathlib.
status—not_formalized
modifiedPerfect pairing gives dual isomorphism3b5f32aa423f
FieldFrom #1173To #2729
mathlib.decl—LinearMap.IsPerfPair
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.PerfectPairing.Basic
note—`LinearMap.IsPerfPair` (and `Module.IsReflexive.of_isPerfPair`) express that a perfect pairing induces an isomorphism to the dual.
status—formalized
modifiedPoincaré duality (complex manifolds)e843d7a3ef9c
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Poincaré duality is not formalized in Mathlib.
status—not_formalized
modifiedPoincaré duality via de Rham2782d313e429
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The de Rham version of Poincaré duality is not formalized.
status—not_formalized
modifiedPoincaré duality reverses dimensionsa662e3d5bb86
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Dimension-reversal statement of Poincaré duality is not in Mathlib.
status—not_formalized
modifiedl-adic Poincaré-style duality3e4f50212fd4
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—ℓ-adic Poincaré duality is not formalized in Mathlib.
status—not_formalized
modifiedVerdier dualityb0d45b080f13
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Verdier duality is not formalized in Mathlib.
status—not_formalized
modifiedSerre / coherent duality2d3c14ac6c9a
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Serre / coherent duality is not formalized in Mathlib.
status—not_formalized
modifiedGalois cohomology pairing over finite fields62044eb34cc0
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Étale-cohomology Galois pairings over finite fields are not formalized in Mathlib.
status—not_formalized
modifiedLocal and Poitou–Tate duality3cef7a797322
FieldFrom #1173To #2729
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Local Tate duality and Poitou–Tate duality are not formalized in Mathlib.
status—not_formalized