English
If φ: A →ₗ[R] B is surjective and B is endowed with the module topology, then φ is a quotient map.
Русский
Если φ: A →ₗ[R] B сюръективно отображает A на B и B имеет модульную топологию, то φ является топологической фактор-мэпой.
LaTeX
$$$IsQuotientMap(φ) \quad\text{for surjective } φ$$$
Lean4
/-- A linear surjection between modules with the module topology is a quotient map.
Equivalently, the pushforward of the module topology along a surjective linear map is
again the module topology. -/
theorem isQuotientMap_of_surjective [τB : TopologicalSpace B] [IsModuleTopology R B] {φ : A →ₗ[R] B}
(hφ : Function.Surjective φ) : IsQuotientMap φ
where
surjective := hφ
eq_coinduced := by
-- We need to prove that the topology on B is coinduced from that on A.
-- First tell the typeclass inference system that A and B are topological groups.
haveI := topologicalAddGroup R A
haveI := topologicalAddGroup R B
have this : Continuous φ := continuous_of_linearMap φ
rw [continuous_iff_coinduced_le] at this
refine le_antisymm ?_ this
rw [eq_moduleTopology R B]
-- Now let's remove B's topology from the typeclass system
clear! τB
letI : TopologicalSpace B := .coinduced φ inferInstance
have hφo : IsOpenQuotientMap φ :=
AddMonoidHom.isOpenQuotientMap_of_isQuotientMap
⟨hφ, rfl⟩
-- We're trying to prove the module topology on B is ≤ the coinduced topology.
-- But recall that the module topology is the Inf of the topologies on B making addition
-- and scalar multiplication continuous, so it suffices to prove
-- that the coinduced topology on B has these properties.
refine sInf_le ⟨?_, ?_⟩
· -- In this branch, we prove that `• : R × B → B` is continuous for the coinduced topology.
apply ContinuousSMul.mk
obtain ⟨hA⟩ : ContinuousSMul R A := inferInstance
have hφ2 : (fun p ↦ p.1 • p.2 : R × B → B) ∘ (Prod.map id φ) = φ ∘ (fun p ↦ p.1 • p.2 : R × A → A) := by ext;
simp
-- Furthermore, the identity from R to R is an open quotient map as is `φ`,
-- so the product `id × φ` is an open quotient map, by a result in the library.
have hoq : IsOpenQuotientMap (_ : R × A → R × B) := IsOpenQuotientMap.prodMap .id hφo
rw [← hoq.continuous_comp_iff]
-- but the diagonal is the composite of the continuous maps `φ` and `• : R × A → A`
rw [hφ2]
-- so we're done
exact Continuous.comp hφo.continuous hA
· /- In this branch we show that addition is continuous for the coinduced topology on `B`.
The argument is basically the same, this time using commutativity of
A × A --(+)--> A
| |
|φ × φ |φ
| |
\/ \/
B × B --(+)--> B
-/
apply ContinuousAdd.mk
obtain ⟨hA⟩ := IsModuleTopology.toContinuousAdd R A
have hφ2 : (fun p ↦ p.1 + p.2 : B × B → B) ∘ (Prod.map φ φ) = φ ∘ (fun p ↦ p.1 + p.2 : A × A → A) := by ext; simp
rw [← (IsOpenQuotientMap.prodMap hφo hφo).continuous_comp_iff, hφ2]
exact Continuous.comp hφo.continuous hA
