Skip to content

Commit

Permalink
chore: classify broken dot notation porting notes (#11038)
Browse files Browse the repository at this point in the history
Classifies by adding issue number #11036 to porting notes claiming: 

> broken dot notation
  • Loading branch information
pitmonticone authored and riccardobrasca committed Mar 1, 2024
1 parent 035e1e2 commit 60eafa2
Show file tree
Hide file tree
Showing 4 changed files with 28 additions and 28 deletions.
14 changes: 7 additions & 7 deletions Mathlib/Algebra/Category/ModuleCat/Kernels.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -92,22 +92,22 @@ 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_π _ _
#align Module.kernel_iso_ker_inv_kernel_ι ModuleCat.kernelIsoKer_inv_kernel_ι

@[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
Expand All @@ -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
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Module/Torsion.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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

Expand Down
36 changes: 18 additions & 18 deletions Mathlib/LinearAlgebra/Dual.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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⟩
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
_ = _ := ?_
Expand Down Expand Up @@ -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 <|
Expand Down Expand Up @@ -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 φ
Expand Down Expand Up @@ -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,
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 60eafa2

Please sign in to comment.