show that isomorphism between rings is an equivalence relati

Stream: general

[ZHAO Jinxiang]

I don't know how to define isomorphism between rings is an equivalence relation in lean

RingEquiv support two Type* parameters

structure RingEquiv (R S : Type*) [Mul R] [Mul S] [Add R] [Add S] extends R ≃ S, R ≃* S, R ≃+ S

Equivalence support only one Sort u parameter

structure Equivalence {α : Sort u} (r : α → α → Prop) : Prop

So it will not type check to use both of them.

Is there anyone who know how to define this?

[Christian Merten]

The α in docs#Equivalence is the domain of the relation r. You should think about what (informally) the domain of your relation is. This might lead you to a definition like this:

We need the type of all rings of a fixed universe u:

universe u

structure RingType where
  carrier : Type u
  ring : Ring carrier

If you want, you can use the pre-existing docs#RingCat from mathlib.

Then you can define a predicate IsIsomorphic : α → α → Prop where α is the domain of your relation.

Full example

import Mathlib.Algebra.Ring.Equiv

universe u

structure RingType where
  carrier : Type u
  ring : Ring carrier

attribute [instance] RingType.ring

def IsIsomorphic (R S : RingType) : Prop :=
  Nonempty (R.carrier ≃+* S.carrier)

lemma equivalence_isIsomorphic : Equivalence IsIsomorphic := sorry

[ZHAO Jinxiang]

@Christian Merten Thank you very much. It helps me a lot.

[ZHAO Jinxiang]

import Mathlib.Algebra.Category.Ring.Basic
import Mathlib.CategoryTheory.IsomorphismClasses

/-- show that isomorphism between rings is an equivalence relation -/
lemma equivalence_isIsomorphic : Equivalence (@CategoryTheory.IsIsomorphic RingCat _) :=
{
  refl := by
    intro X
    constructor
    exact {
      hom := by
        -- we need add hom here, can I add `id` ring hom here?
        show X ⟶ X
        sorry
      inv := by sorry
      hom_inv_id := by
        sorry
      inv_hom_id := by
        sorry
    }
  symm := by
    intro X Y
    sorry
  trans := by
    intro X Y Z
    sorry
}

What should I provide If there need provide quiver X ⟶ X? I want to provide id function here.

[Eric Wieser]

Note that with a little help, exact? can solve all of these:

lemma equivalence_isIsomorphic : Equivalence (@CategoryTheory.IsIsomorphic RingCat _) where
  refl X := by
    constructor
    exact?
  symm e := by
    cases e
    constructor
    exact?
  trans e f := by
    cases e
    cases f
    constructor
    exact?

[ZHAO Jinxiang]

If I use exact? in show X ⟶ X, it will be exact CategoryTheory.CategoryStruct.id X

But I want to find a function which can convert RingHomId to quiver X ⟶ X

[Eric Wieser]

exact CategoryTheory.CategoryStruct.id X sounds right to me

[Eric Wieser]

I think the function you're looking for is docs#RingCat.ofHom, but it's not the right tool to use here

[ZHAO Jinxiang]

Thank you.

exact RingCat.ofHom (RingHom.id X)

This works well for me.

[Eric Wieser]

Here's the proof you really want:

lemma equivalence_isIsomorphic : Equivalence (@CategoryTheory.IsIsomorphic RingCat _) :=
  (CategoryTheory.isIsomorphicSetoid _).iseqv

