Updating some proofs to new mathlib

Stream: new members

[Sebastian Monnet]

I tried to PR the following four lemmas, but mathlib has changed and they no longer work. Could someone help me fix the broken ones?

def ring_equiv.subsemiring_equiv_map {A B : Type*} [non_assoc_semiring A]
  [non_assoc_semiring B] (e : A ≃+* B) (R : subsemiring A) :
  R ≃+* R.map e.to_ring_hom :=
{ ..e.to_add_equiv.add_submonoid_equiv_map R.to_add_submonoid,
  ..e.to_mul_equiv.submonoid_equiv_map R.to_submonoid }

def ring_equiv.subring_equiv_map {A B : Type*} [ring A]
  [ring B] (e : A ≃+* B) (R : subring A) :
  R ≃+* R.map e.to_ring_hom :=
e.subsemiring_equiv_map R.to_subsemiring

def alg_equiv.subalgebra_equiv_map {R A B : Type*} [comm_semiring R] [semiring A]
  [semiring B] [algebra R A] [algebra R B] (e : A ≃ₐ[R] B) (S : subalgebra R A) :
  S ≃ₐ[R] (S.map e.to_alg_hom) :=
{ commutes' := λ r, by { ext, simp },
  ..e.to_ring_equiv.subsemiring_equiv_map S.to_subsemiring }

def alg_equiv.intermediate_field_equiv_map {K L M : Type*} [field K] [field L] [field M]
  [algebra K L] [algebra K M] (e : L ≃ₐ[K] M) (E : intermediate_field K L) :
  E ≃ₐ[K] (E.map e.to_alg_hom) :=
e.subalgebra_equiv_map E.to_subalgebra

The first and third one don't work anymore, and I haven't been able to find a fix

[Kevin Buzzard]

Can you make a #mwe ?

[Sebastian Monnet]

Ah sorry, my bad

[Sebastian Monnet]

Will do in a few minutes

[Sebastian Monnet]

Here it is:

import field_theory.galois

def ring_equiv.subsemiring_equiv_map {A B : Type*} [non_assoc_semiring A]
  [non_assoc_semiring B] (e : A ≃+* B) (R : subsemiring A) :
  R ≃+* R.map e.to_ring_hom :=
{ ..e.to_add_equiv.add_submonoid_equiv_map R.to_add_submonoid,
  ..e.to_mul_equiv.submonoid_equiv_map R.to_submonoid }

def ring_equiv.subring_equiv_map {A B : Type*} [ring A]
  [ring B] (e : A ≃+* B) (R : subring A) :
  R ≃+* R.map e.to_ring_hom :=
e.subsemiring_equiv_map R.to_subsemiring

def alg_equiv.subalgebra_equiv_map {R A B : Type*} [comm_semiring R] [semiring A]
  [semiring B] [algebra R A] [algebra R B] (e : A ≃ₐ[R] B) (S : subalgebra R A) :
  S ≃ₐ[R] (S.map e.to_alg_hom) :=
{ commutes' := λ r, by { ext, simp },
  ..e.to_ring_equiv.subsemiring_equiv_map S.to_subsemiring }

def alg_equiv.intermediate_field_equiv_map {K L M : Type*} [field K] [field L] [field M]
  [algebra K L] [algebra K M] (e : L ≃ₐ[K] M) (E : intermediate_field K L) :
  E ≃ₐ[K] (E.map e.to_alg_hom) :=
e.subalgebra_equiv_map E.to_subalgebra

[Eric Wieser]

I already told you how to fix this in the PR review :) - just replace *_equiv_map with *_map everywhere

[Sebastian Monnet]

Eric Wieser said:

I already told you how to fix this in the PR review :) - just replace *_equiv_map with *_map everywhere

Ohh thank you! Sorry, I missed that comment on the PR