refactor: Make circle a type Circle (#15116)

See https://github.com/leanprover-community/mathlib4/wiki/Tradeoffs-of-concrete-types-defined-as-subobjects for context

Author: YaelDillies

Mathlib/Analysis/Complex/Circle.lean

@@ -38,105 +38,142 @@ open Complex Metric
 
 open ComplexConjugate
 
-/-- The unit circle in `ℂ`, here given the structure of a submonoid of `ℂ`. -/
+/-- The unit circle in `ℂ`, here given the structure of a submonoid of `ℂ`.
+
+Please use `Circle` when referring to the circle as a type. -/
+@[deprecated (since := "2024-07-24")]
 def circle : Submonoid ℂ :=
   Submonoid.unitSphere ℂ
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated (since := "2024-07-24")]
 theorem mem_circle_iff_abs {z : ℂ} : z ∈ circle ↔ abs z = 1 :=
   mem_sphere_zero_iff_norm
 
-theorem circle_def : ↑circle = { z : ℂ | abs z = 1 } :=
-  Set.ext fun _ => mem_circle_iff_abs
-
-@[simp]
-theorem abs_coe_circle (z : circle) : abs z = 1 :=
-  mem_circle_iff_abs.mp z.2
+set_option linter.deprecated false in
+@[deprecated (since := "2024-07-24")]
+theorem mem_circle_iff_normSq {z : ℂ} : z ∈ circle ↔ normSq z = 1 := by
+  simp [Complex.abs, mem_circle_iff_abs]
 
-theorem mem_circle_iff_normSq {z : ℂ} : z ∈ circle ↔ normSq z = 1 := by simp [Complex.abs]
+/-- The unit circle in `ℂ`. -/
+def Circle : Type := Submonoid.unitSphere ℂ
+deriving TopologicalSpace
 
-@[simp]
-theorem normSq_eq_of_mem_circle (z : circle) : normSq z = 1 := by simp [normSq_eq_abs]
+namespace Circle
 
-theorem ne_zero_of_mem_circle (z : circle) : (z : ℂ) ≠ 0 :=
-  ne_zero_of_mem_unit_sphere z
+instance instCoeOut : CoeOut Circle ℂ := subtypeCoe
 
-instance commGroup : CommGroup circle :=
-  Metric.sphere.commGroup
+instance instCommGroup : CommGroup Circle := Metric.sphere.commGroup
+instance instMetricSpace : MetricSpace Circle := Subtype.metricSpace
 
-@[simp]
-theorem coe_inv_circle (z : circle) : ↑z⁻¹ = (z : ℂ)⁻¹ :=
-  rfl
+@[simp] lemma abs_coe (z : Circle) : abs z = 1 := mem_sphere_zero_iff_norm.1 z.2
+@[simp] lemma normSq_coe (z : Circle) : normSq z = 1 := by simp [normSq_eq_abs]
+@[simp] lemma coe_ne_zero (z : Circle) : (z : ℂ) ≠ 0 := ne_zero_of_mem_unit_sphere z
+@[simp, norm_cast] lemma coe_one : ↑(1 : Circle) = (1 : ℂ) := rfl
+@[simp, norm_cast] lemma coe_mul (z w : Circle) : ↑(z * w) = (z : ℂ) * w := rfl
+@[simp, norm_cast] lemma coe_inv (z : Circle) : ↑z⁻¹ = (z : ℂ)⁻¹ := rfl
+lemma coe_inv_eq_conj (z : Circle) : ↑z⁻¹ = conj (z : ℂ) := by
+  rw [coe_inv, inv_def, normSq_coe, inv_one, ofReal_one, mul_one]
 
-theorem coe_inv_circle_eq_conj (z : circle) : ↑z⁻¹ = conj (z : ℂ) := by
-  rw [coe_inv_circle, inv_def, normSq_eq_of_mem_circle, inv_one, ofReal_one, mul_one]
+@[simp, norm_cast] lemma coe_div (z w : Circle) : ↑(z / w) = (z : ℂ) / w := rfl
 
