Rewrite using Ring Isomorphisms

Stream: mathlib4

[Gareth Ma]

Hello, how do I "rewrite" using f here?

import Mathlib.Algebra.RingQuot
import Mathlib.RingTheory.Ideal.IsPrimary
import Mathlib.RingTheory.Ideal.LocalRing

open Polynomial Ideal Quotient LocalRing

example {R S : Type*} [CommRing R] [CommRing S] (f : R ≃+* S) : IsDomain R ↔ IsDomain S := by
  simp

[Riccardo Brasca]

If this is not already in the library (maybe for injective rather than equiv) you can add it, it should be rather easy.

[Gareth Ma]

I realised that IsDomain is actually a mix-in. Should this lemma still be written like this?

[Gareth Ma]

Or should I use typeclasses

[Gareth Ma]

This is failing: for "cannot find synthesization order for instance @instIsDomainToSemiringToCommSemiring with type"

instance {R S : Type*}  [CommRing R] [CommRing S] (f : R ≃+* S) [IsDomain R] : IsDomain S := by
  infer_instance

[Riccardo Brasca]

infer_instance cannot use f, so there is no hope it works automatically. You can prove it by hand (noting that injectivity is enough)

[Riccardo Brasca]

Something like docs#IsPrincipalIdealRing.of_surjective

[Gareth Ma]

I will do it for isomorphism first, then try to use my brain later (x) Thanks!

[Gareth Ma]

I have another question here, if you don't mind to take a look

[Riccardo Brasca]

I am on my phone, the other one needs a computer I am afraid

[Gareth Ma]

What is the syntax for injective ringhom?

[Gareth Ma]

Also I'm pretty sure it doesn't work with just a injective ring homomorphism? $\mathbb{Z} \hookrightarrow \mathbb{Z}[X]/\langle X^2 \rangle$ for example. Sorry for the terrible example...
But I got it for an isomorphism. I'll use that for now :D

[Gareth Ma]

theorem IsDomain.of_equiv {R S : Type*} [CommRing R] [CommRing S] (f : R ≃+* S) [IsDomain R] :
    IsDomain S where
  mul_left_cancel_of_ne_zero := by
    /- Prove that ab=ac -> a=0 or b=c by f^-1 (surjectivity) and R is ID -/
    intro a b c ha h
    apply_fun f.symm at h
    simpa [f.symm.map_mul, ha] using h
  mul_right_cancel_of_ne_zero := by
    intro a b c ha h
    apply_fun f.symm at h
    simpa [f.symm.map_mul, ha] using h
  exists_pair_ne := by
    obtain ⟨x, y, h⟩ := @Nontrivial.exists_pair_ne R _
    use f x, f y, fun h' ↦ h (f.injective h') /- Prove that S is nontrivial using injectivity: |S| >= |R| -/

[Eric Wieser]

You should be able to use docs#Function.Injective.nontrivial for that last field

[Eric Wieser]

And docs#Function.Injective.noZeroDivisors for the other two

[Eric Wieser]

Or just use docs#Function.Injective.isDomain for the whole thing!

[Gareth Ma]

Wait hmm why does my example fail then

[Gareth Ma]

Oops should’ve searched harder, thanks

[Gareth Ma]

No the isDomain is flipped

[Eric Wieser]

Sure, but you have an equiv so you can flip that

[Gareth Ma]

Ah yea with an equiv yes

[Gareth Ma]

It’s very hard to find the instances I need, eg given the equiv f, what dot notations are accessible

[Gareth Ma]

Wish there’s a way like dir(f) in Python to list them

[Eric Wieser]

Auto complete sometimes helps

[Eric Wieser]

@loogle RingEquiv _ _ |- _

[loogle]

:exclamation: <input>:1:14: expected end of input

[Eric Wieser]

Well, without the |- _ that would have worked

[Gareth Ma]

theorem IsDomain.of_equiv {R S : Type*} [CommRing R] [CommRing S] (f : R ≃+* S) [IsDomain R] :
    IsDomain S :=
  f.symm.injective.isDomain f.symm.toRingHom

yay!

[Eric Wieser]

Probably not worth having in mathlib though, since it's just a special case of the more general injective case

[Eric Wieser]

Oh, I guess the iff version is

[Gareth Ma]

Yeah definitely. For iff do you mean IsDomain R iff IsDomain S (given an equiv)?

[Gareth Ma]

Ah well in that case you don't need an equiv either you just need a bijective function

[Gareth Ma]

probably

[Eric Wieser]

All bijective ring homs are equivalences anyway, right?

[Gareth Ma]

Think so, oops
It's just RingEquiv.ofBijective

[Gareth Ma]

my bad

[Kevin Buzzard]

In topology, bijective continuous maps aren't necessarily homeomorphisms, but in algebra this sort of thing is essentially always true.