remove freeness hypothesis :-)

Author: kbuzzard

FLT/ForMathlib/ActionTopology.lean

@@ -250,6 +250,67 @@ lemma continuous_neg (C : Type*) [AddCommGroup C] [Module R C] [TopologicalSpace
 
 end function
 
+section surjection
+
+variable {R : Type*} [τR : TopologicalSpace R] [Ring R] [TopologicalRing R]
+variable {A : Type*} [AddCommGroup A] [Module R A] [aA : TopologicalSpace A] [IsActionTopology R A]
+variable {B : Type*} [AddCommGroup B] [Module R B] [aB : TopologicalSpace B] [IsActionTopology R B]
+
+-- Here I need the lemma about how quotients are open so I do need groups
+-- because this relies on translates of an open being open
+lemma coinduced_of_surjective {φ : A →ₗ[R] B} (hφ : Function.Surjective φ) :
+    TopologicalSpace.coinduced φ (actionTopology R A) = actionTopology R B := by
+  have : Continuous φ := continuous_of_linearMap φ
+  rw [continuous_iff_coinduced_le, isActionTopology R A, isActionTopology R B] at this
+  apply le_antisymm this
+  have : ContinuousAdd A := isActionTopology_continuousAdd R A
+  refine sInf_le ⟨?_, ?_⟩
+  · apply @ContinuousSMul.mk R B _ _ (_)
+    obtain ⟨foo⟩ : ContinuousSMul R A := inferInstance
+    rw [continuous_def] at foo ⊢
+    intro U hU
+    rw [isOpen_coinduced, ← isActionTopology R A] at hU
+    specialize foo _ hU; clear hU
+    rw [← Set.preimage_comp, show φ ∘ (fun p ↦ p.1 • p.2 : R × A → A) =
+      (fun p ↦ p.1 • p.2 : R × B → B) ∘
+      (Prod.map id ⇑φ.toAddMonoidHom) by ext; simp, Set.preimage_comp] at foo
+    clear! aB -- easiest to just remove topology on B completely now so typeclass inference
+    -- never sees it
+    convert isOpenMap_of_coinduced (AddMonoidHom.prodMap (AddMonoidHom.id R) φ.toAddMonoidHom)
+      (_) (_) (_) foo
+    · -- aesop would do this if `Function.surjective_id : Surjective ⇑(AddMonoidHom.id R)`
+      -- was known by it
+      apply (Set.image_preimage_eq _ _).symm
+      rw [AddMonoidHom.coe_prodMap, Prod.map_surjective]
+      exact ⟨Function.surjective_id, by simp_all⟩
+    · -- should `apply continuousprodmap ctrl-space` find `Continuous.prod_map`?
+      apply @Continuous.prod_map _ _ _ _ (_) (_) (_) (_) id φ continuous_id
+      rw [continuous_iff_coinduced_le, isActionTopology R A]
+    · rw [← isActionTopology R A]
+      exact coinduced_prod_eq_prod_coinduced (AddMonoidHom.id R) φ.toAddMonoidHom
+       (Function.surjective_id) hφ
+  · apply @ContinuousAdd.mk _ (_)
+    obtain ⟨bar⟩ := isActionTopology_continuousAdd R A
+    rw [continuous_def] at bar ⊢
+    intro U hU
+    rw [isOpen_coinduced, ← isActionTopology R A] at hU
+    specialize bar _ hU; clear hU
+    rw [← Set.preimage_comp, show φ ∘ (fun p ↦ p.1 + p.2 : A × A → A) =
+      (fun p ↦ p.1 + p.2 : B × B → B) ∘
+      (Prod.map ⇑φ.toAddMonoidHom ⇑φ.toAddMonoidHom) by ext; simp, Set.preimage_comp] at bar
+    clear! aB -- easiest to just remove topology on B completely now
+    convert isOpenMap_of_coinduced (AddMonoidHom.prodMap φ.toAddMonoidHom φ.toAddMonoidHom)
+      (_) (_) (_) bar
+    · aesop
+    · apply @Continuous.prod_map _ _ _ _ (_) (_) (_) (_) <;>
+      · rw [continuous_iff_coinduced_le, isActionTopology R A]; rfl
+    · rw [← isActionTopology R A]
+      exact coinduced_prod_eq_prod_coinduced φ φ hφ hφ
+
+
+end surjection
+
+
 section prod
 
 variable {R : Type*} [τR : TopologicalSpace R] [Semiring R] [TopologicalSemiring R]
@@ -287,16 +348,6 @@ section Pi
 
 variable {R : Type*} [τR : TopologicalSpace R] [Semiring R] [TopologicalSemiring R]
 
--- not sure I'm going to do it this way -- see `pi` below.
--- instance piNat (n : ℕ) {A : Fin n → Type*} [∀ i, AddCommGroup (A i)]
---     [∀ i, Module R (A i)] [∀ i, TopologicalSpace (A i)]
---     [∀ i, IsActionTopology R (A i)]: IsActionTopology R (Π i, A i) := by
---   induction n
---   · infer_instance
---   · case succ n IH _ _ _ _ =>
---     specialize IH (A := fun i => A (Fin.castSucc i))
---     sorry
-
 variable {ι : Type*} [Finite ι] {A : ι → Type*} [∀ i, AddCommGroup (A i)]
   [∀ i, Module R (A i)] [∀ i, TopologicalSpace (A i)]
   [∀ i, IsActionTopology R (A i)]
@@ -319,10 +370,10 @@ instance pi : IsActionTopology R (∀ i, A i) := by
 
 end Pi
 
-section bilinear
+section semiring_bilinear
 
 -- I need rings not semirings here, because ` ChooseBasisIndex.fintype` incorrectly(?) needs
--- a ring instead of a semiring
+-- a ring instead of a semiring. This should be fixed.
 variable {R : Type*} [τR : TopologicalSpace R] [CommRing R] [TopologicalRing R]
 
 -- similarly these don't need to be groups
@@ -359,12 +410,7 @@ lemma Module.continuous_bilinear_of_pi_finite (ι : Type*) [Finite ι]
   use Set.univ
   simp [Set.toFinite _]
 
--- Probably this can be beefed up in two distinct ways:
--- Firstly, as it stands the lemma should be provable for semirings.
--- Secind, we should be able to drop Module.Free in the ring case, change elinear.symm
--- into a
--- surjection not a bijection, and then use that quotients coinduce the action
--- topology for groups (proved later, but not using this)
+-- Probably this can be beefed up to semirings.
 lemma Module.continuous_bilinear_of_finite_free [Module.Finite R A] [Module.Free R A]
     (bil : A →ₗ[R] B →ₗ[R] C) : Continuous (fun ab ↦ bil ab.1 ab.2 : (A × B → C)) := by
   let ι := Module.Free.ChooseBasisIndex R A
@@ -382,9 +428,42 @@ lemma Module.continuous_bilinear_of_finite_free [Module.Finite R A] [Module.Free
   · exact continuous_of_linearMap (elinear.toLinearMap ∘ₗ (LinearMap.fst R A B))
   · fun_prop
 
-end bilinear
+end semiring_bilinear
+
+section ring_bilinear
+
+variable {R : Type*} [τR : TopologicalSpace R] [CommRing R] [TopologicalRing R]
+
+variable {A : Type*} [AddCommGroup A] [Module R A] [aA : TopologicalSpace A] [IsActionTopology R A]
+variable {B : Type*} [AddCommGroup B] [Module R B] [aB : TopologicalSpace B] [IsActionTopology R B]
+variable {C : Type*} [AddCommGroup C] [Module R C] [aC : TopologicalSpace C] [IsActionTopology R C]
+
+-- This needs rings though
+lemma Module.continuous_bilinear_of_finite [Module.Finite R A]
+    (bil : A →ₗ[R] B →ₗ[R] C) : Continuous (fun ab ↦ bil ab.1 ab.2 : (A × B → C)) := by
+  obtain ⟨m, f, hf⟩ := Module.Finite.exists_fin' R A
+  let bil' : (Fin m → R) →ₗ[R] B →ₗ[R] C := bil.comp f
+  have := Module.continuous_bilinear_of_pi_finite (Fin m) bil'
+  let φ := f.prodMap (LinearMap.id : B →ₗ[R] B)
+  have foo : Function.Surjective (LinearMap.id : B →ₗ[R] B) :=
+    Function.RightInverse.surjective (congrFun rfl)
+  have hφ : Function.Surjective φ := Function.Surjective.prodMap hf foo
+  have := coinduced_of_surjective hφ
+  rw [isActionTopology R (A × B), ← this, continuous_def]
+  intro U hU
+  rw [isOpen_coinduced, ← Set.preimage_comp]
+  suffices Continuous ((fun ab ↦ (bil ab.1) ab.2) ∘ φ : (Fin m → R) × B → C) by
+    rw [continuous_def] at this
+    convert this _ hU
+    rw [← prod.isActionTopology']
+  rw [show (fun ab ↦ (bil ab.1) ab.2 : A × B → C) ∘ φ = (fun fb ↦ bil' fb.1 fb.2) by
+    ext ⟨a, b⟩
+    simp [bil', φ]]
+  apply Module.continuous_bilinear_of_finite_free
+
+end ring_bilinear
 
-section algebra
+section semiring_algebra
 
 -- these shouldn't be rings, they should be semirings
 variable (R) [CommRing R] [TopologicalSpace R] [TopologicalRing R]
@@ -394,74 +473,36 @@ variable [TopologicalSpace D] [IsActionTopology R D]
 open scoped TensorProduct
 
 @[continuity, fun_prop]
-lemma continuous_mul : Continuous (fun ab ↦ ab.1 * ab.2 : D × D → D) := by
+lemma continuous_mul' : Continuous (fun ab ↦ ab.1 * ab.2 : D × D → D) := by
   letI : TopologicalSpace (D ⊗[R] D) := actionTopology R _
   haveI : IsActionTopology R (D ⊗[R] D) := { isActionTopology' := rfl }
   convert Module.continuous_bilinear_of_finite_free <| LinearMap.mul R D
 
-def Module.topologicalRing : TopologicalRing D where
+-- this should be about top semirings
+def Module.topologicalSemiring : TopologicalSemiring D where
   continuous_add := (isActionTopology_continuousAdd R D).1
-  continuous_mul := continuous_mul R D
-  continuous_neg := continuous_neg R D
+  continuous_mul := continuous_mul' R D
 
-end algebra
+end semiring_algebra
 
-section topology_problem
+section ring_algebra
 
-variable {R : Type*} [τR : TopologicalSpace R] [Ring R] [TopologicalRing R]
-variable {A : Type*} [AddCommGroup A] [Module R A] [aA : TopologicalSpace A] [IsActionTopology R A]
-variable {B : Type*} [AddCommGroup B] [Module R B] [aB : TopologicalSpace B] [IsActionTopology R B]
+-- these shouldn't be rings, they should be semirings
+variable (R) [CommRing R] [TopologicalSpace R] [TopologicalRing R]
+variable (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D]
+variable [TopologicalSpace D] [IsActionTopology R D]
 
--- Here I need the lemma about how quotients are open so I do need groups
--- because this relies on translates of an open being open
-lemma coinduced_of_surjective {φ : A →ₗ[R] B} (hφ : Function.Surjective φ) :
-    TopologicalSpace.coinduced φ (actionTopology R A) = actionTopology R B := by
-  have : Continuous φ := continuous_of_linearMap φ
-  rw [continuous_iff_coinduced_le, isActionTopology R A, isActionTopology R B] at this
-  apply le_antisymm this
-  have : ContinuousAdd A := isActionTopology_continuousAdd R A
-  refine sInf_le ⟨?_, ?_⟩
-  · apply @ContinuousSMul.mk R B _ _ (_)
-    obtain ⟨foo⟩ : ContinuousSMul R A := inferInstance
-    rw [continuous_def] at foo ⊢
-    intro U hU
-    rw [isOpen_coinduced, ← isActionTopology R A] at hU
-    specialize foo _ hU; clear hU
-    rw [← Set.preimage_comp, show φ ∘ (fun p ↦ p.1 • p.2 : R × A → A) =
-      (fun p ↦ p.1 • p.2 : R × B → B) ∘
-      (Prod.map id ⇑φ.toAddMonoidHom) by ext; simp, Set.preimage_comp] at foo
-    clear! aB -- easiest to just remove topology on B completely now so typeclass inference
-    -- never sees it
-    convert isOpenMap_of_coinduced (AddMonoidHom.prodMap (AddMonoidHom.id R) φ.toAddMonoidHom)
-      (_) (_) (_) foo
-    · -- aesop would do this if `Function.surjective_id : Surjective ⇑(AddMonoidHom.id R)`
-      -- was known by it
-      apply (Set.image_preimage_eq _ _).symm
-      rw [AddMonoidHom.coe_prodMap, Prod.map_surjective]
-      exact ⟨Function.surjective_id, by simp_all⟩
-    · -- should `apply continuousprodmap ctrl-space` find `Continuous.prod_map`?
-      apply @Continuous.prod_map _ _ _ _ (_) (_) (_) (_) id φ continuous_id
-      rw [continuous_iff_coinduced_le, isActionTopology R A]
-    · rw [← isActionTopology R A]
-      exact coinduced_prod_eq_prod_coinduced (AddMonoidHom.id R) φ.toAddMonoidHom
-       (Function.surjective_id) hφ
-  · apply @ContinuousAdd.mk _ (_)
-    obtain ⟨bar⟩ := isActionTopology_continuousAdd R A
-    rw [continuous_def] at bar ⊢
-    intro U hU
-    rw [isOpen_coinduced, ← isActionTopology R A] at hU
-    specialize bar _ hU; clear hU
-    rw [← Set.preimage_comp, show φ ∘ (fun p ↦ p.1 + p.2 : A × A → A) =
-      (fun p ↦ p.1 + p.2 : B × B → B) ∘
-      (Prod.map ⇑φ.toAddMonoidHom ⇑φ.toAddMonoidHom) by ext; simp, Set.preimage_comp] at bar
-    clear! aB -- easiest to just remove topology on B completely now
-    convert isOpenMap_of_coinduced (AddMonoidHom.prodMap φ.toAddMonoidHom φ.toAddMonoidHom)
-      (_) (_) (_) bar
-    · aesop
-    · apply @Continuous.prod_map _ _ _ _ (_) (_) (_) (_) <;>
-      · rw [continuous_iff_coinduced_le, isActionTopology R A]; rfl
-    · rw [← isActionTopology R A]
-      exact coinduced_prod_eq_prod_coinduced φ φ hφ hφ
+open scoped TensorProduct
 
+@[continuity, fun_prop]
+lemma continuous_mul : Continuous (fun ab ↦ ab.1 * ab.2 : D × D → D) := by
+  letI : TopologicalSpace (D ⊗[R] D) := actionTopology R _
+  haveI : IsActionTopology R (D ⊗[R] D) := { isActionTopology' := rfl }
+  convert Module.continuous_bilinear_of_finite <| LinearMap.mul R D
+
+def Module.topologicalRing : TopologicalRing D where
+  continuous_add := (isActionTopology_continuousAdd R D).1
+  continuous_mul := continuous_mul R D
+  continuous_neg := continuous_neg R D
 
-end topology_problem
+end ring_algebra