Subalgebra.equivOpposite

Stream: Is there code for X?

[Jz Pan]

Do we have this (or is it correct):

def Subalgebra.equivOpposite
    {R : Type*} [CommSemiring R] {A : Type*} [Semiring A] [Algebra R A] :
    Subalgebra R Aᵐᵒᵖ ≃o Subalgebra R A :=
  sorry

I think we only have docs#Submodule.equivOpposite, but not the above. Also, I think Submodule.equivOpposite is also an OrderIso, but this is also not in mathlib yet?

[Yaël Dillies]

It seems correct

[Jz Pan]

I started with this code:

variable {R : Type*} [CommSemiring R] {A : Type*} [Semiring A] [Algebra R A]

def _root_.Subalgebra.fromOpposite (S : Subalgebra R Aᵐᵒᵖ) : Subalgebra R A where
  __ := MulOpposite.unop (Submodule.equivOpposite (toSubmodule S))
  mul_mem' ha hb := by
    sorry
  algebraMap_mem' r := by
    sorry

def _root_.Subalgebra.toOpposite (S : Subalgebra R A) : Subalgebra R Aᵐᵒᵖ where
  __ := Submodule.equivOpposite.symm (MulOpposite.op (toSubmodule S))
  mul_mem' ha hb := sorry
  algebraMap_mem' r := sorry

def _root_.Subalgebra.equivOpposite : Subalgebra R Aᵐᵒᵖ ≃o Subalgebra R A :=
  sorry

but it immediately crashes Lean at the by sorry code :man_facepalming:

[Jz Pan]

algebraMap_mem' r := sorry works, but algebraMap_mem' r := by sorry crashes

[Jz Pan]

OK this works:

variable {R : Type*} [CommSemiring R] {A : Type*} [Semiring A] [Algebra R A]

def _root_.Subalgebra.equivOpposite : Subalgebra R Aᵐᵒᵖ ≃o Subalgebra R A where
  toFun S := { MulOpposite.unop (Submodule.equivOpposite (toSubmodule S)) with
    mul_mem' := fun ha hb ↦ S.mul_mem hb ha
    algebraMap_mem' := S.algebraMap_mem }
  invFun S := { Submodule.equivOpposite.symm (MulOpposite.op (toSubmodule S)) with
    mul_mem' := fun ha hb ↦ S.mul_mem hb ha
    algebraMap_mem' := S.algebraMap_mem }
  left_inv _ := rfl
  right_inv _ := rfl
  map_rel_iff' {_} {_} :=
    Submodule.comap_le_comap_iff_of_surjective (MulOpposite.opLinearEquiv R).surjective _ _

I still need to define the map from S to equivOpposite S...

[Eric Wieser]

do we have docs#Subring.equivOpposite

[Eric Wieser]

It might make sense to build all the weaker versions along the way at the same time

[Kevin Buzzard]

I raised the issue of the crash here.

[Eric Wieser]

We have docs#Submonoid.equivOpposite, right?

[Eric Wieser]

Maybe docs#Submonoid.op ?

[Eric Wieser]

Aha, docs#AddSubmonoid.opEquiv

[Eric Wieser]

I guess we need to unify these names too

[Jz Pan]

PR created as #12846.