From 22c765ddf98425aca49893e6edb618bb96b6d56b Mon Sep 17 00:00:00 2001 From: Matthew Jasper Date: Thu, 26 Mar 2026 19:58:43 +0000 Subject: [PATCH] chore: fix diamonds for Real/Complex Algebra instances --- Mathlib/Algebra/Algebra/Defs.lean | 4 +++- Mathlib/Algebra/Algebra/Pi.lean | 3 ++- Mathlib/Algebra/Algebra/Prod.lean | 3 ++- Mathlib/Analysis/Complex/Basic.lean | 1 - Mathlib/Data/Complex/Basic.lean | 3 ++- Mathlib/LinearAlgebra/Complex/Module.lean | 20 ++++++++++++-------- MathlibTest/instance_diamonds.lean | 9 +++------ 7 files changed, 24 insertions(+), 19 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Defs.lean b/Mathlib/Algebra/Algebra/Defs.lean index c634c2cd56393a..c21ccc7b63f0b2 100644 --- a/Mathlib/Algebra/Algebra/Defs.lean +++ b/Mathlib/Algebra/Algebra/Defs.lean @@ -104,6 +104,7 @@ class Algebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends SM end Prio /-- Embedding `R →+* A` given by `Algebra` structure. -/ +@[implicit_reducible] def algebraMap (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* A := Algebra.algebraMap @@ -350,7 +351,8 @@ This is the algebra version of `Module.compHom`. -/ abbrev compHom : Algebra S A where __ := Module.compHom A f - algebraMap := (algebraMap R A).comp f + algebraMap.__ := (algebraMap R A).comp f + algebraMap.toFun x := algebraMap R A (f x) commutes' _ _ := Algebra.commutes _ _ smul_def' _ _ := Algebra.smul_def _ _ diff --git a/Mathlib/Algebra/Algebra/Pi.lean b/Mathlib/Algebra/Algebra/Pi.lean index 02bfeb667e759f..e49888744ed8a2 100644 --- a/Mathlib/Algebra/Algebra/Pi.lean +++ b/Mathlib/Algebra/Algebra/Pi.lean @@ -36,7 +36,8 @@ variable (A : ι → Type*) variable [CommSemiring R] [∀ i, Semiring (A i)] [∀ i, Algebra R (A i)] instance algebra : Algebra R (Π i, A i) where - algebraMap := Pi.ringHom fun i ↦ algebraMap R (A i) + algebraMap.__ := Pi.ringHom fun i ↦ algebraMap R (A i) + algebraMap.toFun x i := algebraMap R (A i) x commutes' := fun a f ↦ by ext; simp [Algebra.commutes] smul_def' := fun a f ↦ by ext; simp [Algebra.smul_def] diff --git a/Mathlib/Algebra/Algebra/Prod.lean b/Mathlib/Algebra/Algebra/Prod.lean index 46058dff5af82d..5159051562dc69 100644 --- a/Mathlib/Algebra/Algebra/Prod.lean +++ b/Mathlib/Algebra/Algebra/Prod.lean @@ -37,7 +37,8 @@ variable (R A B) open Algebra instance algebra : Algebra R (A × B) where - algebraMap := RingHom.prod (algebraMap R A) (algebraMap R B) + algebraMap.__ := RingHom.prod (algebraMap R A) (algebraMap R B) + algebraMap.toFun x := (algebraMap R A x, algebraMap R B x) commutes' := by rintro r ⟨a, b⟩ dsimp diff --git a/Mathlib/Analysis/Complex/Basic.lean b/Mathlib/Analysis/Complex/Basic.lean index abfa35259a5a81..e3436e96bc7467 100644 --- a/Mathlib/Analysis/Complex/Basic.lean +++ b/Mathlib/Analysis/Complex/Basic.lean @@ -64,7 +64,6 @@ instance : DenselyNormedField ℂ where let ⟨x, h⟩ := exists_between hr ⟨x, by rwa [norm_real, Real.norm_of_nonneg (h₀.trans_lt h.1).le]⟩ -set_option backward.isDefEq.respectTransparency false in instance {R : Type*} [NormedField R] [NormedAlgebra R ℝ] : NormedAlgebra R ℂ where norm_smul_le r x := by rw [← algebraMap_smul ℝ r x, real_smul, norm_mul, norm_real, norm_algebraMap'] diff --git a/Mathlib/Data/Complex/Basic.lean b/Mathlib/Data/Complex/Basic.lean index b2c31426eaaa36..c0abfd24945690 100644 --- a/Mathlib/Data/Complex/Basic.lean +++ b/Mathlib/Data/Complex/Basic.lean @@ -77,7 +77,7 @@ theorem range_im : range im = univ := im_surjective.range_eq /-- The natural inclusion of the real numbers into the complex numbers. -/ -@[coe] +@[coe, implicit_reducible] def ofReal (r : ℝ) : ℂ := ⟨r, 0⟩ instance : Coe ℝ ℂ := @@ -561,6 +561,7 @@ theorem add_conj (z : ℂ) : z + conj z = (2 * z.re : ℝ) := Complex.ext_iff.2 <| by simp [two_mul, ofReal] /-- The coercion `ℝ → ℂ` as a `RingHom`. -/ +@[implicit_reducible] def ofRealHom : ℝ →+* ℂ where toFun x := (x : ℂ) map_one' := ofReal_one diff --git a/Mathlib/LinearAlgebra/Complex/Module.lean b/Mathlib/LinearAlgebra/Complex/Module.lean index 849e35dcd943e8..5e2eb95b39f2f9 100644 --- a/Mathlib/LinearAlgebra/Complex/Module.lean +++ b/Mathlib/LinearAlgebra/Complex/Module.lean @@ -98,7 +98,8 @@ instance (priority := 100) instModule [Semiring R] [Module R ℝ] : Module R ℂ -- priority manually adjusted in https://github.com/leanprover-community/mathlib4/pull/11980 instance (priority := 95) instAlgebraOfReal [CommSemiring R] [Algebra R ℝ] : Algebra R ℂ where - algebraMap := Complex.ofRealHom.comp (algebraMap R ℝ) + algebraMap.__ := Complex.ofRealHom.comp (algebraMap R ℝ) + algebraMap.toFun x := algebraMap R ℝ x smul_def' := fun r x => by ext <;> simp [smul_re, smul_im, Algebra.smul_def] commutes' := fun r ⟨xr, xi⟩ => by ext <;> simp [Algebra.commutes] @@ -166,15 +167,18 @@ instance (priority := 900) Algebra.complexToReal {A : Type*} [Semiring A] [Algeb Algebra ℝ A := .restrictScalars ℝ ℂ A --- try to make sure we're not introducing diamonds but we will need --- `reducible_and_instances` which currently fails https://github.com/leanprover-community/mathlib4/issues/10906 -example : Prod.algebra ℝ ℂ ℂ = (Prod.algebra ℂ ℂ ℂ).complexToReal := rfl +-- make sure that there's no semireducible steps in the definition of the algebraMap +example (x : ℝ) : (algebraMap ℝ ℂ x).re = x := by + with_reducible_and_instances exact rfl --- try to make sure we're not introducing diamonds but we will need --- `reducible_and_instances` which currently fails https://github.com/leanprover-community/mathlib4/issues/10906 +-- try to make sure we're not introducing diamonds +example : Prod.algebra ℝ ℂ ℂ = (Prod.algebra ℂ ℂ ℂ).complexToReal := by + with_reducible_and_instances rfl + +-- try to make sure we're not introducing diamonds example {ι : Type*} [Fintype ι] : - Pi.algebra (R := ℝ) ι (fun _ ↦ ℂ) = (Pi.algebra (R := ℂ) ι (fun _ ↦ ℂ)).complexToReal := - rfl + Pi.algebra (R := ℝ) ι (fun _ ↦ ℂ) = (Pi.algebra (R := ℂ) ι (fun _ ↦ ℂ)).complexToReal := by + with_reducible_and_instances rfl example {A : Type*} [Ring A] [inst : Algebra ℂ A] : (inst.complexToReal).toModule = (inst.toModule).complexToReal := by diff --git a/MathlibTest/instance_diamonds.lean b/MathlibTest/instance_diamonds.lean index 51da1545491e5d..ba1027180434ae 100644 --- a/MathlibTest/instance_diamonds.lean +++ b/MathlibTest/instance_diamonds.lean @@ -27,13 +27,11 @@ open scoped Polynomial example : (SubNegMonoid.toZSMul : SMul ℤ ℂ) = (Complex.SMul.instSMulRealComplex : SMul ℤ ℂ) := by with_reducible_and_instances rfl -set_option backward.isDefEq.respectTransparency false in example : Module.restrictScalars ℝ ℂ ℂ = Complex.instModule := by with_reducible_and_instances rfl --- fails `with_reducible_and_instances` https://github.com/leanprover-community/mathlib4/issues/10906 example : Algebra.restrictScalars ℝ ℂ ℂ = Complex.instAlgebraOfReal := by - rfl + with_reducible_and_instances rfl example (α β : Type _) [AddMonoid α] [AddMonoid β] : (Prod.instSMul : SMul ℕ (α × β)) = AddMonoid.toNSMul := by @@ -57,7 +55,6 @@ open scoped TensorProduct open Complex -set_option backward.isDefEq.respectTransparency false in /- `TensorProduct.Algebra.module` forms a diamond with `instSMulOfMul` and `algebra.tensor_product.tensor_product.semiring`. Given a commutative semiring `A` over a commutative semiring `R`, we get two mathematically different scalar actions of `A ⊗[R] A` on @@ -259,9 +256,9 @@ that at least some potential diamonds are avoided. -/ section complexToReal --- fails `with_reducible_and_instances` https://github.com/leanprover-community/mathlib4/issues/10906 -- the two ways to get `Algebra ℝ ℂ` are definitionally equal -example : (Algebra.id ℂ).complexToReal = Complex.instAlgebraOfReal := rfl +example : (Algebra.id ℂ).complexToReal = Complex.instAlgebraOfReal := by + with_reducible_and_instances rfl -- fails `with_reducible_and_instances` https://github.com/leanprover-community/mathlib4/issues/10906 /- The complexification of an `ℝ`-algebra `A` (i.e., `ℂ ⊗[ℝ] A`) is a `ℂ`-algebra. Viewing this