refactor: make ContinuousLinearMap.id protected (leanprover-community#30362)

As it is for many other kinds of homomorphisms.

Author: EtienneC30

Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean

@@ -55,7 +55,7 @@ def ConformalAt (f : X → Y) (x : X) :=
   ∃ f' : X →L[ℝ] Y, HasFDerivAt f f' x ∧ IsConformalMap f'
 
 theorem conformalAt_id (x : X) : ConformalAt _root_.id x :=
-  ⟨id ℝ X, hasFDerivAt_id _, isConformalMap_id⟩
+  ⟨.id ℝ X, hasFDerivAt_id _, isConformalMap_id⟩
 
 theorem conformalAt_const_smul {c : ℝ} (h : c ≠ 0) (x : X) : ConformalAt (fun x' : X => c • x') x :=
   ⟨c • ContinuousLinearMap.id ℝ X, (hasFDerivAt_id x).const_smul c, isConformalMap_const_smul h⟩

Mathlib/Analysis/Calculus/FDeriv/Add.lean

@@ -944,11 +944,11 @@ theorem hasFDerivAt_sub_const_iff (c : F) : HasFDerivAt (f · - c) f' x ↔ HasF
 alias ⟨_, HasFDerivAt.sub_const⟩ := hasFDerivAt_sub_const_iff
 
 @[fun_prop]
-theorem hasStrictFDerivAt_sub_const {x : F} (c : F) : HasStrictFDerivAt (· - c) (id 𝕜 F) x :=
+theorem hasStrictFDerivAt_sub_const {x : F} (c : F) : HasStrictFDerivAt (· - c) (.id 𝕜 F) x :=
   (hasStrictFDerivAt_id x).sub_const c
 
 @[fun_prop]
-theorem hasFDerivAt_sub_const {x : F} (c : F) : HasFDerivAt (· - c) (id 𝕜 F) x :=
+theorem hasFDerivAt_sub_const {x : F} (c : F) : HasFDerivAt (· - c) (.id 𝕜 F) x :=
   (hasFDerivAt_id x).sub_const c
 
 @[fun_prop]

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

@@ -713,18 +713,18 @@ section id
 /-! ### Derivative of the identity -/
 
 @[fun_prop]
-theorem hasStrictFDerivAt_id (x : E) : HasStrictFDerivAt id (id 𝕜 E) x :=
+theorem hasStrictFDerivAt_id (x : E) : HasStrictFDerivAt id (.id 𝕜 E) x :=
   .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left <| by simp
 
-theorem hasFDerivAtFilter_id (x : E) (L : Filter E) : HasFDerivAtFilter id (id 𝕜 E) x L :=
+theorem hasFDerivAtFilter_id (x : E) (L : Filter E) : HasFDerivAtFilter id (.id 𝕜 E) x L :=
   .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left <| by simp
 
 @[fun_prop]
-theorem hasFDerivWithinAt_id (x : E) (s : Set E) : HasFDerivWithinAt id (id 𝕜 E) s x :=
+theorem hasFDerivWithinAt_id (x : E) (s : Set E) : HasFDerivWithinAt id (.id 𝕜 E) s x :=
   hasFDerivAtFilter_id _ _
 
 @[fun_prop]
-theorem hasFDerivAt_id (x : E) : HasFDerivAt id (id 𝕜 E) x :=
+theorem hasFDerivAt_id (x : E) : HasFDerivAt id (.id 𝕜 E) x :=
   hasFDerivAtFilter_id _ _
 
 @[simp, fun_prop]
@@ -761,14 +761,14 @@ theorem differentiableOn_id : DifferentiableOn 𝕜 id s :=
   differentiable_id.differentiableOn
 
 @[simp]
-theorem fderiv_id : fderiv 𝕜 id x = id 𝕜 E :=
+theorem fderiv_id : fderiv 𝕜 id x = .id 𝕜 E :=
   HasFDerivAt.fderiv (hasFDerivAt_id x)
 
 @[simp]
 theorem fderiv_id' : fderiv 𝕜 (fun x : E => x) x = ContinuousLinearMap.id 𝕜 E :=
   fderiv_id
 
-theorem fderivWithin_id (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 id s x = id 𝕜 E := by
+theorem fderivWithin_id (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 id s x = .id 𝕜 E := by
   rw [DifferentiableAt.fderivWithin differentiableAt_id hxs]
   exact fderiv_id
 

Mathlib/Analysis/Normed/Operator/Basic.lean

@@ -189,7 +189,7 @@ theorem opNorm_zero : ‖(0 : E →SL[σ₁₂] F)‖ = 0 :=
 
 /-- The norm of the identity is at most `1`. It is in fact `1`, except when the space is trivial
 where it is `0`. It means that one cannot do better than an inequality in general. -/
-theorem norm_id_le : ‖id 𝕜 E‖ ≤ 1 :=
+theorem norm_id_le : ‖ContinuousLinearMap.id 𝕜 E‖ ≤ 1 :=
   opNorm_le_bound _ zero_le_one fun x => by simp
 
 section
@@ -279,10 +279,10 @@ theorem opNorm_add_le : ‖f + g‖ ≤ ‖f‖ + ‖g‖ :=
 
 /-- If there is an element with norm different from `0`, then the norm of the identity equals `1`.
 (Since we are working with seminorms supposing that the space is non-trivial is not enough.) -/
-theorem norm_id_of_nontrivial_seminorm (h : ∃ x : E, ‖x‖ ≠ 0) : ‖id 𝕜 E‖ = 1 :=
+theorem norm_id_of_nontrivial_seminorm (h : ∃ x : E, ‖x‖ ≠ 0) : ‖ContinuousLinearMap.id 𝕜 E‖ = 1 :=
   le_antisymm norm_id_le <| by
     let ⟨x, hx⟩ := h
-    have := (id 𝕜 E).ratio_le_opNorm x
+    have := (ContinuousLinearMap.id 𝕜 E).ratio_le_opNorm x
     rwa [id_apply, div_self hx] at this
 
 theorem opNorm_smul_le {𝕜' : Type*} [NormedField 𝕜'] [NormedSpace 𝕜' F] [SMulCommClass 𝕜₂ 𝕜' F]

Mathlib/Analysis/Normed/Operator/Bilinear.lean

@@ -228,7 +228,7 @@ vector.
 
 This is the continuous version of `LinearMap.applyₗ`. -/
 def apply' : E →SL[σ₁₂] (E →SL[σ₁₂] F) →L[𝕜₂] F :=
-  flip (id 𝕜₂ (E →SL[σ₁₂] F))
+  flip (.id 𝕜₂ (E →SL[σ₁₂] F))
 
 variable {F σ₁₂}
 
@@ -243,7 +243,7 @@ vector.
 
 This is the continuous version of `LinearMap.applyₗ`. -/
 def apply : E →L[𝕜] (E →L[𝕜] Fₗ) →L[𝕜] Fₗ :=
-  flip (id 𝕜 (E →L[𝕜] Fₗ))
+  flip (.id 𝕜 (E →L[𝕜] Fₗ))
 
 variable {𝕜 Fₗ}
 

Mathlib/Analysis/Normed/Operator/Conformal.lean

@@ -42,7 +42,6 @@ noncomputable section
 
 open Function LinearIsometry ContinuousLinearMap
 
-
 /-- A continuous linear map `f'` is said to be conformal if it's
 a nonzero multiple of a linear isometry. -/
 def IsConformalMap {R : Type*} {X Y : Type*} [NormedField R] [SeminormedAddCommGroup X]
@@ -53,15 +52,15 @@ variable {R M N G M' : Type*} [NormedField R] [SeminormedAddCommGroup M] [Semino
   [SeminormedAddCommGroup G] [NormedSpace R M] [NormedSpace R N] [NormedSpace R G]
   [NormedAddCommGroup M'] [NormedSpace R M'] {f : M →L[R] N} {g : N →L[R] G} {c : R}
 
-theorem isConformalMap_id : IsConformalMap (id R M) :=
+theorem isConformalMap_id : IsConformalMap (.id R M) :=
   ⟨1, one_ne_zero, id, by simp⟩
 
 theorem IsConformalMap.smul (hf : IsConformalMap f) {c : R} (hc : c ≠ 0) :
     IsConformalMap (c • f) := by
   rcases hf with ⟨c', hc', li, rfl⟩
   exact ⟨c * c', mul_ne_zero hc hc', li, smul_smul _ _ _⟩
 
-theorem isConformalMap_const_smul (hc : c ≠ 0) : IsConformalMap (c • id R M) :=
+theorem isConformalMap_const_smul (hc : c ≠ 0) : IsConformalMap (c • .id R M) :=
   isConformalMap_id.smul hc
 
 protected theorem LinearIsometry.isConformalMap (f' : M →ₗᵢ[R] N) :

Mathlib/Analysis/Normed/Operator/NormedSpace.lean

@@ -105,13 +105,13 @@ theorem opNorm_zero_iff [RingHomIsometric σ₁₂] : ‖f‖ = 0 ↔ f = 0 :=
 
 /-- If a normed space is non-trivial, then the norm of the identity equals `1`. -/
 @[simp]
-theorem norm_id [Nontrivial E] : ‖id 𝕜 E‖ = 1 := by
+theorem norm_id [Nontrivial E] : ‖ContinuousLinearMap.id 𝕜 E‖ = 1 := by
   refine norm_id_of_nontrivial_seminorm ?_
   obtain ⟨x, hx⟩ := exists_ne (0 : E)
   exact ⟨x, ne_of_gt (norm_pos_iff.2 hx)⟩
 
 @[simp]
-lemma nnnorm_id [Nontrivial E] : ‖id 𝕜 E‖₊ = 1 := NNReal.eq norm_id
+lemma nnnorm_id [Nontrivial E] : ‖ContinuousLinearMap.id 𝕜 E‖₊ = 1 := NNReal.eq norm_id
 
 instance normOneClass [Nontrivial E] : NormOneClass (E →L[𝕜] E) :=
   ⟨norm_id⟩

Mathlib/Topology/Algebra/Module/Equiv.lean

@@ -1095,11 +1095,12 @@ lemma IsInvertible.comp {g : M₂ →L[R] M₃} {f : M →L[R] M₂}
   exact ⟨M.trans N, rfl⟩
 
 lemma IsInvertible.of_inverse {f : M →L[R] M₂} {g : M₂ →L[R] M}
-    (hf : f ∘L g = id R M₂) (hg : g ∘L f = id R M) :
+    (hf : f ∘L g = .id R M₂) (hg : g ∘L f = .id R M) :
     f.IsInvertible :=
   ⟨ContinuousLinearEquiv.equivOfInverse' _ _ hf hg, rfl⟩
 
-lemma inverse_eq {f : M →L[R] M₂} {g : M₂ →L[R] M} (hf : f ∘L g = id R M₂) (hg : g ∘L f = id R M) :
+lemma inverse_eq {f : M →L[R] M₂} {g : M₂ →L[R] M}
+    (hf : f ∘L g = .id R M₂) (hg : g ∘L f = .id R M) :
     f.inverse = g := by
   have : f = ContinuousLinearEquiv.equivOfInverse' f g hf hg := rfl
   rw [this, inverse_equiv]
@@ -1202,7 +1203,7 @@ theorem ringInverse_eq_inverse : Ring.inverse = inverse (R := R) (M := M) := by
 @[deprecated (since := "2025-04-22")]
 alias ring_inverse_eq_map_inverse := ringInverse_eq_inverse
 
-@[simp] theorem inverse_id : (id R M).inverse = id R M := by
+@[simp] theorem inverse_id : (ContinuousLinearMap.id R M).inverse = .id R M := by
   rw [← ringInverse_eq_inverse]
   exact Ring.inverse_one _
 

Mathlib/Topology/Algebra/Module/LinearMap.lean

@@ -313,34 +313,34 @@ section
 variable (R₁ M₁)
 
 /-- the identity map as a continuous linear map. -/
-def id : M₁ →L[R₁] M₁ :=
+protected def id : M₁ →L[R₁] M₁ :=
   ⟨LinearMap.id, continuous_id⟩
 
 end
 
 instance one : One (M₁ →L[R₁] M₁) :=
-  ⟨id R₁ M₁⟩
+  ⟨.id R₁ M₁⟩
 
-theorem one_def : (1 : M₁ →L[R₁] M₁) = id R₁ M₁ :=
+theorem one_def : (1 : M₁ →L[R₁] M₁) = .id R₁ M₁ :=
   rfl
 
-theorem id_apply (x : M₁) : id R₁ M₁ x = x :=
+theorem id_apply (x : M₁) : ContinuousLinearMap.id R₁ M₁ x = x :=
   rfl
 
 @[simp, norm_cast]
-theorem coe_id : (id R₁ M₁ : M₁ →ₗ[R₁] M₁) = LinearMap.id :=
+theorem coe_id : (ContinuousLinearMap.id R₁ M₁ : M₁ →ₗ[R₁] M₁) = LinearMap.id :=
   rfl
 
 @[simp, norm_cast]
-theorem coe_id' : ⇑(id R₁ M₁) = _root_.id :=
+theorem coe_id' : ⇑(ContinuousLinearMap.id R₁ M₁) = id :=
   rfl
 
 @[simp, norm_cast]
 theorem toContinuousAddMonoidHom_id :
-    (id R₁ M₁ : ContinuousAddMonoidHom M₁ M₁) = .id _ := rfl
+    (ContinuousLinearMap.id R₁ M₁ : ContinuousAddMonoidHom M₁ M₁) = .id _ := rfl
 
 @[simp, norm_cast]
-theorem coe_eq_id {f : M₁ →L[R₁] M₁} : (f : M₁ →ₗ[R₁] M₁) = LinearMap.id ↔ f = id _ _ := by
+theorem coe_eq_id {f : M₁ →L[R₁] M₁} : (f : M₁ →ₗ[R₁] M₁) = LinearMap.id ↔ f = .id _ _ := by
   rw [← coe_id, coe_inj]
 
 @[simp]
@@ -441,11 +441,11 @@ theorem comp_apply (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M
   rfl
 
 @[simp]
-theorem comp_id (f : M₁ →SL[σ₁₂] M₂) : f.comp (id R₁ M₁) = f :=
+theorem comp_id (f : M₁ →SL[σ₁₂] M₂) : f.comp (.id R₁ M₁) = f :=
   ext fun _x => rfl
 
 @[simp]
-theorem id_comp (f : M₁ →SL[σ₁₂] M₂) : (id R₂ M₂).comp f = f :=
+theorem id_comp (f : M₁ →SL[σ₁₂] M₂) : (ContinuousLinearMap.id R₂ M₂).comp f = f :=
   ext fun _x => rfl
 
 section
@@ -887,7 +887,7 @@ variable {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁]
 `LinearMap.range f₂`. -/
 def projKerOfRightInverse [IsTopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M)
     (h : Function.RightInverse f₂ f₁) : M →L[R] LinearMap.ker f₁ :=
-  (id R M - f₂.comp f₁).codRestrict (LinearMap.ker f₁) fun x => by simp [h (f₁ x)]
+  (.id R M - f₂.comp f₁).codRestrict (LinearMap.ker f₁) fun x => by simp [h (f₁ x)]
 
 @[simp]
 theorem coe_projKerOfRightInverse_apply [IsTopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂)
@@ -1141,7 +1141,8 @@ theorem ClosedComplemented.exists_isClosed_isCompl {p : Submodule R M} [T1Space
 protected theorem ClosedComplemented.isClosed [IsTopologicalAddGroup M] [T1Space M]
     {p : Submodule R M} (h : ClosedComplemented p) : IsClosed (p : Set M) := by
   rcases h with ⟨f, hf⟩
-  have : ker (id R M - p.subtypeL.comp f) = p := LinearMap.ker_id_sub_eq_of_proj hf
+  have : ker (ContinuousLinearMap.id R M - p.subtypeL.comp f) = p :=
+    LinearMap.ker_id_sub_eq_of_proj hf
   exact this ▸ isClosed_ker _
 
 @[simp]
@@ -1150,7 +1151,8 @@ theorem closedComplemented_bot : ClosedComplemented (⊥ : Submodule R M) :=
 
 @[simp]
 theorem closedComplemented_top : ClosedComplemented (⊤ : Submodule R M) :=
-  ⟨(id R M).codRestrict ⊤ fun _x => trivial, fun x => Subtype.ext_iff.2 <| by simp⟩
+  ⟨(ContinuousLinearMap.id R M).codRestrict ⊤ fun _x => trivial,
+    fun x => Subtype.ext_iff.2 <| by simp⟩
 
 end Submodule
 

Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean

@@ -53,11 +53,11 @@ variable (R M₁ M₂)
 
 /-- The left injection into a product is a continuous linear map. -/
 def inl : M₁ →L[R] M₁ × M₂ :=
-  (id R M₁).prod 0
+  (ContinuousLinearMap.id R M₁).prod 0
 
 /-- The right injection into a product is a continuous linear map. -/
 def inr : M₂ →L[R] M₁ × M₂ :=
-  (0 : M₂ →L[R] M₁).prod (id R M₂)
+  (0 : M₂ →L[R] M₁).prod (.id R M₂)
 
 end
 
@@ -116,7 +116,7 @@ theorem coe_snd' : ⇑(snd R M₁ M₂) = Prod.snd :=
   rfl
 
 @[simp]
-theorem fst_prod_snd : (fst R M₁ M₂).prod (snd R M₁ M₂) = id R (M₁ × M₂) :=
+theorem fst_prod_snd : (fst R M₁ M₂).prod (snd R M₁ M₂) = .id R (M₁ × M₂) :=
   ext fun ⟨_x, _y⟩ => rfl
 
 @[simp]