-@[simp]
-theorem coe_div_circle (z w : circle) : ↑(z / w) = (z : ℂ) / w :=
-  circle.subtype.map_div z w
+/-- The coercion `Circle → ℂ` as a monoid homomorphism. -/
+@[simps]
+def coeHom : Circle →* ℂ where
+  toFun := (↑)
+  map_one' := coe_one
+  map_mul' := coe_mul
+
+@[deprecated (since := "2024-07-24")] alias _root_.abs_coe_circle := abs_coe
+@[deprecated (since := "2024-07-24")] alias _root_.normSq_eq_of_mem_circle := normSq_coe
+@[deprecated (since := "2024-07-24")] alias _root_.ne_zero_of_mem_circle := coe_ne_zero
+@[deprecated (since := "2024-07-24")] alias _root_.coe_inv_circle := coe_inv
+@[deprecated (since := "2024-07-24")] alias _root_.coe_inv_circle_eq_conj := coe_inv_eq_conj
+@[deprecated (since := "2024-07-24")] alias _root_.coe_div_circle := coe_div
 
 /-- The elements of the circle embed into the units. -/
-def circle.toUnits : circle →* Units ℂ :=
-  unitSphereToUnits ℂ
-
--- written manually because `@[simps]` was slow and generated the wrong lemma
-@[simp]
-theorem circle.toUnits_apply (z : circle) :
-    circle.toUnits z = Units.mk0 ↑z (ne_zero_of_mem_circle z) :=
-  rfl
-
-instance : CompactSpace circle :=
-  Metric.sphere.compactSpace _ _
+def toUnits : Circle →* Units ℂ := unitSphereToUnits ℂ
 
-instance : TopologicalGroup circle :=
-  Metric.sphere.topologicalGroup
+-- written manually because `@[simps]` generated the wrong lemma
+@[simp] lemma toUnits_apply (z : Circle) : toUnits z = Units.mk0 ↑z z.coe_ne_zero := rfl
 
-instance : UniformGroup circle := by
-  convert topologicalGroup_is_uniform_of_compactSpace circle
+instance : CompactSpace Circle := Metric.sphere.compactSpace _ _
+instance : TopologicalGroup Circle := Metric.sphere.topologicalGroup
+instance instUniformSpace : UniformSpace Circle := instUniformSpaceSubtype
+instance : UniformGroup Circle := by
+  convert topologicalGroup_is_uniform_of_compactSpace Circle
   exact unique_uniformity_of_compact rfl rfl
 
 /-- If `z` is a nonzero complex number, then `conj z / z` belongs to the unit circle. -/
 @[simps]
-def circle.ofConjDivSelf (z : ℂ) (hz : z ≠ 0) : circle :=
-  ⟨conj z / z,
-    mem_circle_iff_abs.2 <| by rw [map_div₀, abs_conj, div_self]; exact Complex.abs.ne_zero hz⟩
+def ofConjDivSelf (z : ℂ) (hz : z ≠ 0) : Circle where
+  val := conj z / z
+  property := mem_sphere_zero_iff_norm.2 <| by
+    rw [norm_div, RCLike.norm_conj, div_self]; exact Complex.abs.ne_zero hz
 
 /-- The map `fun t => exp (t * I)` from `ℝ` to the unit circle in `ℂ`. -/
-def expMapCircle : C(ℝ, circle) where
-  toFun t := ⟨exp (t * I), by simp [exp_mul_I, abs_cos_add_sin_mul_I]⟩
+def exp : C(ℝ, Circle) where
+  toFun t := ⟨(t * I).exp, by simp [Submonoid.unitSphere, exp_mul_I, abs_cos_add_sin_mul_I]⟩
+  continuous_toFun := Continuous.subtype_mk (by fun_prop)
+    (by simp [Submonoid.unitSphere, exp_mul_I, abs_cos_add_sin_mul_I])
 
 @[simp]
-theorem expMapCircle_apply (t : ℝ) : ↑(expMapCircle t) = Complex.exp (t * Complex.I) :=
-  rfl
+theorem exp_apply (t : ℝ) : ↑(exp t) = Complex.exp (t * Complex.I) := rfl
 
 @[simp]
-theorem expMapCircle_zero : expMapCircle 0 = 1 :=
-  Subtype.ext <| by
-    rw [expMapCircle_apply, ofReal_zero, zero_mul, exp_zero, Submonoid.coe_one]
+theorem exp_zero : exp 0 = 1 :=
+  Subtype.ext <| by rw [exp_apply, ofReal_zero, zero_mul, Complex.exp_zero, coe_one]
 
 @[simp]
