chore: Rename Embedding to IsEmbedding (#18133)

`Function.Embedding` is a type while `Embedding` is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards
1. renaming `Embedding` to `IsEmbedding` and similarly for neighboring declarations (which `Embedding` is)
2. namespacing it inside `Topology`

Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

@@ -63,7 +63,7 @@ lemma eq_inf : @IsClosedImmersion = (topologically IsClosedEmbedding) ⊓
 lemma iff_isPreimmersion {X Y : Scheme} {f : X ⟶ Y} :
     IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (Set.range f.base) := by
   rw [and_comm, isClosedImmersion_iff, isPreimmersion_iff, ← and_assoc, isClosedEmbedding_iff,
-    @and_comm (Embedding _)]
+    @and_comm (IsEmbedding _)]
 
 lemma of_isPreimmersion {X Y : Scheme} (f : X ⟶ Y) [IsPreimmersion f]
     (hf : IsClosed (Set.range f.base)) : IsClosedImmersion f :=

Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean

@@ -76,7 +76,7 @@ instance [IsImmersion f] : IsClosedImmersion f.liftCoborder := by
   have : IsPreimmersion f.liftCoborder := .of_comp f.liftCoborder f.coborderRange.ι
   refine .of_isPreimmersion _ ?_
   convert isClosed_preimage_val_coborder
-  apply Set.image_injective.mpr f.coborderRange.ι.embedding.inj
+  apply Set.image_injective.mpr f.coborderRange.ι.isEmbedding.inj
   rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.comp_base, f.liftCoborder_ι]
   exact (Set.image_preimage_eq_of_subset (by simpa using subset_coborder)).symm
 
@@ -121,7 +121,7 @@ instance : MorphismProperty.IsMultiplicative @IsImmersion where
   comp_mem {X Y Z} f g hf hg := by
     refine { __ := inferInstanceAs (IsPreimmersion (f ≫ g)), isLocallyClosed_range := ?_ }
     simp only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp]
-    exact f.isLocallyClosed_range.image g.embedding.toInducing g.isLocallyClosed_range
+    exact f.isLocallyClosed_range.image g.isEmbedding.toInducing g.isLocallyClosed_range
 
 instance comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsImmersion f]
     [IsImmersion g] : IsImmersion (f ≫ g) :=
@@ -141,7 +141,7 @@ theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsImmersion g]
     [IsImmersion (f ≫ g)] : IsImmersion f where
   __ := IsPreimmersion.of_comp f g
   isLocallyClosed_range := by
-    rw [← Set.preimage_image_eq (Set.range _) g.embedding.inj]
+    rw [← Set.preimage_image_eq (Set.range _) g.isEmbedding.inj]
     have := (f ≫ g).isLocallyClosed_range.preimage g.base.2
     simpa only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp] using this
 

Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean

@@ -30,7 +30,7 @@ lemma isomorphisms_eq_stalkwise :
   congr 1
   ext X Y f
   exact ⟨fun H ↦ inferInstanceAs (IsIso (TopCat.isoOfHomeo
-    (H.1.1.toHomeomeomorph_of_surjective H.2)).hom), fun (_ : IsIso f.base) ↦
+    (H.1.1.toHomeomorph_of_surjective H.2)).hom), fun (_ : IsIso f.base) ↦
     let e := (TopCat.homeoOfIso <| asIso f.base); ⟨e.isOpenEmbedding, e.surjective⟩⟩
 
 instance : IsLocalAtTarget (isomorphisms Scheme) :=

Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

@@ -34,18 +34,21 @@ namespace AlgebraicGeometry
 topological spaces is an embedding and the induced morphisms of stalks are all surjective. -/
 @[mk_iff]
 class IsPreimmersion {X Y : Scheme} (f : X ⟶ Y) : Prop where
-  base_embedding : Embedding f.base
+  base_embedding : IsEmbedding f.base
   surj_on_stalks : ∀ x, Function.Surjective (f.stalkMap x)
 
-lemma Scheme.Hom.embedding {X Y : Scheme} (f : Hom X Y) [IsPreimmersion f] : Embedding f.base :=
+lemma Scheme.Hom.isEmbedding {X Y : Scheme} (f : Hom X Y) [IsPreimmersion f] : IsEmbedding f.base :=
   IsPreimmersion.base_embedding
 
