[Merged by Bors] - feat(SeparationQuotient): add missing instances #17239
Conversation
urkud
added
the
t-topology
PR summary 96bcdc4fd2
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Topology.Algebra.SeparationQuotient | 1060 | 1061 | +1 (+0.09%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Topology.Algebra.SeparationQuotient |
1 |
Declarations diff
+ instContinuousSMul
+ instUniformGroup
+ isOpenQuotientMap_mk
+ postcomp_mkCLM_surjective
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
| theorem postcomp_mkCLM_surjective {L : Type*} [Semiring L] (σ : L →+* K) | ||
| (F : Type*) [AddCommMonoid F] [Module L F] [TopologicalSpace F] : |
There was a problem hiding this comment.
The variable order looks a little strange here; I'd expect F to come before σ, but maybe there's a good reason not to do that.
There was a problem hiding this comment.
My reason was: in "σ-semilinear maps from E to F", σ comes before F.
| @@ -391,6 +409,14 @@ theorem mk_outCLM (x : SeparationQuotient E) : mk (outCLM K E x) = x := | |||
| @[simp] | |||
| theorem mk_comp_outCLM : mk ∘ outCLM K E = id := funext (mk_outCLM K) | |||
|
|
|||
| variable {K} in | |||
| theorem postcomp_mkCLM_surjective {L : Type*} [Semiring L] (σ : L →+* K) | |||
There was a problem hiding this comment.
This lemma isn't a misisng instance; can you mention it in the PR description, or bump it to a later PR?
bors d+
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
Also prove `SeparationQuotient.postcomp_mkCLM_surjective`. I'm going to need these instances and lemmas to generalize `CompleteSpace (E →L[K] F)` to topological vector spaces without assuming that `F` is a Hausdorff space, see #17244.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Also prove `SeparationQuotient.postcomp_mkCLM_surjective`. I'm going to need these instances and lemmas to generalize `CompleteSpace (E →L[K] F)` to topological vector spaces without assuming that `F` is a Hausdorff space, see #17244.
Also prove
SeparationQuotient.postcomp_mkCLM_surjective.I'm going to need these instances and lemmas
to generalize
CompleteSpace (E →L[K] F)to topological vector spaceswithout assuming that
Fis a Hausdorff space, see #17244.