-theorem expMapCircle_add (x y : ℝ) : expMapCircle (x + y) = expMapCircle x * expMapCircle y :=
+theorem exp_add (x y : ℝ) : exp (x + y) = exp x * exp y :=
   Subtype.ext <| by
-    simp only [expMapCircle_apply, Submonoid.coe_mul, ofReal_add, add_mul, Complex.exp_add]
+    simp only [exp_apply, Submonoid.coe_mul, ofReal_add, add_mul, Complex.exp_add, coe_mul]
 
 /-- The map `fun t => exp (t * I)` from `ℝ` to the unit circle in `ℂ`,
 considered as a homomorphism of groups. -/
 @[simps]
-def expMapCircleHom : ℝ →+ Additive circle where
-  toFun := Additive.ofMul ∘ expMapCircle
-  map_zero' := expMapCircle_zero
-  map_add' := expMapCircle_add
+def expHom : ℝ →+ Additive Circle where
+  toFun := Additive.ofMul ∘ exp
+  map_zero' := exp_zero
+  map_add' := exp_add
 
-@[simp]
-theorem expMapCircle_sub (x y : ℝ) : expMapCircle (x - y) = expMapCircle x / expMapCircle y :=
-  expMapCircleHom.map_sub x y
+@[simp] lemma exp_sub (x y : ℝ) : exp (x - y) = exp x / exp y := expHom.map_sub x y
+@[simp] lemma exp_neg (x : ℝ) : exp (-x) = (exp x)⁻¹ := expHom.map_neg x
 
-@[simp]
-theorem expMapCircle_neg (x : ℝ) : expMapCircle (-x) = (expMapCircle x)⁻¹ :=
-  expMapCircleHom.map_neg x
+variable {α β M : Type*}
+
+instance instSMul [SMul ℂ α] : SMul Circle α := Submonoid.smul _
+
+instance instSMulCommClass_left [SMul ℂ β] [SMul α β] [SMulCommClass ℂ α β] :
+    SMulCommClass Circle α β := Submonoid.smulCommClass_left _
+
+instance instSMulCommClass_right [SMul ℂ β] [SMul α β] [SMulCommClass α ℂ β] :
+    SMulCommClass α Circle β := Submonoid.smulCommClass_right _
+
+instance instIsScalarTower [SMul ℂ α] [SMul ℂ β] [SMul α β] [IsScalarTower ℂ α β] :
+    IsScalarTower Circle α β := Submonoid.isScalarTower _
+
+instance instMulAction [MulAction ℂ α] : MulAction Circle α := Submonoid.mulAction _
+
+instance instDistribMulAction [AddMonoid M] [DistribMulAction ℂ M] :
+    DistribMulAction Circle M := Submonoid.distribMulAction _
+
+lemma smul_def [SMul ℂ α] (z : Circle) (a : α) : z • a = (z : ℂ) • a := rfl
+
+instance instContinuousSMul [TopologicalSpace α] [MulAction ℂ α] [ContinuousSMul ℂ α] :
+    ContinuousSMul Circle α := Submonoid.continuousSMul
 
 @[simp]
-lemma norm_circle_smul {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℂ E]
-    (u : circle) (v : E) :
+protected lemma norm_smul {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℂ E]
+    (u : Circle) (v : E) :
     ‖u • v‖ = ‖v‖ := by
   rw [Submonoid.smul_def, norm_smul, norm_eq_of_mem_sphere, one_mul]
+
+@[deprecated (since := "2024-07-24")] noncomputable alias _root_.expMapCircle := exp
+@[deprecated (since := "2024-07-24")] noncomputable alias _root_.expMapCircle_apply := exp_apply
+@[deprecated (since := "2024-07-24")] noncomputable alias _root_.expMapCircle_zero := exp_zero
+@[deprecated (since := "2024-07-24")] noncomputable alias _root_.expMapCircle_sub := exp_sub
+@[deprecated (since := "2024-07-24")] noncomputable alias _root_.norm_circle_smul :=
+  Circle.norm_smul
+
+end Circle