+@[deprecated (since := "2024-10-26")]
+alias Scheme.Hom.embedding := Scheme.Hom.isEmbedding
+
 lemma Scheme.Hom.stalkMap_surjective {X Y : Scheme} (f : Hom X Y) [IsPreimmersion f] (x) :
     Function.Surjective (f.stalkMap x) :=
   IsPreimmersion.surj_on_stalks x
 
 lemma isPreimmersion_eq_inf :
-    @IsPreimmersion = topologically Embedding ⊓ stalkwise (Function.Surjective ·) := by
+    @IsPreimmersion = topologically IsEmbedding ⊓ stalkwise (Function.Surjective ·) := by
   ext
   rw [isPreimmersion_iff]
   rfl
@@ -61,7 +64,7 @@ instance : IsLocalAtTarget @IsPreimmersion :=
   isPreimmersion_eq_inf ▸ inferInstance
 
 instance (priority := 900) {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : IsPreimmersion f where
-  base_embedding := f.isOpenEmbedding.toEmbedding
+  base_embedding := f.isOpenEmbedding.isEmbedding
   surj_on_stalks _ := (ConcreteCategory.bijective_of_isIso _).2
 
 instance : MorphismProperty.IsMultiplicative @IsPreimmersion where
@@ -79,14 +82,14 @@ instance (priority := 900) {X Y} (f : X ⟶ Y) [IsPreimmersion f] : Mono f := by
   refine (Scheme.forgetToLocallyRingedSpace ⋙
     LocallyRingedSpace.forgetToSheafedSpace).mono_of_mono_map ?_
   apply SheafedSpace.mono_of_base_injective_of_stalk_epi
-  · exact f.embedding.inj
+  · exact f.isEmbedding.inj
   · exact fun x ↦ ConcreteCategory.epi_of_surjective _ (f.stalkMap_surjective x)
 
 theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion g]
     [IsPreimmersion (f ≫ g)] : IsPreimmersion f where
   base_embedding := by
-    have h := (f ≫ g).embedding
-    rwa [← g.embedding.of_comp_iff]
+    have h := (f ≫ g).isEmbedding
+    rwa [← g.isEmbedding.of_comp_iff]
   surj_on_stalks x := by
     have h := (f ≫ g).stalkMap_surjective x
     rw [Scheme.stalkMap_comp] at h
@@ -97,7 +100,7 @@ theorem comp_iff {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion g]
   ⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩
 
 lemma Spec_map_iff {R S : CommRingCat.{u}} (f : R ⟶ S) :
-    IsPreimmersion (Spec.map f) ↔ Embedding (PrimeSpectrum.comap f) ∧ f.SurjectiveOnStalks := by
+    IsPreimmersion (Spec.map f) ↔ IsEmbedding (PrimeSpectrum.comap f) ∧ f.SurjectiveOnStalks := by
   haveI : (RingHom.toMorphismProperty <| fun f ↦ Function.Surjective f).RespectsIso := by
     rw [← RingHom.toMorphismProperty_respectsIso_iff]
     exact RingHom.surjective_respectsIso
@@ -111,15 +114,15 @@ lemma Spec_map_iff {R S : CommRingCat.{u}} (f : R ⟶ S) :
     exact h₂ x.asIdeal x.isPrime
 
 lemma mk_Spec_map {R S : CommRingCat.{u}} {f : R ⟶ S}
-    (h₁ : Embedding (PrimeSpectrum.comap f)) (h₂ : f.SurjectiveOnStalks) :
+    (h₁ : IsEmbedding (PrimeSpectrum.comap f)) (h₂ : f.SurjectiveOnStalks) :
     IsPreimmersion (Spec.map f) :=
   (Spec_map_iff f).mpr ⟨h₁, h₂⟩
 
 lemma of_isLocalization {R S : Type u} [CommRing R] (M : Submonoid R) [CommRing S]
     [Algebra R S] [IsLocalization M S] :
     IsPreimmersion (Spec.map (CommRingCat.ofHom <| algebraMap R S)) :=
   IsPreimmersion.mk_Spec_map
