Double opposite is the same ring/algebra

Stream: Is there code for X?

[Eric Wieser]

This worked in Lean 3, but the new structure-based MulIOpposite makes it no longer work:

local attribute [semireducible] mul_opposite
example {M} [monoid M] : Mᵐᵒᵖᵐᵒᵖ ≃* M := mul_equiv.refl M
example {R} [ring R] : Rᵐᵒᵖᵐᵒᵖ ≃+* R := ring_equiv.refl R
-- ok, this one didn't work very well
example {R A} [comm_ring R] [ring A] [algebra R A] : Aᵐᵒᵖᵐᵒᵖ ≃ₐ[R] A :=
  by convert @alg_equiv.refl R A _ _ _; ext; refl

[Eric Wieser]

I'm not too upset that these no longer work; but do we have them anywhere in mathlib?

[Eric Wieser]

If we don't already have them, it's not too hard to build the last one as:

@[simps]
def mul_opposite.op_op_alg_equiv : Aᵐᵒᵖᵐᵒᵖ ≃ₐ[R] A :=
alg_equiv.of_linear_equiv
  ((mul_opposite.op_linear_equiv _).trans (mul_opposite.op_linear_equiv _)).symm
  (λ x y, rfl)
  (λ r, rfl)

[Eric Wieser]

A related question is whether we have ℂᵐᵒᵖ ≃ₐ[ℂ] ℂ anywhere; the closest I can find is docs#RingHom.fromOpposite

[Kevin Buzzard]

You mean docs#Complex.conj ? Oh that doesn't exist any more? And docs#starRingEnd is a ring hom, not an algebra equiv?

[Eric Wieser]

Sorry, that question was unclear: I mean id

[Eric Wieser]

Either way, I just ended up writing all these (in lean3, so now I need to wait for mathport to start up)

[Eric Wieser]

#6364 has ℂᵐᵒᵖ ≃ₐ[ℂ] ℂ and some missing AlgHom versions of RingHom helpers.

[Eric Wieser]

The motivation for all this was to build Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₐ[S] (A ⊗[R] B)ᵐᵒᵖ, which in turn I needed to build one of those "conjure a hom then ext" proofs

[Kevin Buzzard]

(oh I'm an idiot -- complex conjugation is not C-linear)

[Eric Wieser]

Eric Wieser said:

#6364 has ℂᵐᵒᵖ ≃ₐ[ℂ] ℂ and some missing AlgHom versions of RingHom helpers.

:ping_pong:; this is unfortunately a bit long, but it's all just expansion of existing boilerplate.

[Eric Wieser]

#6525 contains the titular result of this thread, along with some other helpers I needed for Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₐ[S] (A ⊗[R] B)ᵐᵒᵖ. (#6555)