|
| 1 | +import Mathlib.Algebra.Module.Projective |
| 2 | +import Mathlib.Topology.Algebra.Monoid |
| 3 | + |
| 4 | +section elsewhere |
| 5 | + |
| 6 | +variable {A : Type*} [AddCommGroup A] |
| 7 | +variable {B : Type*} [AddCommGroup B] |
| 8 | + |
| 9 | +lemma AddMonoidHom.sub_mem_ker_iff {A B : Type*} [AddCommGroup A] |
| 10 | + [AddCommGroup B] (φ : A →+ B) {x y : A} : |
| 11 | + x - y ∈ AddMonoidHom.ker φ ↔ φ x = φ y := by |
| 12 | + rw [AddMonoidHom.mem_ker, map_sub, sub_eq_zero] |
| 13 | + |
| 14 | +variable [τA : TopologicalSpace A] [ContinuousAdd A] |
| 15 | +variable [τB : TopologicalSpace B] |
| 16 | + |
| 17 | +lemma isOpenMap_of_coinduced (φ : A →+ B) (hφc : Continuous φ) |
| 18 | + (h : TopologicalSpace.coinduced φ τA = τB) : |
| 19 | + IsOpenMap φ := by |
| 20 | + intro U hU |
| 21 | + rw [← h, isOpen_coinduced] |
| 22 | + suffices ⇑φ ⁻¹' (⇑φ '' U) = ⋃ k ∈ φ.ker, (fun x ↦ x + k) ⁻¹' U by |
| 23 | + exact this ▸ isOpen_biUnion (fun k _ ↦ Continuous.isOpen_preimage (by continuity) _ hU) |
| 24 | + ext x |
| 25 | + constructor |
| 26 | + · rintro ⟨y, hyU, hyx⟩ |
| 27 | + apply Set.mem_iUnion_of_mem (y - x) |
| 28 | + suffices y - x ∈ AddMonoidHom.ker φ by simp_all |
| 29 | + rwa [AddMonoidHom.sub_mem_ker_iff] |
| 30 | + · rintro ⟨_, ⟨k, rfl⟩, _, ⟨hk, rfl⟩, hx⟩ |
| 31 | + use x + k, hx |
| 32 | + rw [AddMonoidHom.map_add, hk, add_zero] |
| 33 | + |
| 34 | +-- **TODO** ask Yury how to golf |
| 35 | +open TopologicalSpace in |
| 36 | +lemma coinduced_prod_eq_prod_coinduced {X Y S T : Type*} [AddCommGroup X] [AddCommGroup Y] |
| 37 | + [AddCommGroup S] [AddCommGroup T] (f : X →+ S) (g : Y →+ T) |
| 38 | + (hf : Function.Surjective f) (hg : Function.Surjective g) |
| 39 | + [τX : TopologicalSpace X] [ContinuousAdd X] [τY : TopologicalSpace Y] [ContinuousAdd Y] : |
| 40 | + coinduced (Prod.map f g) instTopologicalSpaceProd = |
| 41 | + @instTopologicalSpaceProd S T (coinduced f τX) (coinduced g τY) := by |
| 42 | + ext U |
| 43 | + rw [@isOpen_prod_iff, isOpen_coinduced, isOpen_prod_iff] |
| 44 | + constructor |
| 45 | + · intro h s t hst |
| 46 | + obtain ⟨x, rfl⟩ := hf s |
| 47 | + obtain ⟨y, rfl⟩ := hg t |
| 48 | + obtain ⟨V1, V2, hV1, hV2, hx1, hy2, h12⟩ := h x y hst |
| 49 | + use f '' V1, g '' V2, |
| 50 | + @isOpenMap_of_coinduced _ _ _ _ _ _ (coinduced f τX) f |
| 51 | + (by rw [continuous_iff_coinduced_le]) rfl V1 hV1, |
| 52 | + @isOpenMap_of_coinduced _ _ _ _ _ _ (coinduced g τY) g |
| 53 | + (by rw [continuous_iff_coinduced_le]) rfl V2 hV2, |
| 54 | + ⟨x, hx1, rfl⟩, ⟨y, hy2, rfl⟩ |
| 55 | + rintro ⟨s, t⟩ ⟨⟨x', hx', rfl⟩, ⟨y', hy', rfl⟩⟩ |
| 56 | + exact @h12 (x', y') ⟨hx', hy'⟩ |
| 57 | + · intro h x y hxy |
| 58 | + rw [Set.mem_preimage, Prod.map_apply] at hxy |
| 59 | + obtain ⟨U1, U2, hU1, hU2, hx1, hy2, h12⟩ := h (f x) (g y) hxy |
| 60 | + use f ⁻¹' U1, g ⁻¹' U2, hU1, hU2, hx1, hy2 |
| 61 | + intro ⟨x', y'⟩ ⟨hx', hy'⟩ |
| 62 | + exact h12 ⟨hx', hy'⟩ |
| 63 | + |
| 64 | +end elsewhere |
| 65 | + |
| 66 | +section missing_API |
| 67 | + |
| 68 | +variable {R : Type*} [Semiring R] {P : Type*} [AddCommMonoid P] [Module R P] |
| 69 | + |
| 70 | +namespace Module |
| 71 | + |
| 72 | +-- all done for rings bu it should be semirings |
| 73 | + |
| 74 | +/-- Free modules are projective. -/ |
| 75 | +theorem Projective.of_basis' {ι : Type*} (b : Basis ι R P) : Projective R P := by |
| 76 | + -- need P →ₗ (P →₀ R) for definition of projective. |
| 77 | + -- get it from `ι → (P →₀ R)` coming from `b`. |
| 78 | + use b.constr ℕ fun i => Finsupp.single (b i) (1 : R) |
| 79 | + intro m |
| 80 | + simp only [b.constr_apply, mul_one, id, Finsupp.smul_single', Finsupp.total_single, |
| 81 | + map_finsupp_sum] |
| 82 | + exact b.total_repr m |
| 83 | + |
| 84 | +instance (priority := 100) Projective.of_free' [Module.Free R P] : Module.Projective R P := |
| 85 | + .of_basis' <| Module.Free.chooseBasis R P |
| 86 | + |
| 87 | +end Module |
| 88 | + |
| 89 | +end missing_API |
| 90 | + |
| 91 | +theorem TopologicalSpace.prod_mono {α β : Type*} {σ₁ σ₂ : TopologicalSpace α} |
| 92 | + {τ₁ τ₂ : TopologicalSpace β} (hσ : σ₁ ≤ σ₂) (hτ : τ₁ ≤ τ₂) : |
| 93 | + @instTopologicalSpaceProd α β σ₁ τ₁ ≤ @instTopologicalSpaceProd α β σ₂ τ₂ := |
| 94 | + le_inf (le_trans inf_le_left <| induced_mono hσ) |
| 95 | + (le_trans inf_le_right <| induced_mono hτ) |
| 96 | + |
| 97 | +section continuous_smul |
| 98 | + |
| 99 | +variable {R : Type*} [τR : TopologicalSpace R] |
| 100 | +variable {A : Type*} [SMul R A] |
| 101 | +variable {S : Type*} [τS : TopologicalSpace S] {f : S → R} (hf : Continuous f) |
| 102 | +variable {B : Type*} [SMul S B] |
| 103 | + |
| 104 | +-- note: use convert not exact to ensure typeclass inference doesn't try to find topology on B |
| 105 | +lemma induced_continuous_smul [τA : TopologicalSpace A] [ContinuousSMul R A] (g : B →ₑ[f] A) : |
| 106 | + @ContinuousSMul S B _ _ (TopologicalSpace.induced g τA) := by |
| 107 | + convert Inducing.continuousSMul (inducing_induced g) hf (fun {c} {x} ↦ map_smulₛₗ g c x) |
| 108 | + |
| 109 | +lemma induced_continuous_add [AddCommMonoid A] [τA : TopologicalSpace A] [ContinuousAdd A] |
| 110 | + [AddCommMonoid B] (h : B →+ A) : |
| 111 | + @ContinuousAdd B (TopologicalSpace.induced h τA) _ := by |
| 112 | + convert Inducing.continuousAdd h (inducing_induced h) |
| 113 | + |
| 114 | +-- this should be elsewhere |
| 115 | +lemma TopologicalSpace.induced_id (X : Type*) : TopologicalSpace.induced (id : X → X) = id := by |
| 116 | + ext τ S |
| 117 | + constructor |
| 118 | + · rintro ⟨T, hT, rfl⟩ |
| 119 | + exact hT |
| 120 | + · rintro hS |
| 121 | + exact ⟨S, hS, rfl⟩ |
| 122 | + |
| 123 | +-- #check Prod.continuousSMul -- exists and is an instance :-) |
| 124 | +--#check Induced.continuousSMul -- doesn't exist |
| 125 | + |
| 126 | +end continuous_smul |
0 commit comments