-    (PrimeSpectrum.localization_comap_embedding (R := R) S M)
+    (PrimeSpectrum.localization_comap_isEmbedding (R := R) S M)
     (RingHom.surjectiveOnStalks_of_isLocalization (M := M) S)
 
 end IsPreimmersion

Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

@@ -85,7 +85,7 @@ theorem quasiCompact_affineProperty_iff_quasiSeparatedSpace {X Y : Scheme} [IsAf
     let g : pullback U.1.ι V.1.ι ⟶ X := pullback.fst _ _ ≫ U.1.ι
     -- Porting note: `inferInstance` does not work here
     have : IsOpenImmersion g := PresheafedSpace.IsOpenImmersion.comp _ _
-    have e := Homeomorph.ofEmbedding _ this.base_open.toEmbedding
+    have e := Homeomorph.ofIsEmbedding _ this.base_open.isEmbedding
     rw [IsOpenImmersion.range_pullback_to_base_of_left] at e
     erw [Subtype.range_coe, Subtype.range_coe] at e
     rw [isCompact_iff_compactSpace]
@@ -94,7 +94,7 @@ theorem quasiCompact_affineProperty_iff_quasiSeparatedSpace {X Y : Scheme} [IsAf
     let g : pullback f₁ f₂ ⟶ X := pullback.fst _ _ ≫ f₁
     -- Porting note: `inferInstance` does not work here
     have : IsOpenImmersion g := PresheafedSpace.IsOpenImmersion.comp _ _
-    have e := Homeomorph.ofEmbedding _ this.base_open.toEmbedding
+    have e := Homeomorph.ofIsEmbedding _ this.base_open.isEmbedding
     rw [IsOpenImmersion.range_pullback_to_base_of_left] at e
     simp_rw [isCompact_iff_compactSpace] at H
     exact

Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

@@ -17,7 +17,7 @@ of the underlying map of topological spaces, including
 - `Surjective`
 - `IsOpenMap`
 - `IsClosedMap`
-- `Embedding`
+- `IsEmbedding`
 - `IsOpenEmbedding`
 - `IsClosedEmbedding`
 - `DenseRange` (`IsDominant`)
@@ -105,15 +105,15 @@ instance isClosedMap_isLocalAtTarget : IsLocalAtTarget (topologically IsClosedMa
 
 end IsClosedMap
 
-section Embedding
+section IsEmbedding
 
-instance : (topologically Embedding).RespectsIso :=
-  topologically_respectsIso _ (fun e ↦ e.embedding) (fun _ _ hf hg ↦ hg.comp hf)
+instance : (topologically IsEmbedding).RespectsIso :=
+  topologically_respectsIso _ (fun e ↦ e.isEmbedding) (fun _ _ hf hg ↦ hg.comp hf)
 
-instance embedding_isLocalAtTarget : IsLocalAtTarget (topologically Embedding) :=
-  topologically_isLocalAtTarget' _ fun _ _ _ ↦ embedding_iff_embedding_of_iSup_eq_top
+instance isEmbedding_isLocalAtTarget : IsLocalAtTarget (topologically IsEmbedding) :=
+  topologically_isLocalAtTarget' _ fun _ _ _ ↦ isEmbedding_iff_of_iSup_eq_top
 
-end Embedding
+end IsEmbedding
 
 section IsOpenEmbedding
 

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -260,10 +260,13 @@ theorem localization_comap_injective [Algebra R S] (M : Submonoid R) [IsLocaliza
     Function.Injective (comap (algebraMap R S)) :=
   fun _ _ h => localization_specComap_injective S M h
 
-theorem localization_comap_embedding [Algebra R S] (M : Submonoid R) [IsLocalization M S] :
-    Embedding (comap (algebraMap R S)) :=
+theorem localization_comap_isEmbedding [Algebra R S] (M : Submonoid R) [IsLocalization M S] :
+    IsEmbedding (comap (algebraMap R S)) :=
   ⟨localization_comap_inducing S M, localization_comap_injective S M⟩
 
+@[deprecated (since := "2024-10-26")]
+alias localization_comap_embedding := localization_comap_isEmbedding
+
 theorem localization_comap_range [Algebra R S] (M : Submonoid R) [IsLocalization M S] :
     Set.range (comap (algebraMap R S)) = { p | Disjoint (M : Set R) p.asIdeal } :=
   localization_specComap_range ..
@@ -462,11 +465,11 @@ theorem localization_away_comap_range (S : Type v) [CommSemiring S] [Algebra R S
     exact h₁ (x.2.mem_of_pow_mem _ h₃)
 
 theorem localization_away_isOpenEmbedding (S : Type v) [CommSemiring S] [Algebra R S] (r : R)
-    [IsLocalization.Away r S] : IsOpenEmbedding (comap (algebraMap R S)) :=
-  { toEmbedding := localization_comap_embedding S (Submonoid.powers r)
-    isOpen_range := by
-      rw [localization_away_comap_range S r]
-      exact isOpen_basicOpen }
+    [IsLocalization.Away r S] : IsOpenEmbedding (comap (algebraMap R S)) where
+  toIsEmbedding := localization_comap_isEmbedding S (Submonoid.powers r)
+  isOpen_range := by
+    rw [localization_away_comap_range S r]
+    exact isOpen_basicOpen
 
 @[deprecated (since := "2024-10-18")]
 alias localization_away_openEmbedding := localization_away_isOpenEmbedding

Mathlib/AlgebraicGeometry/PrimeSpectrum/TensorProduct.lean

@@ -11,7 +11,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 # Lemmas regarding the prime spectrum of tensor products
 
 ## Main result
-- `PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks`:
+- `PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks`:
   If `R →+* T` is surjective on stalks (see Mathlib/RingTheory/SurjectiveOnStalks.lean),
   then `Spec(S ⊗[R] T) → Spec S × Spec T` is a topological embedding
   (where `Spec S × Spec T` is the cartesian product with the product topology).
@@ -34,7 +34,7 @@ lemma PrimeSpectrum.continuous_tensorProductTo : Continuous (tensorProductTo R S
 variable (hRT : (algebraMap R T).SurjectiveOnStalks)
 include hRT
 
-lemma PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks_aux
+lemma PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux
     (p₁ p₂ : PrimeSpectrum (S ⊗[R] T))
     (h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂) :
     p₁ ≤ p₂ := by
@@ -55,11 +55,11 @@ lemma PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks_aux
     rwa [show p₁.asIdeal.comap (algebraMap S (S ⊗[R] T)) = p₂.asIdeal.comap _ from congr($h.1.1)]
   exact p₁.asIdeal.primeCompl.mul_mem h₄ h₃ h₁
 
-lemma PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks :
-    Embedding (tensorProductTo R S T) := by
+lemma PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks :
+    IsEmbedding (tensorProductTo R S T) := by
   refine ⟨?_, fun p₁ p₂ e ↦
-    (embedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₁ p₂ e).antisymm
-      (embedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₂ p₁ e.symm)⟩
+    (isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₁ p₂ e).antisymm
+      (isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₂ p₁ e.symm)⟩
   let g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
   refine ⟨(continuous_tensorProductTo ..).le_induced.antisymm (isBasis_basic_opens.le_iff.mpr ?_)⟩
   rintro _ ⟨f, rfl⟩
@@ -77,3 +77,7 @@ lemma PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks :
       rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, ← e]
       exact J.asIdeal.primeCompl.mul_mem ht hJ
     rwa [J.isPrime.mul_mem_iff_mem_or_mem.not, not_or] at this
+
+@[deprecated (since := "2024-10-26")]
+alias PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks :=
+  PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks

Mathlib/AlgebraicGeometry/Properties.lean

@@ -31,16 +31,16 @@ variable (X : Scheme)
 
 instance : T0Space X :=
   T0Space.of_open_cover fun x => ⟨_, X.affineCover.covers x,
-    (X.affineCover.map x).opensRange.2, Embedding.t0Space (Y := PrimeSpectrum _)
-    (isAffineOpen_opensRange (X.affineCover.map x)).isoSpec.schemeIsoToHomeo.embedding⟩
+    (X.affineCover.map x).opensRange.2, IsEmbedding.t0Space (Y := PrimeSpectrum _)
+    (isAffineOpen_opensRange (X.affineCover.map x)).isoSpec.schemeIsoToHomeo.isEmbedding⟩
 
 instance : QuasiSober X := by
   apply (config := { allowSynthFailures := true })
     quasiSober_of_open_cover (Set.range fun x => Set.range <| (X.affineCover.map x).base)
   · rintro ⟨_, i, rfl⟩; exact (X.affineCover.IsOpen i).base_open.isOpen_range
   · rintro ⟨_, i, rfl⟩
-    exact @IsOpenEmbedding.quasiSober _ _ _ _ _ (Homeomorph.ofEmbedding _
-      (X.affineCover.IsOpen i).base_open.toEmbedding).symm.isOpenEmbedding PrimeSpectrum.quasiSober
+    exact @IsOpenEmbedding.quasiSober _ _ _ _ _ (Homeomorph.ofIsEmbedding _
+      (X.affineCover.IsOpen i).base_open.isEmbedding).symm.isOpenEmbedding PrimeSpectrum.quasiSober
   · rw [Set.top_eq_univ, Set.sUnion_range, Set.eq_univ_iff_forall]
     intro x; exact ⟨_, ⟨_, rfl⟩, X.affineCover.covers x⟩
 

Mathlib/AlgebraicGeometry/ResidueField.lean

@@ -52,7 +52,8 @@ def residue (X : Scheme.{u}) (x) : X.presheaf.stalk x ⟶ X.residueField x :=
 `Spec.map (X.residue x)` is a closed immersion. -/
 instance {X : Scheme.{u}} (x) : IsPreimmersion (Spec.map (X.residue x)) :=
   IsPreimmersion.mk_Spec_map
-    (PrimeSpectrum.isClosedEmbedding_comap_of_surjective _ _ Ideal.Quotient.mk_surjective).embedding
+    (PrimeSpectrum.isClosedEmbedding_comap_of_surjective _ _
+      Ideal.Quotient.mk_surjective).isEmbedding
     (RingHom.surjectiveOnStalks_of_surjective (Ideal.Quotient.mk_surjective))
 
 @[simp]

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean

@@ -160,9 +160,9 @@ lemma cfc_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S))
     simp [Function.comp, Subtype.val_injective.extend_apply]
   · have : ¬ ContinuousOn (fun x ↦ algebraMap R S (g (f x)) : S → S) (spectrum S a) := by
       refine fun hg' ↦ hg ?_
-      rw [halg.embedding.continuousOn_iff]
-      simpa [halg.embedding.continuousOn_iff, Function.comp_def, h.left_inv _] using
-        hg'.comp halg.embedding.continuous.continuousOn (fun _ : R ↦ spectrum.algebraMap_mem S)
+      rw [halg.isEmbedding.continuousOn_iff]
+      simpa [halg.isEmbedding.continuousOn_iff, Function.comp_def, h.left_inv _] using
+        hg'.comp halg.isEmbedding.continuous.continuousOn (fun _ : R ↦ spectrum.algebraMap_mem S)
     rw [cfc_apply_of_not_continuousOn a hg, cfc_apply_of_not_continuousOn a this]
 
 end SpectrumRestricts
@@ -312,9 +312,9 @@ lemma cfcₙ_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R
     obtain (hg | hg) := hg
     · have : ¬ ContinuousOn (fun x ↦ algebraMap R S (g (f x)) : S → S) (σₙ S a) := by
         refine fun hg' ↦ hg ?_
-        rw [halg.embedding.continuousOn_iff]
-        simpa [halg.embedding.continuousOn_iff, Function.comp_def, h.left_inv _] using
-          hg'.comp halg.embedding.continuous.continuousOn
+        rw [halg.isEmbedding.continuousOn_iff]
+        simpa [halg.isEmbedding.continuousOn_iff, Function.comp_def, h.left_inv _] using
+          hg'.comp halg.isEmbedding.continuous.continuousOn
           (fun _ : R ↦ quasispectrum.algebraMap_mem S)
       rw [cfcₙ_apply_of_not_continuousOn a hg, cfcₙ_apply_of_not_continuousOn a this]
     · rw [cfcₙ_apply_of_not_map_zero a hg, cfcₙ_apply_of_not_map_zero a (by simpa [h.map_zero])]

Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

@@ -333,7 +333,7 @@ theorem HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt
   let F' := UniformSpace.Completion F
   let a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
   let b : (E →L[𝕜] F) →ₗᵢ[𝕜] (E →L[𝕜] F') := UniformSpace.Completion.toComplₗᵢ.postcomp
-  rw [← b.embedding.hasSum_iff]
+  rw [← b.isEmbedding.hasSum_iff]
   have : HasFPowerSeriesWithinOnBall (a ∘ f) (a.compFormalMultilinearSeries p) s x r :=
     a.comp_hasFPowerSeriesWithinOnBall h
   have Z := (this.fderivWithin hu).hasSum h'y (by simpa [edist_eq_coe_nnnorm] using hy)

Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

@@ -36,11 +36,14 @@ theorem isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℍ → ℂ) :=
 @[deprecated (since := "2024-10-18")]
 alias openEmbedding_coe := isOpenEmbedding_coe
 
-theorem embedding_coe : Embedding ((↑) : ℍ → ℂ) :=
-  embedding_subtype_val
+theorem isEmbedding_coe : IsEmbedding ((↑) : ℍ → ℂ) :=
+  IsEmbedding.subtypeVal
+
+@[deprecated (since := "2024-10-26")]
+alias embedding_coe := isEmbedding_coe
 
 theorem continuous_coe : Continuous ((↑) : ℍ → ℂ) :=
-  embedding_coe.continuous
+  isEmbedding_coe.continuous
 
 theorem continuous_re : Continuous re :=
   Complex.continuous_re.comp continuous_coe

Mathlib/Analysis/LocallyConvex/Bounded.lean

@@ -199,7 +199,7 @@ theorem IsVonNBounded.image {σ : 𝕜₁ →+* 𝕜₂} [RingHomSurjective σ]
     (hs : IsVonNBounded 𝕜₁ s) (f : E →SL[σ] F) : IsVonNBounded 𝕜₂ (f '' s) := by
   have σ_iso : Isometry σ := AddMonoidHomClass.isometry_of_norm σ fun x => RingHomIsometric.is_iso
   have : map σ (𝓝 0) = 𝓝 0 := by
-    rw [σ_iso.embedding.map_nhds_eq, σ.surjective.range_eq, nhdsWithin_univ, map_zero]
+    rw [σ_iso.isEmbedding.map_nhds_eq, σ.surjective.range_eq, nhdsWithin_univ, map_zero]
   have hf₀ : Tendsto f (𝓝 0) (𝓝 0) := f.continuous.tendsto' 0 0 (map_zero f)
   simp only [isVonNBounded_iff_tendsto_smallSets_nhds, ← this, tendsto_map'_iff] at hs ⊢
   simpa only [comp_def, image_smul_setₛₗ _ _ σ f] using hf₀.image_smallSets.comp hs

Mathlib/Analysis/Normed/Module/WeakDual.lean

@@ -198,7 +198,7 @@ theorem isClosed_image_coe_of_bounded_of_closed {s : Set (WeakDual 𝕜 E)}
 
 theorem isCompact_of_bounded_of_closed [ProperSpace 𝕜] {s : Set (WeakDual 𝕜 E)}
     (hb : IsBounded (Dual.toWeakDual ⁻¹' s)) (hc : IsClosed s) : IsCompact s :=
-  (Embedding.isCompact_iff DFunLike.coe_injective.embedding_induced).mpr <|
+  DFunLike.coe_injective.isEmbedding_induced.isCompact_iff.mpr <|
     ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image hb <|
       isClosed_image_coe_of_bounded_of_closed hb hc
 

Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

@@ -200,7 +200,10 @@ theorem nnnorm_map (x : E) : ‖f x‖₊ = ‖x‖₊ :=
 protected theorem isometry : Isometry f :=
   AddMonoidHomClass.isometry_of_norm f.toLinearMap (norm_map _)
 
-protected lemma embedding (f : F →ₛₗᵢ[σ₁₂] E₂) : Embedding f := f.isometry.embedding
+lemma isEmbedding (f : F →ₛₗᵢ[σ₁₂] E₂) : IsEmbedding f := f.isometry.isEmbedding
+
+@[deprecated (since := "2024-10-26")]
+alias embedding := isEmbedding
 
 -- Should be `@[simp]` but it doesn't fire due to `lean4#3107`.
 theorem isComplete_image_iff [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) {s : Set E} :