From 60eafa2817475b2f35d98c00c96035b75c54f13b Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 28 Feb 2024 16:59:04 +0000 Subject: [PATCH] chore: classify `broken dot notation` porting notes (#11038) Classifies by adding issue number #11036 to porting notes claiming: > broken dot notation --- .../Algebra/Category/ModuleCat/Kernels.lean | 14 ++++---- Mathlib/Algebra/Module/Torsion.lean | 4 +-- Mathlib/LinearAlgebra/Dual.lean | 36 +++++++++---------- .../Matrix/SpecialLinearGroup.lean | 2 +- 4 files changed, 28 insertions(+), 28 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Kernels.lean b/Mathlib/Algebra/Category/ModuleCat/Kernels.lean index dff5ea92e79606..06c7bce0a2a0b3 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Kernels.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Kernels.lean @@ -36,7 +36,7 @@ def kernelCone : KernelFork f := def kernelIsLimit : IsLimit (kernelCone f) := Fork.IsLimit.mk _ (fun s => - -- Porting note: broken dot notation on LinearMap.ker + -- Porting note (#11036): broken dot notation on LinearMap.ker LinearMap.codRestrict (LinearMap.ker f) (Fork.ι s) fun c => LinearMap.mem_ker.2 <| by -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 @@ -58,10 +58,10 @@ def cokernelIsColimit : IsColimit (cokernelCocone f) := (fun s => f.range.liftQ (Cofork.π s) <| LinearMap.range_le_ker_iff.2 <| CokernelCofork.condition s) (fun s => f.range.liftQ_mkQ (Cofork.π s) _) fun s m h => by - -- Porting note: broken dot notation + -- Porting note (#11036): broken dot notation haveI : Epi (asHom (LinearMap.range f).mkQ) := (epi_iff_range_eq_top _).mpr (Submodule.range_mkQ _) - -- Porting note: broken dot notation + -- Porting note (#11036): broken dot notation apply (cancel_epi (asHom (LinearMap.range f).mkQ)).1 convert h -- Porting note: no longer necessary @@ -92,14 +92,14 @@ variable {G H : ModuleCat.{v} R} (f : G ⟶ H) agrees with the usual module-theoretical kernel. -/ noncomputable def kernelIsoKer {G H : ModuleCat.{v} R} (f : G ⟶ H) : - -- Porting note: broken dot notation + -- Porting note (#11036): broken dot notation kernel f ≅ ModuleCat.of R (LinearMap.ker f) := limit.isoLimitCone ⟨_, kernelIsLimit f⟩ #align Module.kernel_iso_ker ModuleCat.kernelIsoKer -- We now show this isomorphism commutes with the inclusion of the kernel into the source. @[simp, elementwise] - -- Porting note: broken dot notation + -- Porting note (#11036): broken dot notation theorem kernelIsoKer_inv_kernel_ι : (kernelIsoKer f).inv ≫ kernel.ι f = (LinearMap.ker f).subtype := limit.isoLimitCone_inv_π _ _ @@ -107,7 +107,7 @@ theorem kernelIsoKer_inv_kernel_ι : (kernelIsoKer f).inv ≫ kernel.ι f = @[simp, elementwise] theorem kernelIsoKer_hom_ker_subtype : - -- Porting note: broken dot notation + -- Porting note (#11036): broken dot notation (kernelIsoKer f).hom ≫ (LinearMap.ker f).subtype = kernel.ι f := IsLimit.conePointUniqueUpToIso_inv_comp _ (limit.isLimit _) WalkingParallelPair.zero #align Module.kernel_iso_ker_hom_ker_subtype ModuleCat.kernelIsoKer_hom_ker_subtype @@ -116,7 +116,7 @@ theorem kernelIsoKer_hom_ker_subtype : agrees with the usual module-theoretical quotient. -/ noncomputable def cokernelIsoRangeQuotient {G H : ModuleCat.{v} R} (f : G ⟶ H) : - -- Porting note: broken dot notation + -- Porting note (#11036): broken dot notation cokernel f ≅ ModuleCat.of R (H ⧸ LinearMap.range f) := colimit.isoColimitCocone ⟨_, cokernelIsColimit f⟩ #align Module.cokernel_iso_range_quotient ModuleCat.cokernelIsoRangeQuotient diff --git a/Mathlib/Algebra/Module/Torsion.lean b/Mathlib/Algebra/Module/Torsion.lean index e6d665b78942bf..a4432cc1787afd 100644 --- a/Mathlib/Algebra/Module/Torsion.lean +++ b/Mathlib/Algebra/Module/Torsion.lean @@ -74,7 +74,7 @@ variable (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M] /-- The torsion ideal of `x`, containing all `a` such that `a • x = 0`.-/ @[simps!] def torsionOf (x : M) : Ideal R := - -- Porting note: broken dot notation on LinearMap.ker Lean4#1910 + -- Porting note (#11036): broken dot notation on LinearMap.ker Lean4#1910 LinearMap.ker (LinearMap.toSpanSingleton R M x) #align ideal.torsion_of Ideal.torsionOf @@ -163,7 +163,7 @@ namespace Submodule `a • x = 0`. -/ @[simps!] def torsionBy (a : R) : Submodule R M := - -- Porting note: broken dot notation on LinearMap.ker Lean4#1910 + -- Porting note (#11036): broken dot notation on LinearMap.ker Lean4#1910 LinearMap.ker (DistribMulAction.toLinearMap R M a) #align submodule.torsion_by Submodule.torsionBy diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index 9b89bcf813069a..fe9f93f51bc66e 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -369,12 +369,12 @@ theorem toDual_inj (m : M) (a : b.toDual m = 0) : m = 0 := b.toDual_injective (by rwa [_root_.map_zero]) #align basis.to_dual_inj Basis.toDual_inj --- Porting note: broken dot notation lean4#1910 LinearMap.ker +-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.ker theorem toDual_ker : LinearMap.ker b.toDual = ⊥ := ker_eq_bot'.mpr b.toDual_inj #align basis.to_dual_ker Basis.toDual_ker --- Porting note: broken dot notation lean4#1910 LinearMap.range +-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range theorem toDual_range [Finite ι] : LinearMap.range b.toDual = ⊤ := by refine' eq_top_iff'.2 fun f => _ let lin_comb : ι →₀ R := Finsupp.equivFunOnFinite.symm fun i => f (b i) @@ -491,7 +491,7 @@ theorem eval_ker {ι : Type*} (b : Basis ι R M) : exact (Basis.forall_coord_eq_zero_iff _).mp fun i => hm (b.coord i) #align basis.eval_ker Basis.eval_ker --- Porting note: broken dot notation lean4#1910 LinearMap.range +-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range theorem eval_range {ι : Type*} [Finite ι] (b : Basis ι R M) : LinearMap.range (Dual.eval R M) = ⊤ := by classical @@ -543,7 +543,7 @@ section variable (K) (V) --- Porting note: broken dot notation lean4#1910 LinearMap.ker +-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.ker theorem eval_ker : LinearMap.ker (eval K V) = ⊥ := by classical exact (Module.Free.chooseBasis K V).eval_ker #align module.eval_ker Module.eval_ker @@ -619,7 +619,7 @@ theorem dual_rank_eq [Module.Finite K V] : (Module.Free.chooseBasis K V).dual_rank_eq #align module.dual_rank_eq Module.dual_rank_eq --- Porting note: broken dot notation lean4#1910 LinearMap.range +-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range theorem erange_coe [Module.Finite K V] : LinearMap.range (eval K V) = ⊤ := (Module.Free.chooseBasis K V).eval_range #align module.erange_coe Module.erange_coe @@ -902,7 +902,7 @@ theorem dualRestrict_apply (W : Submodule R M) (φ : Module.Dual R M) (x : W) : that `φ w = 0` for all `w ∈ W`. -/ def dualAnnihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (W : Submodule R M) : Submodule R <| Module.Dual R M := --- Porting note: broken dot notation lean4#1910 LinearMap.ker +-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.ker LinearMap.ker W.dualRestrict #align submodule.dual_annihilator Submodule.dualAnnihilator @@ -916,7 +916,7 @@ theorem mem_dualAnnihilator (φ : Module.Dual R M) : φ ∈ W.dualAnnihilator /-- That $\operatorname{ker}(\iota^* : V^* \to W^*) = \operatorname{ann}(W)$. This is the definition of the dual annihilator of the submodule $W$. -/ theorem dualRestrict_ker_eq_dualAnnihilator (W : Submodule R M) : - -- Porting note: broken dot notation lean4#1910 LinearMap.ker + -- Porting note (#11036): broken dot notation lean4#1910 LinearMap.ker LinearMap.ker W.dualRestrict = W.dualAnnihilator := rfl #align submodule.dual_restrict_ker_eq_dual_annihilator Submodule.dualRestrict_ker_eq_dualAnnihilator @@ -1171,7 +1171,7 @@ theorem quotAnnihilatorEquiv_apply (W : Subspace K V) (φ : Module.Dual K V) : #align subspace.quot_annihilator_equiv_apply Subspace.quotAnnihilatorEquiv_apply /-- The natural isomorphism from the dual of a subspace `W` to `W.dualLift.range`. -/ --- Porting note: broken dot notation lean4#1910 LinearMap.range +-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range noncomputable def dualEquivDual (W : Subspace K V) : Module.Dual K W ≃ₗ[K] LinearMap.range W.dualLift := LinearEquiv.ofInjective _ dualLift_injective @@ -1216,7 +1216,7 @@ theorem dualAnnihilator_dualAnnihilator_eq (W : Subspace K V) : #align subspace.dual_annihilator_dual_annihilator_eq Subspace.dualAnnihilator_dualAnnihilator_eq /-- The quotient by the dual is isomorphic to its dual annihilator. -/ --- Porting note: broken dot notation lean4#1910 LinearMap.range +-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range noncomputable def quotDualEquivAnnihilator (W : Subspace K V) : (Module.Dual K V ⧸ LinearMap.range W.dualLift) ≃ₗ[K] W.dualAnnihilator := LinearEquiv.quotEquivOfQuotEquiv <| LinearEquiv.trans W.quotAnnihilatorEquiv W.dualEquivDual @@ -1268,7 +1268,7 @@ variable [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M variable (f : M₁ →ₗ[R] M₂) --- Porting note: broken dot notation lean4#1910 LinearMap.ker +-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.ker theorem ker_dualMap_eq_dualAnnihilator_range : LinearMap.ker f.dualMap = f.range.dualAnnihilator := by ext @@ -1277,7 +1277,7 @@ theorem ker_dualMap_eq_dualAnnihilator_range : rfl #align linear_map.ker_dual_map_eq_dual_annihilator_range LinearMap.ker_dualMap_eq_dualAnnihilator_range --- Porting note: broken dot notation lean4#1910 LinearMap.range +-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range theorem range_dualMap_le_dualAnnihilator_ker : LinearMap.range f.dualMap ≤ f.ker.dualAnnihilator := by rintro _ ⟨ψ, rfl⟩ @@ -1339,7 +1339,7 @@ theorem dualPairing_apply {W : Submodule R M} (φ : Module.Dual R M) (x : W) : rfl #align submodule.dual_pairing_apply Submodule.dualPairing_apply --- Porting note: broken dot notation lean4#1910 LinearMap.range +-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range /-- That $\operatorname{im}(q^* : (V/W)^* \to V^*) = \operatorname{ann}(W)$. -/ theorem range_dualMap_mkQ_eq (W : Submodule R M) : LinearMap.range W.mkQ.dualMap = W.dualAnnihilator := by @@ -1362,7 +1362,7 @@ def dualQuotEquivDualAnnihilator (W : Submodule R M) : Module.Dual R (M ⧸ W) ≃ₗ[R] W.dualAnnihilator := LinearEquiv.ofLinear (W.mkQ.dualMap.codRestrict W.dualAnnihilator fun φ => --- Porting note: broken dot notation lean4#1910 LinearMap.mem_range_self +-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.mem_range_self W.range_dualMap_mkQ_eq ▸ LinearMap.mem_range_self W.mkQ.dualMap φ) W.dualCopairing (by ext; rfl) (by ext; rfl) #align submodule.dual_quot_equiv_dual_annihilator Submodule.dualQuotEquivDualAnnihilator @@ -1421,7 +1421,7 @@ namespace LinearMap open Submodule --- Porting note: broken dot notation lean4#1910 LinearMap.range +-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range theorem range_dualMap_eq_dualAnnihilator_ker_of_surjective (f : M →ₗ[R] M') (hf : Function.Surjective f) : LinearMap.range f.dualMap = f.ker.dualAnnihilator := ((f.quotKerEquivOfSurjective hf).dualMap.range_comp _).trans f.ker.range_dualMap_mkQ_eq @@ -1436,7 +1436,7 @@ theorem range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective (f : M rw [← range_eq_top, range_rangeRestrict] have := range_dualMap_eq_dualAnnihilator_ker_of_surjective f.rangeRestrict rr_surj convert this using 1 - -- Porting note: broken dot notation lean4#1910 + -- Porting note (#11036): broken dot notation lean4#1910 · calc _ = range ((range f).subtype.comp f.rangeRestrict).dualMap := by simp _ = _ := ?_ @@ -1479,7 +1479,7 @@ theorem dualMap_surjective_of_injective {f : V₁ →ₗ[K] V₂} (hf : Function ⟨φ.comp f', ext fun x ↦ congr(φ <| $hf' x)⟩ #align linear_map.dual_map_surjective_of_injective LinearMap.dualMap_surjective_of_injective - -- Porting note: broken dot notation lean4#1910 LinearMap.range + -- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range theorem range_dualMap_eq_dualAnnihilator_ker (f : V₁ →ₗ[K] V₂) : LinearMap.range f.dualMap = f.ker.dualAnnihilator := range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective f <| @@ -1535,7 +1535,7 @@ theorem dualAnnihilator_inf_eq (W W' : Subspace K V₁) : (W ⊓ W').dualAnnihilator = W.dualAnnihilator ⊔ W'.dualAnnihilator := by refine' le_antisymm _ (sup_dualAnnihilator_le_inf W W') let F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (Submodule.mkQ W).prod (Submodule.mkQ W') - -- Porting note: broken dot notation lean4#1910 LinearMap.ker + -- Porting note (#11036): broken dot notation lean4#1910 LinearMap.ker have : LinearMap.ker F = W ⊓ W' := by simp only [F, LinearMap.ker_prod, ker_mkQ] rw [← this, ← LinearMap.range_dualMap_eq_dualAnnihilator_ker] intro φ @@ -1594,7 +1594,7 @@ namespace LinearMap @[simp] theorem finrank_range_dualMap_eq_finrank_range (f : V₁ →ₗ[K] V₂) : - -- Porting note: broken dot notation lean4#1910 + -- Porting note (#11036): broken dot notation lean4#1910 finrank K (LinearMap.range f.dualMap) = finrank K (LinearMap.range f) := by rw [congr_arg dualMap (show f = (range f).subtype.comp f.rangeRestrict by rfl), ← dualMap_comp_dualMap, range_comp, diff --git a/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean b/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean index 7832c4ed861a7d..8adc11fab640a0 100644 --- a/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean +++ b/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean @@ -239,7 +239,7 @@ def toGL : SpecialLinearGroup n R →* GeneralLinearGroup R (n → R) := set_option linter.uppercaseLean3 false in #align matrix.special_linear_group.to_GL Matrix.SpecialLinearGroup.toGL --- Porting note: broken dot notation +-- Porting note (#11036): broken dot notation theorem coe_toGL (A : SpecialLinearGroup n R) : SpecialLinearGroup.toGL A = A.toLin'.toLinearMap := rfl set_option linter.uppercaseLean3 false in