From 83e3075fd4a639b2668280d9fecc7bdbc251d6ee Mon Sep 17 00:00:00 2001 From: Winston Yin Date: Thu, 4 Jan 2024 00:57:28 -0800 Subject: [PATCH 1/5] sphere --- Mathlib/Geometry/Manifold/Instances/Sphere.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/Mathlib/Geometry/Manifold/Instances/Sphere.lean index bb922383d08d1..2f6d9128e5349 100644 --- a/Mathlib/Geometry/Manifold/Instances/Sphere.lean +++ b/Mathlib/Geometry/Manifold/Instances/Sphere.lean @@ -382,7 +382,7 @@ theorem stereographic'_target {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphe /-- The unit sphere in an `n + 1`-dimensional inner product space `E` is a charted space modelled on the Euclidean space of dimension `n`. -/ -instance chartedSpace {n : ℕ} [Fact (finrank ℝ E = n + 1)] : +instance Metric.sphere.instChartedSpace {n : ℕ} [Fact (finrank ℝ E = n + 1)] : ChartedSpace (EuclideanSpace ℝ (Fin n)) (sphere (0 : E) 1) where atlas := {f | ∃ v : sphere (0 : E) 1, f = stereographic' n v} chartAt v := stereographic' n (-v) @@ -411,7 +411,7 @@ theorem stereographic'_symm_apply {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : /-- The unit sphere in an `n + 1`-dimensional inner product space `E` is a smooth manifold, modelled on the Euclidean space of dimension `n`. -/ -instance smoothMfldWithCorners {n : ℕ} [Fact (finrank ℝ E = n + 1)] : +instance Metric.sphere.instSmoothManifoldWithCorners {n : ℕ} [Fact (finrank ℝ E = n + 1)] : SmoothManifoldWithCorners (𝓡 n) (sphere (0 : E) 1) := smoothManifoldWithCorners_of_contDiffOn (𝓡 n) (sphere (0 : E) 1) (by @@ -443,7 +443,7 @@ instance smoothMfldWithCorners {n : ℕ} [Fact (finrank ℝ E = n + 1)] : theorem contMDiff_coe_sphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] : ContMDiff (𝓡 n) 𝓘(ℝ, E) ∞ ((↑) : sphere (0 : E) 1 → E) := by -- Porting note: trouble with filling these implicit variables in the instance - have := smoothMfldWithCorners (E := E) (n := n) + have := Metric.sphere.instSmoothManifoldWithCorners (E := E) (n := n) rw [contMDiff_iff] constructor · exact continuous_subtype_val @@ -589,10 +589,10 @@ attribute [local instance] finrank_real_complex_fact' /-- The unit circle in `ℂ` is a charted space modelled on `EuclideanSpace ℝ (Fin 1)`. This follows by definition from the corresponding result for `Metric.Sphere`. -/ instance : ChartedSpace (EuclideanSpace ℝ (Fin 1)) circle := - chartedSpace + Metric.sphere.instChartedSpace instance : SmoothManifoldWithCorners (𝓡 1) circle := - smoothMfldWithCorners (E := ℂ) + Metric.sphere.instSmoothManifoldWithCorners (E := ℂ) /-- The unit circle in `ℂ` is a Lie group. -/ instance : LieGroup (𝓡 1) circle where From 9475b0ed3840cee5a0f9128a90a3ee73b71cb8d8 Mon Sep 17 00:00:00 2001 From: Winston Yin Date: Thu, 4 Jan 2024 00:59:32 -0800 Subject: [PATCH 2/5] funLike --- Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean b/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean index d9bef5da10fd8..4bc6b10688607 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean @@ -71,7 +71,7 @@ structure MulChar extends MonoidHom R R' where map_nonunit' : ∀ a : R, ¬IsUnit a → toFun a = 0 #align mul_char MulChar -instance funLike : FunLike (MulChar R R') R (fun _ => R') := +instance MulChar.instFunLike : FunLike (MulChar R R') R (fun _ => R') := ⟨fun χ => χ.toFun, fun χ₀ χ₁ h => by cases χ₀; cases χ₁; congr; apply MonoidHom.ext (fun _ => congr_fun h _)⟩ From ff80babc87ef5bda079ec6fb0054d519d98425cb Mon Sep 17 00:00:00 2001 From: Winston Yin Date: Thu, 4 Jan 2024 01:08:38 -0800 Subject: [PATCH 3/5] overview.yaml --- docs/overview.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/overview.yaml b/docs/overview.yaml index d262da1176d36..5996d8d63c403 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -408,7 +408,7 @@ Geometry: tangent bundle: 'TangentBundle' tangent map: 'tangentMap' Lie group: 'LieGroup' - sphere: 'smoothMfldWithCorners' + sphere: 'Metric.sphere.instSmoothManifoldWithCorners' Algebraic geometry: prime spectrum: 'PrimeSpectrum' From 42e30cd8866b7f6ae19d52450815d8bfad8f41d4 Mon Sep 17 00:00:00 2001 From: Winston Yin Date: Thu, 4 Jan 2024 11:21:36 -0800 Subject: [PATCH 4/5] EuclideanSpace.xxxSphere --- Mathlib/Geometry/Manifold/Instances/Sphere.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/Mathlib/Geometry/Manifold/Instances/Sphere.lean index 2f6d9128e5349..c84328c8ea028 100644 --- a/Mathlib/Geometry/Manifold/Instances/Sphere.lean +++ b/Mathlib/Geometry/Manifold/Instances/Sphere.lean @@ -382,7 +382,7 @@ theorem stereographic'_target {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphe /-- The unit sphere in an `n + 1`-dimensional inner product space `E` is a charted space modelled on the Euclidean space of dimension `n`. -/ -instance Metric.sphere.instChartedSpace {n : ℕ} [Fact (finrank ℝ E = n + 1)] : +instance EuclideanSpace.instChartedSpaceSphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] : ChartedSpace (EuclideanSpace ℝ (Fin n)) (sphere (0 : E) 1) where atlas := {f | ∃ v : sphere (0 : E) 1, f = stereographic' n v} chartAt v := stereographic' n (-v) @@ -411,7 +411,7 @@ theorem stereographic'_symm_apply {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : /-- The unit sphere in an `n + 1`-dimensional inner product space `E` is a smooth manifold, modelled on the Euclidean space of dimension `n`. -/ -instance Metric.sphere.instSmoothManifoldWithCorners {n : ℕ} [Fact (finrank ℝ E = n + 1)] : +instance EuclideanSpace.instSmoothManifoldWithCornersSphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] : SmoothManifoldWithCorners (𝓡 n) (sphere (0 : E) 1) := smoothManifoldWithCorners_of_contDiffOn (𝓡 n) (sphere (0 : E) 1) (by @@ -443,7 +443,7 @@ instance Metric.sphere.instSmoothManifoldWithCorners {n : ℕ} [Fact (finrank theorem contMDiff_coe_sphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] : ContMDiff (𝓡 n) 𝓘(ℝ, E) ∞ ((↑) : sphere (0 : E) 1 → E) := by -- Porting note: trouble with filling these implicit variables in the instance - have := Metric.sphere.instSmoothManifoldWithCorners (E := E) (n := n) + have := EuclideanSpace.instSmoothManifoldWithCornersSphere (E := E) (n := n) rw [contMDiff_iff] constructor · exact continuous_subtype_val @@ -589,10 +589,10 @@ attribute [local instance] finrank_real_complex_fact' /-- The unit circle in `ℂ` is a charted space modelled on `EuclideanSpace ℝ (Fin 1)`. This follows by definition from the corresponding result for `Metric.Sphere`. -/ instance : ChartedSpace (EuclideanSpace ℝ (Fin 1)) circle := - Metric.sphere.instChartedSpace + EuclideanSpace.instChartedSpaceSphere instance : SmoothManifoldWithCorners (𝓡 1) circle := - Metric.sphere.instSmoothManifoldWithCorners (E := ℂ) + EuclideanSpace.instSmoothManifoldWithCornersSphere (E := ℂ) /-- The unit circle in `ℂ` is a Lie group. -/ instance : LieGroup (𝓡 1) circle where From 37c3895b2fd58f29c3fcf39f8b062435917892a3 Mon Sep 17 00:00:00 2001 From: Winston Yin Date: Thu, 4 Jan 2024 11:39:10 -0800 Subject: [PATCH 5/5] overview.yaml --- docs/overview.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/overview.yaml b/docs/overview.yaml index 5996d8d63c403..bf6a5b7332969 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -408,7 +408,7 @@ Geometry: tangent bundle: 'TangentBundle' tangent map: 'tangentMap' Lie group: 'LieGroup' - sphere: 'Metric.sphere.instSmoothManifoldWithCorners' + sphere: 'EuclideanSpace.instSmoothManifoldWithCornersSphere' Algebraic geometry: prime spectrum: 'PrimeSpectrum'