From e2ddbf6c3e6a41b15a2d4e605548a880defe879f Mon Sep 17 00:00:00 2001 From: syur2 Date: Sun, 13 Oct 2024 12:00:30 +0800 Subject: [PATCH] fix the name error between LocalizedModule.map' and mapfromlift --- .../MissingLemmas/LocalizedModule.lean | 42 ++++++++++++++----- .../MissingLemmas/TensorProduct.lean | 12 +++--- 2 files changed, 36 insertions(+), 18 deletions(-) diff --git a/ModuleLocalProperties/MissingLemmas/LocalizedModule.lean b/ModuleLocalProperties/MissingLemmas/LocalizedModule.lean index 21d2835..0749aec 100644 --- a/ModuleLocalProperties/MissingLemmas/LocalizedModule.lean +++ b/ModuleLocalProperties/MissingLemmas/LocalizedModule.lean @@ -106,14 +106,34 @@ lemma LiftOnLocalizationModule_unique (g : LocalizedModule S M →ₗ[R] N) end LocalizedModule -section LocalizedModule.map'' +section LocalizedModule.map' + +namespace LocalizedModule + +variable {R : Type*} [CommSemiring R] (S : Submonoid R) {M N : Type*} + [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] + +noncomputable def map' : (M →ₗ[R] N) →ₗ[R] LocalizedModule S M →ₗ[Localization S] LocalizedModule S N where + toFun := fun f => LinearMap.extendScalarsOfIsLocalization S _ <| map S f + map_add' := by + intro f g + ext x + dsimp + rw [map_add, LinearMap.add_apply] + map_smul' := by + intro r f + ext x + dsimp + rw [map_smul, LinearMap.smul_apply] +end LocalizedModule +section LocalizedModule.maplift -- This is LocalizedModule.map and LocalizedModule.map' with out using IsLocalizedModule.map namespace LocalizedModule variable {R : Type*} [CommSemiring R] (S : Submonoid R) {M N : Type*} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] -noncomputable def map'' : (M →ₗ[R] N) →ₗ[R] LocalizedModule S M →ₗ[R] LocalizedModule S N where +noncomputable def mapfromlift' : (M →ₗ[R] N) →ₗ[R] LocalizedModule S M →ₗ[R] LocalizedModule S N where toFun := fun f => LiftOnLocalizationModule' S <| mkLinearMap S N ∘ₗ f map_add' := by intro f g @@ -132,14 +152,14 @@ noncomputable def map'' : (M →ₗ[R] N) →ₗ[R] LocalizedModule S M →ₗ[R Function.comp_apply, LinearMap.smul_apply, map_smul] rw[smul_comm] -lemma map''_mk (f : M →ₗ[R] N) (m : M) (s : S) : map'' S f (mk m s) = mk (f m) s := by +lemma mapfromlift'_mk (f : M →ₗ[R] N) (m : M) (s : S) : mapfromlift' S f (mk m s) = mk (f m) s := by show (LiftOnLocalizationModule' S (mkLinearMap S N ∘ₗ f)) (mk m s) = mk (f m) s rw[LiftOnLocalizationModule'_mk, LinearMap.coe_comp, Function.comp_apply, mkLinearMap_apply, ← mk_right_smul_mk_den_one (s := s)] -noncomputable def map' : +noncomputable def mapfromlift : (M →ₗ[R] N) →ₗ[R] LocalizedModule S M →ₗ[Localization S] LocalizedModule S N where - toFun := fun f => LinearMap.extendScalarsOfIsLocalization S _ <| map'' S f + toFun := fun f => LinearMap.extendScalarsOfIsLocalization S _ <| mapfromlift' S f map_add' := by intro f g ext x @@ -151,8 +171,8 @@ noncomputable def map' : dsimp rw [map_smul, LinearMap.smul_apply] -lemma map'_mk (f : M →ₗ[R] N) (m : M) (s : S) : map' S f (mk m s) = mk (f m) s := - map''_mk _ _ _ _ +lemma mapfromlift_mk (f : M →ₗ[R] N) (m : M) (s : S) : mapfromlift S f (mk m s) = mk (f m) s := + mapfromlift'_mk _ _ _ _ end LocalizedModule @@ -181,23 +201,23 @@ noncomputable def {R : Type*} [CommSemiring R] (S : Submonoid R) {M N : Type*} noncomputable def LocalizedMapLift' : LocalizedModule S (M →ₗ[R] N) →ₗ[R] LocalizedModule S M →ₗ[R] LocalizedModule S N := LiftOnLocalizationModule' _ (M := (M →ₗ[R] N)) (N := LocalizedModule S M →ₗ[R] LocalizedModule S N) - <| map'' _ + <| mapfromlift' _ lemma LocalizedMapLift'_mk (f : M →ₗ[R] N) (m : M) (s t : S) : LocalizedMapLift' S (mk f s) (mk m t) = mk (f m) (s * t) := by unfold LocalizedMapLift' - rw [LiftOnLocalizationModule'_mk, LinearMap.smul_apply, map''_mk, mk_right_smul_mk] + rw [LiftOnLocalizationModule'_mk, LinearMap.smul_apply, mapfromlift'_mk, mk_right_smul_mk] noncomputable def LocalizedMapLift : LocalizedModule S (M →ₗ[R] N) →ₗ[Localization S] LocalizedModule S M →ₗ[Localization S] LocalizedModule S N := LiftOnLocalizationModule _ (M := (M →ₗ[R] N)) (N := LocalizedModule S M →ₗ[Localization S] LocalizedModule S N) - <| map' _ + <| mapfromlift _ lemma LocalizedMapLift_mk (f : M →ₗ[R] N) (m : M) (s t : S) : LocalizedMapLift S (mk f s) (mk m t) = mk (f m) (s * t) := by unfold LocalizedMapLift - rw [LiftOnLocalizationModule_mk, LinearMap.smul_apply, map'_mk, mk_right_smul_mk] + rw [LiftOnLocalizationModule_mk, LinearMap.smul_apply, mapfromlift_mk, mk_right_smul_mk] end LocalizedModule diff --git a/ModuleLocalProperties/MissingLemmas/TensorProduct.lean b/ModuleLocalProperties/MissingLemmas/TensorProduct.lean index a6516f4..0c45939 100644 --- a/ModuleLocalProperties/MissingLemmas/TensorProduct.lean +++ b/ModuleLocalProperties/MissingLemmas/TensorProduct.lean @@ -20,12 +20,12 @@ variable {R : Type*} {M N P : Type*} [CommSemiring R] (S : Submonoid R) [AddComm noncomputable def BilinearMap : LocalizedModule S M →ₗ[Localization S] LocalizedModule S N →ₗ[Localization S] LocalizedModule S P := - LocalizedMapLift S ∘ₗ (map' (M := M) (N := N →ₗ[R] P) S f) + LocalizedMapLift S ∘ₗ (mapfromlift (M := M) (N := N →ₗ[R] P) S f) lemma BilinearMap_mk (m : M) (n : N) (s t : S) : BilinearMap S f (mk m s) (mk n t) = mk (f m n) (s * t) :=by unfold BilinearMap - rw [LinearMap.coe_comp, Function.comp_apply, map'_mk, LocalizedMapLift_mk] + rw [LinearMap.coe_comp, Function.comp_apply, mapfromlift_mk, LocalizedMapLift_mk] end LocalizedModule @@ -89,24 +89,22 @@ lemma InvTensorProductMap_apply' (m : M) (n : N) (s t : S) : lemma TensorProductMap_rightInv : TensorProductMap S ∘ₗ (InvTensorProductMap S (M := M) (N := N)) = LinearMap.id := by - unfold TensorProductMap ext x induction' x with y s dsimp induction' y with m n m n hm hn · simp only [zero_mk, map_zero] - · rw [InvTensorProductMap_apply, map_smul, TensorProduct.lift.tmul, TensorProductBilinearMap_mk, + · rw [InvTensorProductMap_apply, map_smul, TensorProductMap_mk, one_mul, mk_right_smul_mk_den_one] · rw [mk_add_mk_right, map_add, map_add, hm, hn] lemma TensorProductMap_leftInv : - InvTensorProductMap S ∘ₗ (TensorProductMap S (M := M) (N := N)) = LinearMap.id :=by - unfold TensorProductMap + InvTensorProductMap S ∘ₗ (TensorProductMap S (M := M) (N := N)) = LinearMap.id := by ext x y dsimp induction' x with m s induction' y with n t - rw [TensorProductBilinearMap_mk, InvTensorProductMap_apply'] + rw [TensorProductMap_mk, InvTensorProductMap_apply'] noncomputable def TensorProductEquiv : (LocalizedModule S M) ⊗[Localization S] (LocalizedModule S N) ≃ₗ[Localization S] LocalizedModule S (M ⊗[R] N) :=