feat(Topology/Algebra/Field): ContinuousSMul for intermediate fields

Mathlib.lean

@@ -4621,6 +4621,7 @@ import Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
 import Mathlib.Topology.Algebra.InfiniteSum.Order
 import Mathlib.Topology.Algebra.InfiniteSum.Real
 import Mathlib.Topology.Algebra.InfiniteSum.Ring
+import Mathlib.Topology.Algebra.IntermediateField
 import Mathlib.Topology.Algebra.Localization
 import Mathlib.Topology.Algebra.Module.Alternating.Basic
 import Mathlib.Topology.Algebra.Module.Alternating.Topology

Mathlib/Topology/Algebra/Algebra.lean

@@ -52,6 +52,10 @@ theorem continuousSMul_of_algebraMap [TopologicalSemiring A] (h : Continuous (al
     ContinuousSMul R A :=
   ⟨(continuous_algebraMap_iff_smul R A).1 h⟩
 
+instance Subalgebra.continuousSMul (S : Subalgebra R A) (X) [TopologicalSpace X] [MulAction A X]
+    [ContinuousSMul A X] : ContinuousSMul S X :=
+  Subsemiring.continuousSMul S.toSubsemiring X
+
 section
 variable [ContinuousSMul R A]
 

Mathlib/Topology/Algebra/Field.lean

@@ -149,3 +149,13 @@ theorem IsPreconnected.eq_of_sq_eq [Field 𝕜] [HasContinuousInv₀ 𝕜] [Cont
       (iff_of_eq (iff_false _)).2 (hg_ne _)] at hy' ⊢ <;> assumption
 
 end Preconnected
+
+section ContinuousSMul
+
+variable {F : Type*} [DivisionRing F] [TopologicalSpace F] [TopologicalRing F]
+    (X : Type*) [TopologicalSpace X] [MulAction F X] [ContinuousSMul F X]
+
+instance Subfield.continuousSMul (M : Subfield F) : ContinuousSMul M X :=
+  Subring.continuousSMul M.toSubring X
+
+end ContinuousSMul

Mathlib/Topology/Algebra/IntermediateField.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2024 Jiedong Jiang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jiedong Jiang
+-/
+import Mathlib.FieldTheory.Adjoin
+import Mathlib.Topology.Algebra.Field
+
+/-!
+# Topology on intermediate fields
+
+In this file we define the instances related topology on intermediate fields. The topology is
+already defined in earlier files as the subspace topology.
+-/
+
+variable {K L : Type*} [Field K] [Field L] [Algebra K L]
+    [TopologicalSpace L] [TopologicalRing L]
+
+variable (X : Type*) [TopologicalSpace X] [MulAction L X] [ContinuousSMul L X]
+
+instance IntermediateField.continuousSMul (M : IntermediateField K L) : ContinuousSMul M X :=
+  M.toSubfield.continuousSMul X
+
+instance IntermediateField.botContinuousSMul (M : IntermediateField K L) :
+    ContinuousSMul (⊥ : IntermediateField K L) M :=
+  Inducing.continuousSMul (X := L) (N := (⊥ : IntermediateField K L)) (Y := M)
+    (M := (⊥ : IntermediateField K L)) inducing_subtype_val continuous_id rfl

Mathlib/Topology/Algebra/Ring/Basic.lean

@@ -91,6 +91,10 @@ namespace Subsemiring
 instance topologicalSemiring (S : Subsemiring α) : TopologicalSemiring S :=
   { S.toSubmonoid.continuousMul, S.toAddSubmonoid.continuousAdd with }
 
+instance continuousSMul (s : Subsemiring α) (X) [TopologicalSpace X] [MulAction α X]
+    [ContinuousSMul α X] : ContinuousSMul s X :=
+  Submonoid.continuousSMul
+
 end Subsemiring
 
 /-- The (topological-space) closure of a subsemiring of a topological semiring is
@@ -234,6 +238,10 @@ variable [Ring α] [TopologicalRing α]
 instance Subring.instTopologicalRing (S : Subring α) : TopologicalRing S :=
   { S.toSubmonoid.continuousMul, inferInstanceAs (TopologicalAddGroup S.toAddSubgroup) with }
 
+instance Subring.continuousSMul (s : Subring α) (X) [TopologicalSpace X] [MulAction α X]
+    [ContinuousSMul α X] : ContinuousSMul s X :=
+  Subsemiring.continuousSMul s.toSubsemiring X
+
 /-- The (topological-space) closure of a subring of a topological ring is
 itself a subring. -/
 def Subring.topologicalClosure (S : Subring α) : Subring α :=