Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(SeparationQuotient): add missing instances #17239

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat(SeparationQuotient): add missing instances #17239

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 27 additions & 1 deletion Mathlib/Topology/Algebra/SeparationQuotient.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,9 @@ Copyright (c) 2024 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
import Mathlib.Topology.Algebra.Module.Basic
import Mathlib.LinearAlgebra.Basis.VectorSpace
import Mathlib.Topology.Algebra.Module.Basic
import Mathlib.Topology.Maps.OpenQuotient

/-!
# Algebraic operations on `SeparationQuotient`
Expand Down Expand Up @@ -63,6 +64,12 @@ instance instIsScalarTower [SMul M N] [ContinuousConstSMul N X] [IsScalarTower M

end SMul

instance instContinuousSMul {M X : Type*} [SMul M X] [TopologicalSpace M] [TopologicalSpace X]
[ContinuousSMul M X] : ContinuousSMul M (SeparationQuotient X) where
continuous_smul := by
rw [(IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).quotientMap.continuous_iff]
exact continuous_mk.comp continuous_smul

instance instSMulZeroClass {M X : Type*} [Zero X] [SMulZeroClass M X] [TopologicalSpace X]
[ContinuousConstSMul M X] : SMulZeroClass M (SeparationQuotient X) :=
ZeroHom.smulZeroClass ⟨mk, mk_zero⟩ mk_smul
Expand Down Expand Up @@ -190,6 +197,17 @@ instance instCommGroup [CommGroup G] [TopologicalGroup G] : CommGroup (Separatio

end Group

section UniformGroup

@[to_additive]
instance instUniformGroup {G : Type*} [Group G] [UniformSpace G] [UniformGroup G] :
UniformGroup (SeparationQuotient G) where
uniformContinuous_div := by
rw [uniformContinuous_dom₂]
exact uniformContinuous_mk.comp uniformContinuous_div

end UniformGroup

section MonoidWithZero

variable {M₀ : Type*} [TopologicalSpace M₀]
Expand Down Expand Up @@ -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)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This lemma isn't a misisng instance; can you mention it in the PR description, or bump it to a later PR?

bors d+

(F : Type*) [AddCommMonoid F] [Module L F] [TopologicalSpace F] :
Comment on lines +413 to +414
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My reason was: in "σ-semilinear maps from E to F", σ comes before F.

Function.Surjective ((mkCLM K E).comp : (F →SL[σ] E) → (F →SL[σ] SeparationQuotient E)) := by
intro f
use (outCLM K E).comp f
rw [← ContinuousLinearMap.comp_assoc, mkCLM_comp_outCLM, ContinuousLinearMap.id_comp]

/-- The `SeparationQuotient.outCLM K E` map is a topological embedding. -/
theorem outCLM_embedding : Embedding (outCLM K E) :=
Function.LeftInverse.embedding (mk_outCLM K) continuous_mk (map_continuous _)
Expand Down
3 changes: 3 additions & 0 deletions Mathlib/Topology/Inseparable.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -548,6 +548,9 @@ theorem preimage_image_mk_open (hs : IsOpen s) : mk ⁻¹' (mk '' s) = s := by
theorem isOpenMap_mk : IsOpenMap (mk : X → SeparationQuotient X) := fun s hs =>
quotientMap_mk.isOpen_preimage.1 <| by rwa [preimage_image_mk_open hs]

theorem isOpenQuotientMap_mk : IsOpenQuotientMap (mk : X → SeparationQuotient X) :=
⟨surjective_mk, continuous_mk, isOpenMap_mk⟩

theorem preimage_image_mk_closed (hs : IsClosed s) : mk ⁻¹' (mk '' s) = s := by
refine Subset.antisymm ?_ (subset_preimage_image _ _)
rintro x ⟨y, hys, hxy⟩
Expand Down
Loading