Mathlib/Analysis/Complex/Isometry.lean

@@ -38,27 +38,27 @@ local notation "|" x "|" => Complex.abs x
 
 /-- An element of the unit circle defines a `LinearIsometryEquiv` from `ℂ` to itself, by
 rotation. -/
-def rotation : circle →* ℂ ≃ₗᵢ[ℝ] ℂ where
+def rotation : Circle →* ℂ ≃ₗᵢ[ℝ] ℂ where
   toFun a :=
     { DistribMulAction.toLinearEquiv ℝ ℂ a with
-      norm_map' := fun x => show |a * x| = |x| by rw [map_mul, abs_coe_circle, one_mul] }
-  map_one' := LinearIsometryEquiv.ext <| one_smul circle
+      norm_map' := fun x => show |a * x| = |x| by rw [map_mul, Circle.abs_coe, one_mul] }
+  map_one' := LinearIsometryEquiv.ext <| by simp
   map_mul' a b := LinearIsometryEquiv.ext <| mul_smul a b
 
 @[simp]
-theorem rotation_apply (a : circle) (z : ℂ) : rotation a z = a * z :=
+theorem rotation_apply (a : Circle) (z : ℂ) : rotation a z = a * z :=
   rfl
 
 @[simp]
-theorem rotation_symm (a : circle) : (rotation a).symm = rotation a⁻¹ :=
+theorem rotation_symm (a : Circle) : (rotation a).symm = rotation a⁻¹ :=
   LinearIsometryEquiv.ext fun _ => rfl
 
 @[simp]
-theorem rotation_trans (a b : circle) : (rotation a).trans (rotation b) = rotation (b * a) := by
+theorem rotation_trans (a b : Circle) : (rotation a).trans (rotation b) = rotation (b * a) := by
   ext1
   simp
 
-theorem rotation_ne_conjLIE (a : circle) : rotation a ≠ conjLIE := by
+theorem rotation_ne_conjLIE (a : Circle) : rotation a ≠ conjLIE := by
   intro h
   have h1 : rotation a 1 = conj 1 := LinearIsometryEquiv.congr_fun h 1
   have hI : rotation a I = conj I := LinearIsometryEquiv.congr_fun h I
@@ -69,11 +69,11 @@ theorem rotation_ne_conjLIE (a : circle) : rotation a ≠ conjLIE := by
 /-- Takes an element of `ℂ ≃ₗᵢ[ℝ] ℂ` and checks if it is a rotation, returns an element of the
 unit circle. -/
 @[simps]
-def rotationOf (e : ℂ ≃ₗᵢ[ℝ] ℂ) : circle :=
-  ⟨e 1 / Complex.abs (e 1), by simp⟩
+def rotationOf (e : ℂ ≃ₗᵢ[ℝ] ℂ) : Circle :=
+  ⟨e 1 / Complex.abs (e 1), by simp [Submonoid.unitSphere, ← Complex.norm_eq_abs]⟩
 
 @[simp]
-theorem rotationOf_rotation (a : circle) : rotationOf (rotation a) = a :=
+theorem rotationOf_rotation (a : Circle) : rotationOf (rotation a) = a :=
   Subtype.ext <| by simp
 
 theorem rotation_injective : Function.Injective rotation :=
@@ -127,8 +127,8 @@ theorem linear_isometry_complex_aux {f : ℂ ≃ₗᵢ[ℝ] ℂ} (h : f 1 = 1) :
       fin_cases i <;> simp [h, h']
 
 theorem linear_isometry_complex (f : ℂ ≃ₗᵢ[ℝ] ℂ) :
-    ∃ a : circle, f = rotation a ∨ f = conjLIE.trans (rotation a) := by
-  let a : circle := ⟨f 1, by rw [mem_circle_iff_abs, ← Complex.norm_eq_abs, f.norm_map, norm_one]⟩
+    ∃ a : Circle, f = rotation a ∨ f = conjLIE.trans (rotation a) := by
+  let a : Circle := ⟨f 1, by simp [Submonoid.unitSphere, ← Complex.norm_eq_abs, f.norm_map]⟩
   use a
   have : (f.trans (rotation a).symm) 1 = 1 := by simpa using rotation_apply a⁻¹ (f 1)
   refine (linear_isometry_complex_aux this).imp (fun h₁ => ?_) fun h₂ => ?_
@@ -137,7 +137,7 @@ theorem linear_isometry_complex (f : ℂ ≃ₗᵢ[ℝ] ℂ) :
 
 /-- The matrix representation of `rotation a` is equal to the conformal matrix
 `!![re a, -im a; im a, re a]`. -/
-theorem toMatrix_rotation (a : circle) :
+theorem toMatrix_rotation (a : Circle) :
     LinearMap.toMatrix basisOneI basisOneI (rotation a).toLinearEquiv =
       Matrix.planeConformalMatrix (re a) (im a) (by simp [pow_two, ← normSq_apply]) := by
   ext i j
@@ -149,11 +149,11 @@ theorem toMatrix_rotation (a : circle) :
 
 /-- The determinant of `rotation` (as a linear map) is equal to `1`. -/
 @[simp]
-theorem det_rotation (a : circle) : LinearMap.det ((rotation a).toLinearEquiv : ℂ →ₗ[ℝ] ℂ) = 1 := by
+theorem det_rotation (a : Circle) : LinearMap.det ((rotation a).toLinearEquiv : ℂ →ₗ[ℝ] ℂ) = 1 := by
   rw [← LinearMap.det_toMatrix basisOneI, toMatrix_rotation, Matrix.det_fin_two]
   simp [← normSq_apply]
 
 /-- The determinant of `rotation` (as a linear equiv) is equal to `1`. -/
 @[simp]
-theorem linearEquiv_det_rotation (a : circle) : LinearEquiv.det (rotation a).toLinearEquiv = 1 := by
+theorem linearEquiv_det_rotation (a : Circle) : LinearEquiv.det (rotation a).toLinearEquiv = 1 := by
   rw [← Units.eq_iff, LinearEquiv.coe_det, det_rotation, Units.val_one]

Mathlib/Analysis/Complex/UnitDisc/Basic.lean

@@ -97,23 +97,23 @@ theorem coe_eq_zero {z : 𝔻} : (z : ℂ) = 0 ↔ z = 0 :=
 instance : Inhabited 𝔻 :=
   ⟨0⟩
 
-instance circleAction : MulAction circle 𝔻 :=
+instance circleAction : MulAction Circle 𝔻 :=
   mulActionSphereBall
 
-instance isScalarTower_circle_circle : IsScalarTower circle circle 𝔻 :=
+instance isScalarTower_circle_circle : IsScalarTower Circle Circle 𝔻 :=
   isScalarTower_sphere_sphere_ball
 
-instance isScalarTower_circle : IsScalarTower circle 𝔻 𝔻 :=
+instance isScalarTower_circle : IsScalarTower Circle 𝔻 𝔻 :=
   isScalarTower_sphere_ball_ball
 
-instance instSMulCommClass_circle : SMulCommClass circle 𝔻 𝔻 :=
+instance instSMulCommClass_circle : SMulCommClass Circle 𝔻 𝔻 :=
   instSMulCommClass_sphere_ball_ball
 
-instance instSMulCommClass_circle' : SMulCommClass 𝔻 circle 𝔻 :=
+instance instSMulCommClass_circle' : SMulCommClass 𝔻 Circle 𝔻 :=
   SMulCommClass.symm _ _ _
 
 @[simp, norm_cast]
-theorem coe_smul_circle (z : circle) (w : 𝔻) : ↑(z • w) = (z * w : ℂ) :=
+theorem coe_smul_circle (z : Circle) (w : 𝔻) : ↑(z • w) = (z * w : ℂ) :=
   rfl
 
 instance closedBallAction : MulAction (closedBall (0 : ℂ) 1) 𝔻 :=
@@ -132,10 +132,10 @@ instance instSMulCommClass_closedBall : SMulCommClass (closedBall (0 : ℂ) 1) 
 instance instSMulCommClass_closedBall' : SMulCommClass 𝔻 (closedBall (0 : ℂ) 1) 𝔻 :=
   SMulCommClass.symm _ _ _
 
-instance instSMulCommClass_circle_closedBall : SMulCommClass circle (closedBall (0 : ℂ) 1) 𝔻 :=
+instance instSMulCommClass_circle_closedBall : SMulCommClass Circle (closedBall (0 : ℂ) 1) 𝔻 :=
   instSMulCommClass_sphere_closedBall_ball
 
-instance instSMulCommClass_closedBall_circle : SMulCommClass (closedBall (0 : ℂ) 1) circle 𝔻 :=
+instance instSMulCommClass_closedBall_circle : SMulCommClass (closedBall (0 : ℂ) 1) Circle 𝔻 :=
   SMulCommClass.symm _ _ _
 
 @[simp, norm_cast]

Mathlib/Analysis/Fourier/AddCircle.lean

@@ -111,7 +111,7 @@ theorem fourier_apply {n : ℤ} {x : AddCircle T} : fourier n x = toCircle (n 
 theorem fourier_coe_apply {n : ℤ} {x : ℝ} :
     fourier n (x : AddCircle T) = Complex.exp (2 * π * Complex.I * n * x / T) := by
   rw [fourier_apply, ← QuotientAddGroup.mk_zsmul, toCircle, Function.Periodic.lift_coe,
-    expMapCircle_apply, Complex.ofReal_mul, Complex.ofReal_div, Complex.ofReal_mul, zsmul_eq_mul,
+    Circle.exp_apply, Complex.ofReal_mul, Complex.ofReal_div, Complex.ofReal_mul, zsmul_eq_mul,
     Complex.ofReal_mul, Complex.ofReal_intCast]
   norm_num
   congr 1; ring
@@ -145,7 +145,7 @@ theorem fourier_neg {n : ℤ} {x : AddCircle T} : fourier (-n) x = conj (fourier
   induction x using QuotientAddGroup.induction_on
   simp_rw [fourier_apply, toCircle]
   rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_zsmul]
-  simp_rw [Function.Periodic.lift_coe, ← coe_inv_circle_eq_conj, ← expMapCircle_neg,
+  simp_rw [Function.Periodic.lift_coe, ← Circle.coe_inv_eq_conj, ← Circle.exp_neg,
     neg_smul, mul_neg]
 
 @[simp]
@@ -154,7 +154,7 @@ theorem fourier_neg' {n : ℤ} {x : AddCircle T} : @toCircle T (-(n • x)) = co
 
 -- @[simp] -- Porting note: simp normal form is `fourier_add'`
 theorem fourier_add {m n : ℤ} {x : AddCircle T} : fourier (m+n) x = fourier m x * fourier n x := by
-  simp_rw [fourier_apply, add_zsmul, toCircle_add, coe_mul_unitSphere]
+  simp_rw [fourier_apply, add_zsmul, toCircle_add, Circle.coe_mul]
 
 @[simp]
 theorem fourier_add' {m n : ℤ} {x : AddCircle T} :
@@ -163,7 +163,7 @@ theorem fourier_add' {m n : ℤ} {x : AddCircle T} :
 
 theorem fourier_norm [Fact (0 < T)] (n : ℤ) : ‖@fourier T n‖ = 1 := by
   rw [ContinuousMap.norm_eq_iSup_norm]
-  have : ∀ x : AddCircle T, ‖fourier n x‖ = 1 := fun x => abs_coe_circle _
+  have : ∀ x : AddCircle T, ‖fourier n x‖ = 1 := fun x => Circle.abs_coe _
   simp_rw [this]
   exact @ciSup_const _ _ _ Zero.instNonempty _
 
@@ -173,7 +173,7 @@ theorem fourier_add_half_inv_index {n : ℤ} (hn : n ≠ 0) (hT : 0 < T) (x : Ad
   rw [fourier_apply, zsmul_add, ← QuotientAddGroup.mk_zsmul, toCircle_add, coe_mul_unitSphere]
   have : (n : ℂ) ≠ 0 := by simpa using hn
   have : (@toCircle T (n • (T / 2 / n) : ℝ) : ℂ) = -1 := by
-    rw [zsmul_eq_mul, toCircle, Function.Periodic.lift_coe, expMapCircle_apply]
+    rw [zsmul_eq_mul, toCircle, Function.Periodic.lift_coe, Circle.exp_apply]
     replace hT := Complex.ofReal_ne_zero.mpr hT.ne'
     convert Complex.exp_pi_mul_I using 3
     field_simp; ring