Feat/projective with seminorms#41932
Conversation
mpacholski
commented
Jul 19, 2026
mpacholski
commented
…arMap₁₂_add` and `toLinearMap₁₂_smul` Prove that the projection `toLinearMap₁₂` (which strips the topology from a continuous semibilinear map) preserves addition and scalar multiplication, and mark both lemmas with `@[simp]`.
…ap₁₂ and remove the now-duplicate toLinearMap₁₂_apply lemma
… with bundled toLinearMap₁₂
… with bundled toLinearMap₁₂
…ion) go back to rw
…arMap₁₂_apply to toLinearMap₁₂_apply_apply_apply and add @[simps apply] to definition
Port the `lifts` API from `PiTensorProduct` to the binary `TensorProduct` in `Mathlib/LinearAlgebra/TensorProduct/Basic.lean`. This API provides the necessary machinery to represent any tensor element as a formal sum of pure generators in the free monoid, which is a key prerequisite for defining and proving properties of the binary projective seminorm. Specifically, add: - `FreeAddMonoid.toTensorProduct`: proves that the image of a free monoid element is the sum of its pure tensor components. - `lifts`: defines the set of all valid monoid representations of a given tensor. - `nonempty_lifts`: proves that every tensor has at least one representation. - `lifts_zero`, `lifts_add`, `lifts_smul_left` and `lifts_smul_right`: establish the algebraic behavior of lifts under addition, zero, and scalar multiplication.
… Create empty file
…ly_apply_apply" This reverts commit 036006b.
This reverts commit 10a8a28.
This reverts commit a695f72.
…e toLinearMap₁₂_apply to toLinearMap₁₂_apply_apply_apply and add @[simps apply] to definition" This reverts commit dfaf63b.
…m on binary tensor products Introduce the projective seminorm on the tensor product of two normed spaces, mirroring the n-ary construction in `PiTensorProduct.ProjectiveSeminorm`. - Create `Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean`. - Define `TensorProduct.projectiveSeminormAux` on `FreeAddMonoid (X × Y)`. - Define the `Norm` instance on `X ⊗[𝕜] Y` as the infimum of the auxiliary seminorm over all representations (lifts) of a tensor. - Prove basic properties including `projectiveSeminormAux_nonneg`, `projectiveSeminormAux_add_le`, `projectiveSeminormAux_smul`, and `projectiveSeminorm_zero`.
…tiveSeminorm to Mathlib file
…eat/projective-seminorm
…ap₁₂_apply_apply_apply, and assign it a hight priority
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
github-actions
Bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary ce4169d83aImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (weak) |
|---|---|---|
| 5016 | 3 | exposed public sections |
Current commit ce4169d83a
Reference commit f041774a2d
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
1c54034 to
f121461
Compare
…inorm family Introduce `ProjectiveSeminormFamily` on the binary tensor product `X ⊗[𝕜] Y` of two polynormable spaces. For each pair of indices `(i, j) : ιX × ιY`, the corresponding seminorm is constructed by: - Temporarily equipping `X` and `Y` with the `SeminormedAddCommGroup` structures induced by `p i` and `q j`. - Upgrading these locally to `NormedSpace` structures. - Instantiating the binary `projectiveSeminorm` on the tensor product under these local structures. feat(Topology/Algebra/Module): define projective tensor product of topological modules Introduce the topological foundations for the projective tensor product of topological modules, following the geometric formulation in Schaefer's "Topological Vector Spaces". - Define the type synonym `ProjectiveTensorProduct 𝕜 X Y` with scoped notation `X ⊗[𝕜]π Y`. - Define the `TopologicalSpace` instance on `X ⊗[𝕜]π Y` as the supremum (`sSup`) of all topologies making the tensor product a locally convex topological module for which the canonical bilinear map `tmul` is continuous. Specifically: - Prove that the topology generated by `ProjectiveSeminormFamily p q` makes the canonical map `tmul` continuous. - Establish the compatibility class `WithSeminorms (ProjectiveSeminormFamily p q)` on the topological space `M ⊗[R]π N` by showing the equivalence between the supremum topology and the seminorm-induced topology. feat(Analysis/LocallyConvex/TensorProduct): show projective topology is induced by the projective seminorm family Prove that the projective tensor topology on `X ⊗[𝕜]π Y` (defined via the `sSup` of compatible topologies making the canonical bilinear map `tmul` continuous) is strictly induced by the projective seminorm family `ProjectiveSeminormFamily p q`. Specifically: - Prove that the topology generated by `ProjectiveSeminormFamily p q` makes the canonical map `tmul` continuous. - Establish the compatibility class `WithSeminorms (ProjectiveSeminormFamily p q)` on the topological space `M ⊗[R]π N` by showing the equivalence between the supremum topology and the seminorm-induced topology. feat(Analysis/LocallyConvex/TensorProduct): show projective topology is induced by the projective seminorm family Prove that the projective tensor topology on `X ⊗[𝕜]π Y` (defined via the `sSup` of compatible topologies making the canonical bilinear map `tmul` continuous) is strictly induced by the projective seminorm family `ProjectiveSeminormFamily p q`. Specifically: - Prove that the topology generated by `ProjectiveSeminormFamily p q` makes the canonical map `tmul` continuous. - Establish the compatibility class `WithSeminorms (ProjectiveSeminormFamily p q)` on the topological space `M ⊗[R]π N` by showing the equivalence between the supremum topology and the seminorm-induced topology.
f121461 to
ce4169d
Compare
1 participant
