chore(topology/algebra/mul_action): rename type variables (#12020)

src/topology/algebra/mul_action.lean

@@ -12,18 +12,18 @@ import topology.algebra.const_mul_action
 /-!
 # Continuous monoid action
 
-In this file we define class `has_continuous_smul`. We say `has_continuous_smul M α` if `M` acts on
-`α` and the map `(c, x) ↦ c • x` is continuous on `M × α`. We reuse this class for topological
+In this file we define class `has_continuous_smul`. We say `has_continuous_smul M X` if `M` acts on
+`X` and the map `(c, x) ↦ c • x` is continuous on `M × X`. We reuse this class for topological
 (semi)modules, vector spaces and algebras.
 
 ## Main definitions
 
-* `has_continuous_smul M α` : typeclass saying that the map `(c, x) ↦ c • x` is continuous
-  on `M × α`;
-* `homeomorph.smul_of_ne_zero`: if a group with zero `G₀` (e.g., a field) acts on `α` and `c : G₀`
-  is a nonzero element of `G₀`, then scalar multiplication by `c` is a homeomorphism of `α`;
-* `homeomorph.smul`: scalar multiplication by an element of a group `G` acting on `α`
-  is a homeomorphism of `α`.
+* `has_continuous_smul M X` : typeclass saying that the map `(c, x) ↦ c • x` is continuous
+  on `M × X`;
+* `homeomorph.smul_of_ne_zero`: if a group with zero `G₀` (e.g., a field) acts on `X` and `c : G₀`
+  is a nonzero element of `G₀`, then scalar multiplication by `c` is a homeomorphism of `X`;
+* `homeomorph.smul`: scalar multiplication by an element of a group `G` acting on `X`
+  is a homeomorphism of `X`.
 * `units.has_continuous_smul`: scalar multiplication by `Mˣ` is continuous when scalar
   multiplication by `M` is continuous. This allows `homeomorph.smul` to be used with on monoids
   with `G = Mˣ`.
@@ -37,49 +37,51 @@ or `filter.tendsto.smul` that provide dot-syntax access to `continuous_smul`.
 open_locale topological_space pointwise
 open filter
 
-/-- Class `has_continuous_smul M α` says that the scalar multiplication `(•) : M → α → α`
+/-- Class `has_continuous_smul M X` says that the scalar multiplication `(•) : M → X → X`
 is continuous in both arguments. We use the same class for all kinds of multiplicative actions,
 including (semi)modules and algebras. -/
-class has_continuous_smul (M α : Type*) [has_scalar M α]
-  [topological_space M] [topological_space α] : Prop :=
-(continuous_smul : continuous (λp : M × α, p.1 • p.2))
+class has_continuous_smul (M X : Type*) [has_scalar M X]
+  [topological_space M] [topological_space X] : Prop :=
+(continuous_smul : continuous (λp : M × X, p.1 • p.2))
 
 export has_continuous_smul (continuous_smul)
 
-/-- Class `has_continuous_vadd M α` says that the additive action `(+ᵥ) : M → α → α`
+/-- Class `has_continuous_vadd M X` says that the additive action `(+ᵥ) : M → X → X`
 is continuous in both arguments. We use the same class for all kinds of additive actions,
 including (semi)modules and algebras. -/
-class has_continuous_vadd (M α : Type*) [has_vadd M α]
-  [topological_space M] [topological_space α] : Prop :=
-(continuous_vadd : continuous (λp : M × α, p.1 +ᵥ p.2))
+class has_continuous_vadd (M X : Type*) [has_vadd M X]
+  [topological_space M] [topological_space X] : Prop :=
+(continuous_vadd : continuous (λp : M × X, p.1 +ᵥ p.2))
 
 export has_continuous_vadd (continuous_vadd)
 
 attribute [to_additive] has_continuous_smul
 
-variables {M α β : Type*}
-variables [topological_space M] [topological_space α]
+section main
+
+variables {M X Y α : Type*} [topological_space M] [topological_space X] [topological_space Y]
 
 section has_scalar
-variables [has_scalar M α] [has_continuous_smul M α]
+
+variables [has_scalar M X] [has_continuous_smul M X]
 
 @[priority 100, to_additive] instance has_continuous_smul.has_continuous_const_smul :
-  has_continuous_const_smul M α :=
+  has_continuous_const_smul M X :=
 { continuous_const_smul := λ _, continuous_smul.comp (continuous_const.prod_mk continuous_id) }
 
 @[to_additive]
-lemma filter.tendsto.smul {f : β → M} {g : β → α} {l : filter β} {c : M} {a : α}
+lemma filter.tendsto.smul {f : α → M} {g : α → X} {l : filter α} {c : M} {a : X}
   (hf : tendsto f l (𝓝 c)) (hg : tendsto g l (𝓝 a)) :
   tendsto (λ x, f x • g x) l (𝓝 $ c • a) :=
 (continuous_smul.tendsto _).comp (hf.prod_mk_nhds hg)
 
 @[to_additive]
-lemma filter.tendsto.smul_const {f : β → M} {l : filter β} {c : M}
-  (hf : tendsto f l (𝓝 c)) (a : α) :
+lemma filter.tendsto.smul_const {f : α → M} {l : filter α} {c : M}
+  (hf : tendsto f l (𝓝 c)) (a : X) :
   tendsto (λ x, (f x) • a) l (𝓝 (c • a)) :=
 hf.smul tendsto_const_nhds
 
-variables [topological_space β] {f : β → M} {g : β → α} {b : β} {s : set β}
+variables {f : Y → M} {g : Y → X} {b : Y} {s : set Y}
 
 @[to_additive]
 lemma continuous_within_at.smul (hf : continuous_within_at f s b)
@@ -103,20 +105,21 @@ lemma continuous.smul (hf : continuous f) (hg : continuous g) :
 continuous_smul.comp (hf.prod_mk hg)
 
 /-- If a scalar is central, then its right action is continuous when its left action is. -/
-instance has_continuous_smul.op [has_scalar Mᵐᵒᵖ α] [is_central_scalar M α] :
-  has_continuous_smul Mᵐᵒᵖ α :=
-⟨ suffices continuous (λ p : M × α, mul_opposite.op p.fst • p.snd),
+instance has_continuous_smul.op [has_scalar Mᵐᵒᵖ X] [is_central_scalar M X] :
+  has_continuous_smul Mᵐᵒᵖ X :=
+⟨ suffices continuous (λ p : M × X, mul_opposite.op p.fst • p.snd),
   from this.comp (mul_opposite.continuous_unop.prod_map continuous_id),
-  by simpa only [op_smul_eq_smul] using (continuous_smul : continuous (λ p : M × α, _)) ⟩
+  by simpa only [op_smul_eq_smul] using (continuous_smul : continuous (λ p : M × X, _)) ⟩
 
 end has_scalar
 
 section monoid
-variables [monoid M] [mul_action M α] [has_continuous_smul M α]
 
-@[to_additive] instance units.has_continuous_smul : has_continuous_smul Mˣ α :=
+variables [monoid M] [mul_action M X] [has_continuous_smul M X]
+
+@[to_additive] instance units.has_continuous_smul : has_continuous_smul Mˣ X :=
 { continuous_smul :=
-    show continuous ((λ p : M × α, p.fst • p.snd) ∘ (λ p : Mˣ × α, (p.1, p.2))),
+    show continuous ((λ p : M × X, p.fst • p.snd) ∘ (λ p : Mˣ × X, (p.1, p.2))),
     from continuous_smul.comp ((units.continuous_coe.comp continuous_fst).prod_mk continuous_snd) }
 
 end monoid
@@ -128,9 +131,9 @@ instance has_continuous_mul.has_continuous_smul {M : Type*} [monoid M]
 ⟨continuous_mul⟩
 
 @[to_additive]
-instance [topological_space β] [has_scalar M α] [has_scalar M β] [has_continuous_smul M α]
-  [has_continuous_smul M β] :
-  has_continuous_smul M (α × β) :=
+instance [has_scalar M X] [has_scalar M Y] [has_continuous_smul M X]
+  [has_continuous_smul M Y] :
+  has_continuous_smul M (X × Y) :=
 ⟨(continuous_fst.smul (continuous_fst.comp continuous_snd)).prod_mk
   (continuous_fst.smul (continuous_snd.comp continuous_snd))⟩
 
@@ -142,41 +145,30 @@ instance {ι : Type*} {γ : ι → Type*}
   (continuous_fst.smul continuous_snd).comp $
     continuous_fst.prod_mk ((continuous_apply i).comp continuous_snd)⟩
 
-section lattice_ops
+end main
 
-variables {ι : Sort*} [has_scalar M β]
-  {ts : set (topological_space β)} (h : Π t ∈ ts, @has_continuous_smul M β _ _ t)
-  {ts' : ι → topological_space β} (h' : Π i, @has_continuous_smul M β _ _ (ts' i))
-  {t₁ t₂ : topological_space β} [h₁ : @has_continuous_smul M β _ _ t₁]
-  [h₂ : @has_continuous_smul M β _ _ t₂]
+section lattice_ops
 
-include h
+variables {ι : Sort*} {M X : Type*} [topological_space M] [has_scalar M X]
 
-@[to_additive] lemma has_continuous_smul_Inf :
-  @has_continuous_smul M β _ _ (Inf ts) :=
+@[to_additive] lemma has_continuous_smul_Inf {ts : set (topological_space X)}
+  (h : Π t ∈ ts, @has_continuous_smul M X _ _ t) :
+  @has_continuous_smul M X _ _ (Inf ts) :=
 { continuous_smul :=
   begin
     rw ← @Inf_singleton _ _ ‹topological_space M›,
     exact continuous_Inf_rng (λ t ht, continuous_Inf_dom₂ (eq.refl _) ht
       (@has_continuous_smul.continuous_smul _ _ _ _ t (h t ht)))
   end }
 
-omit h
-
-include h'
-
-@[to_additive] lemma has_continuous_smul_infi :
-  @has_continuous_smul M β _ _ (⨅ i, ts' i) :=
-by {rw ← Inf_range, exact has_continuous_smul_Inf (set.forall_range_iff.mpr h')}
-
-omit h'
-
-include h₁ h₂
-
-@[to_additive] lemma has_continuous_smul_inf :
-  @has_continuous_smul M β _ _ (t₁ ⊓ t₂) :=
-by {rw inf_eq_infi, refine has_continuous_smul_infi (λ b, _), cases b; assumption}
+@[to_additive] lemma has_continuous_smul_infi {ts' : ι → topological_space X}
+  (h : Π i, @has_continuous_smul M X _ _ (ts' i)) :
+  @has_continuous_smul M X _ _ (⨅ i, ts' i) :=
+has_continuous_smul_Inf $ set.forall_range_iff.mpr h
 
-omit h₁ h₂
+@[to_additive] lemma has_continuous_smul_inf {t₁ t₂ : topological_space X}
+  [@has_continuous_smul M X _ _ t₁] [@has_continuous_smul M X _ _ t₂] :
+  @has_continuous_smul M X _ _ (t₁ ⊓ t₂) :=
+by { rw inf_eq_infi, refine has_continuous_smul_infi (λ b, _), cases b; assumption }
 
 end lattice_ops