From 3e011d6625316ccd1347928427ce9f3e4c5cd59a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 14 Mar 2021 03:22:12 +0000 Subject: [PATCH] chore(equiv/*): add missing lemmas to traverse coercion diamonds (#6648) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit These don't have a preferred direction, but there are cases when they are definitely needed. The conversion paths commute as squares: ``` `→+` <-- `→+*` <-- `→ₐ[R]` ^ ^ ^ | | | `≃+` <-- `≃+*` <-- `≃ₐ[R]` ``` so we only need lemmas to swap within each square. --- src/algebra/algebra/basic.lean | 4 ++++ src/algebra/module/linear_map.lean | 5 +++++ src/data/equiv/ring.lean | 15 +++++++++++++++ 3 files changed, 24 insertions(+) diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean index 39534d64dd590..ce1b1bbf55551 100644 --- a/src/algebra/algebra/basic.lean +++ b/src/algebra/algebra/basic.lean @@ -723,6 +723,10 @@ instance has_coe_to_alg_hom : has_coe (A₁ ≃ₐ[R] A₂) (A₁ →ₐ[R] A₂ @[simp, norm_cast] lemma coe_alg_hom : ((e : A₁ →ₐ[R] A₂) : A₁ → A₂) = e := rfl +/-- The two paths coercion can take to a `ring_hom` are equivalent -/ +lemma coe_ring_hom_commutes : ((e : A₁ →ₐ[R] A₂) : A₁ →+* A₂) = ((e : A₁ ≃+* A₂) : A₁ →+* A₂) := +rfl + @[simp] lemma map_pow : ∀ (x : A₁) (n : ℕ), e (x ^ n) = (e x) ^ n := e.to_alg_hom.map_pow lemma injective : function.injective e := e.to_equiv.injective diff --git a/src/algebra/module/linear_map.lean b/src/algebra/module/linear_map.lean index ee980b505cbaa..6d8920ced26b2 100644 --- a/src/algebra/module/linear_map.lean +++ b/src/algebra/module/linear_map.lean @@ -446,6 +446,11 @@ def trans : M ≃ₗ[R] M₃ := @[simp] lemma coe_to_add_equiv : ⇑(e.to_add_equiv) = e := rfl +/-- The two paths coercion can take to an `add_monoid_hom` are equivalent -/ +lemma to_add_monoid_hom_commutes : + e.to_linear_map.to_add_monoid_hom = e.to_add_equiv.to_add_monoid_hom := +rfl + @[simp] theorem trans_apply (c : M) : (e₁.trans e₂) c = e₂ (e₁ c) := rfl @[simp] theorem apply_symm_apply (c : M₂) : e (e.symm c) = c := e.6 c diff --git a/src/data/equiv/ring.lean b/src/data/equiv/ring.lean index 0c7ff5896bf9e..a1debe137c044 100644 --- a/src/data/equiv/ring.lean +++ b/src/data/equiv/ring.lean @@ -256,6 +256,21 @@ abbreviation to_monoid_hom (e : R ≃+* S) : R →* S := e.to_ring_hom.to_monoid /-- Reinterpret a ring equivalence as an `add_monoid` homomorphism. -/ abbreviation to_add_monoid_hom (e : R ≃+* S) : R →+ S := e.to_ring_hom.to_add_monoid_hom +/-- The two paths coercion can take to an `add_monoid_hom` are equivalent -/ +lemma to_add_monoid_hom_commutes (f : R ≃+* S) : + (f : R →+* S).to_add_monoid_hom = (f : R ≃+ S).to_add_monoid_hom := +rfl + +/-- The two paths coercion can take to an `monoid_hom` are equivalent -/ +lemma to_monoid_hom_commutes (f : R ≃+* S) : + (f : R →+* S).to_monoid_hom = (f : R ≃* S).to_monoid_hom := +rfl + +/-- The two paths coercion can take to an `equiv` are equivalent -/ +lemma to_equiv_commutes (f : R ≃+* S) : + (f : R ≃+ S).to_equiv = (f : R ≃* S).to_equiv := +rfl + @[simp] lemma to_ring_hom_refl : (ring_equiv.refl R).to_ring_hom = ring_hom.id R := rfl