(docs#CategoryTheory.isIsomorphicSetoid)

[ZHAO Jinxiang]

Thanks. I finished this

import Mathlib.Algebra.Category.Ring.Basic
import Mathlib.CategoryTheory.IsomorphismClasses

/-- show that isomorphism between rings is an equivalence relation -/
lemma equivalence_isIsomorphic : Equivalence (@CategoryTheory.IsIsomorphic RingCat _) :=
{
  refl := fun X => ⟨{
    hom := RingCat.ofHom (RingHom.id X)
    inv := RingCat.ofHom (RingHom.id X)
    hom_inv_id := rfl
    inv_hom_id := rfl
  }⟩
  symm := fun ⟨ϕ, ϕ', hom_inv_id, inv_hom_id⟩ => ⟨{
    hom := ϕ'
    inv := ϕ
    hom_inv_id := inv_hom_id
    inv_hom_id := hom_inv_id
  }⟩
  trans := fun {X Y Z} ⟨ϕ, ϕ', hom_inv_id_ϕ, inv_hom_id_ϕ⟩ ⟨ψ, ψ', hom_inv_id_ψ, inv_hom_id_ψ⟩ => by
    -- we have hypotheses ϕ, ϕ', ψ, ψ' such that ϕ' ∘ ϕ = id X, ϕ ∘ ϕ' = id Y, ψ' ∘ ψ = id Y, ψ ∘ ψ' = id Z
    replace hom_inv_id_ψ: ψ'.comp ψ = RingHom.id Y := hom_inv_id_ψ;
    replace inv_hom_id_ϕ: ϕ.comp ϕ' = RingHom.id Y := inv_hom_id_ϕ;
    replace hom_inv_id_ϕ: ϕ'.comp ϕ = RingHom.id X := hom_inv_id_ϕ;
    replace inv_hom_id_ψ: ψ.comp ψ' = RingHom.id Z := inv_hom_id_ψ;
    exact ⟨{
      hom := RingCat.ofHom (ψ.comp ϕ)
      inv := RingCat.ofHom (ϕ'.comp ψ')
      hom_inv_id := by
        -- we need prove that ((ϕ'.comp ψ').comp ψ).comp ϕ = RingHom.id X
        show ((ϕ'.comp ψ').comp ψ).comp ϕ = RingHom.id X
        -- by comp assoc
        show (ϕ'.comp (ψ'.comp ψ)).comp ϕ = RingHom.id X
        -- using ψ' ∘ ψ = id Y
        rw [hom_inv_id_ψ]
        show (ϕ'.comp (RingHom.id Y)).comp ϕ = RingHom.id X
        simp;
        -- using ϕ' ∘ ϕ = id X
        exact hom_inv_id_ϕ
      inv_hom_id := by
        -- we need prove that ((ψ.comp ϕ).comp ϕ').comp ψ' = RingHom.id Z
        show ((ψ.comp ϕ).comp ϕ').comp ψ' = RingHom.id Z
        -- by comp assoc
        show (ψ.comp (ϕ.comp ϕ')).comp ψ' = RingHom.id Z
        -- using ϕ ∘ ϕ' = id Y
        rw [inv_hom_id_ϕ]
        show (ψ.comp (RingHom.id Y)).comp ψ' = RingHom.id Z
        simp;
        -- using ψ ∘ ψ' = id Z
        exact inv_hom_id_ψ
    }⟩
}

[ZHAO Jinxiang]

The operator " ∘ " stands for Function.comp.
Is there any operator stands for RingHom.comp?

[Edward van de Meent]

unfortunately, no

[Edward van de Meent]

a small experiment in making a (limited) notation class for ∘ :

import Mathlib

universe u1 u2 u3 v1 v2 v3 ul ur u
set_option autoImplicit false

class HComp {hl : Type u1 → Type v1} {hm : Type u2 → Type v2} {hr : Type u3 → Type v3}
    (F₁ : (L:Type u1) → (M: Type u2) → (hl L) → (hm M) → Type ul)
    [∀ L:Type u1, ∀ instL:hl L, ∀ M: Type u2, ∀ instM: hm M, FunLike (F₁ L M instL instM) L M]
    (F₂ : (M:Type u2) → (R: Type u3) → (hm M) → (hr R) → Type (ur))
    [∀ M:Type u2, ∀ instM:hm M, ∀ R: Type u3, ∀ instR: hr R, FunLike (F₂ M R instM instR) M R]
    (F₃ : outParam ((L : Type u1) → (R : Type u3) → (hl L) → (hr R) → Type u))
    [∀ L:Type u1, ∀ instL:hl L, ∀ R: Type u3, ∀ instR: hr R, FunLike (F₃ L R instL instR) L R]
    where
  private hcomp' : ∀ {L:Type u1}, ∀ {instL:hl L}, ∀ {M: Type u2}, ∀ {instM: hm M},∀ {R: Type u3}, ∀ {instR: hr R},
    F₂ M R instM instR → F₁ L M instL instM → F₃ L R instL instR

section
variable {hl : Type u1 → Type v1} {hm : Type u2 → Type v2} {hr : Type u3 → Type v3}
    {F₁ : (L:Type u1) → (M: Type u2) → (hl L) → (hm M) → Type ul}
    [∀ L:Type u1, ∀ instL:hl L, ∀ M: Type u2, ∀ instM: hm M, FunLike (F₁ L M instL instM) L M]
    {F₂ : (M:Type u2) → (R: Type u3) → (hm M) → (hr R) → Type (ur)}
    [∀ M:Type u2, ∀ instM:hm M, ∀ R: Type u3, ∀ instR: hr R, FunLike (F₂ M R instM instR) M R]
    {F₃ : outParam ((L : Type u1) → (R : Type u3) → (hl L) → (hr R) → Type u)}
    [∀ L:Type u1, ∀ instL:hl L, ∀ R: Type u3, ∀ instR: hr R, FunLike (F₃ L R instL instR) L R]
    [HComp F₁ F₂ F₃]
    {L : Type u1} {M : Type u2} {R : Type u3} {instL : hl L} {instM : hm M} {instR : hr R}
    (f : F₂ M R instM instR) (g : F₁ L M instL instM)
def HComp.hcomp : F₃ L R instL instR := HComp.hcomp' f g
end

instance : HComp (RingHom) (RingHom) (RingHom) where
  hcomp' φ₁ φ₂ := φ₁.comp φ₂

local infix:49 "h∘" => HComp.hcomp

variable {R₁ R₂ R₃: Type*} [Ring R₁] [Ring R₂] [Ring R₃] (σ₁ : R₂ →+* R₃) (σ₂ : R₁ →+* R₂)

#check σ₁ h∘ σ₂

[Edward van de Meent]

it is "possible" to make the notation work for RingHom.comp, AddHom.comp, etc. but only up to a point, as this only works when the FunLike type you're writing an instance for has the exact right amount of arguments in the right order. so no notation for LinearMap.comp.

[Edward van de Meent]

also, i imagine that rewriting all the api (particularly simp lemmas) to use this will not be worth it.

[Edward van de Meent]

note that the F1 F2 F3 approach is required to enable universe polymorphism.

[Jireh Loreaux]

Actually, we do have notation for composition of linear maps, it's \circ\_l, but indeed we do not have any unified notation.

[Eric Wieser]

Perhaps worth remembering that the code above is using category theory, and the category theory library _does_ have a unified notation, as long as you stick with the Quiver.Homs and don't try to unfold to RingHom

[ZHAO Jinxiang]

Also I have a question that Is there anything like show for hypotheses?

I want to write something like

show hom_inv_id_ψ: ψ'.comp ψ = RingHom.id Y

I could not find it so I wrote a weird code replace hom_inv_id_ψ: ψ'.comp ψ = RingHom.id Y := hom_inv_id_ψ;

[Ruben Van de Velde]

change ... at h, but all of those are a sign of missing API

[Christian Merten]

This is because you are on an old version of mathlib. On current master, we have API for this, e.g.

import Mathlib.Algebra.Category.Ring.Basic

open CategoryTheory

example {R S : RingCat} (f : R ⟶ S) (g : S ⟶ R) (h : f ≫ g = 𝟙 R) :
    g.hom.comp f.hom = RingHom.id R := by
  rwa [RingCat.hom_ext_iff, RingCat.hom_comp, RingCat.hom_id] at h