RingHomClass

Stream: mathlib4

[Kenny Lau]

Should Localization.localRingHom take a RingHomClass?

[Aaron Liu]

no

[Aaron Liu]

and Ideal.comap should not take a RingHomClass

[Aaron Liu]

it should take a plain RingHom

[Kenny Lau]

but you could comap a RingEquiv

[Aaron Liu]

and then you need a lemma docs#Ideal.comap_coe

[Aaron Liu]

and you need to use it backwards sometimes often

[Kenny Lau]

but you would need to coerce it a lof of times

[Aaron Liu]

I can't seem to find the corresponding lemma for docs#Ideal.map

[Kenny Lau]

Ideal.map_coe

[Aaron Liu]

and we have stuff like docs#Ideal.map_comap_of_equiv

[Aaron Liu]

it's stated for the coe on the one side and not coe on the other side

[Aaron Liu]

it's probably better to be consistent and have it all coe all the time

[Kenny Lau]

I see we haven't picked a simpNF too

[Aaron Liu]

Kenny Lau said:

Ideal.map_coe

that's stated for a RingHomClass what if I don't have a RingHomClass

[Kenny Lau]

I don't understand

[Aaron Liu]

import Mathlib

example {R : Type*} [Semiring R] (I : Ideal Nat) :
    I.map (Nat.castAddMonoidHom R) = I.map (Nat.castRingHom R) := by
  -- is there a better way
  rfl

[Kenny Lau]

oh, I didn't know Ideal.map takes FunLike...

[Kenny Lau]

perhaps it should only take RingHomClass?

[Aaron Liu]

@Yaël Dillies back me up here

[Andrew Yang]

The rule of thumb is that definitions shouldn't take *HomClass. We don't want ker f and ker f.toRingHom to be different things.

[Kenny Lau]

by that do you include Prop?

[Kenny Lau]

such as RingHom.Finite (which currently takes RingHom)

[Andrew Yang]

For example docs#IsLocalHom is bad, as IsLocalHom f and IsLocalHom f.toRingHom isn't even defeq.

[Kenny Lau]

what should it take then?

[Aaron Liu]

a plain function?

[Aaron Liu]

what's the weakest context this is interesting in?

[Aaron Liu]

maybe a monoid hom?

[Kenny Lau]

I thought functions are bad

[Kenny Lau]

yeah, but it's "intended" to be used with ring homs

[Andrew Yang]

Probably a plain function in this case. See #24965

[Kenny Lau]

I thought functions are difficult to unify

[Aaron Liu]

what does that mean?

[Aaron Liu]

are you talking about higher order unification?

[Kenny Lau]

I'm talking about how we moved away from IsRingHom f

[Aaron Liu]

oh that's for when you're applying them in lemmas

[Aaron Liu]

are there lemmas that work for IsLocalHom f even if f is a plain function?

[Kenny Lau]

isUnit_of_map_unit, basically the one in its definition

[Aaron Liu]

so only one

[Kenny Lau]

isUnit_map_iff

[Aaron Liu]

then that one lemma might have trouble unifying

[Kenny Lau]

Irreducible.of_map

[Aaron Liu]

Kenny Lau said:

isUnit_map_iff

MonoidHomClass not plain function

[Aaron Liu]

Kenny Lau said:

Irreducible.of_map

(same as above) MonoidHomClass

[Aaron Liu]

I'm starting to think it should take a MonoidHom

[Kenny Lau]

but do they not suffer from the same problem?

[Kenny Lau]

I still think it should take RingHom

[Kenny Lau]

at the cost of some lemmas not being in the "maximum generality"

[Aaron Liu]

Kenny Lau said:

but do they not suffer from the same problem?

well it's a MonoidHomClass therefore not a plain function, so no, it doesn't have the same problem

[Aaron Liu]

the problem only applies to plain functions given as fun x => ...

[Kenny Lau]

Aaron Liu said:

Kenny Lau said:

but do they not suffer from the same problem?

well it's a MonoidHomClass therefore not a plain function, so no, it doesn't have the same problem

if you use Irreducible.of_map and you try to prove x is irreducible, then you apply this lemma, then Lean has to solve Irreducible (?f x)

[Aaron Liu]

no, Lean has to solve Irreducible (DFunLike.coe ?f x)

[Kenny Lau]

aha! ok that makes sense

[Kenny Lau]

AlgEquiv.ofBijective takes A₁ →ₐ[R] A₂ while RingEquiv.ofBijective takes NonUnitalRingHomClass F R S; which one is correct?

[Aaron Liu]

AlgEquiv.ofBijective is correct

[Aaron Liu]

since you're making data

[Kenny Lau]

but I would say that this is a case where you don't need to be concerned about equality / lemma since for this case you probably just want the equiv? as in you just use this as auxiliary

[Kenny Lau]

I would argue that the non-API results that show up in the search above are actually wrong

[Kenny Lau]

.ofBijective is not meant to be any simp NF

[Aaron Liu]

Kenny Lau said:

but I would say that this is a case where you don't need to be concerned about equality / lemma since for this case you probably just want the equiv? as in you just use this as auxiliary

what do you mean by this?

[Kenny Lau]

it is not simp NF, so it does not matter that you have two ways of writing like .ofBijective f vs. .ofBijective \u f

[Kenny Lau]

its use is to construct new equivs, and then those new equivs are the simpNFs

[Aaron Liu]

you still run into the problem of .ofBijective f ⋯ and .ofBijective f.toRingHom ⋯ being different

[Kenny Lau]

that is fine, because neither is simpNF

[Aaron Liu]

but you will still sometimes have to convert between them

[Kenny Lau]

lemme put more pseudocode to make my point clearer:

def foo : AlgHom := ...
def fooEquiv1 : RingEquiv := .ofBijective foo
def fooEquiv2 : RingEquiv := .ofBijective (\u foo)

in this code, fooEquiv1 and fooEquiv2 might not be defeq (i suspect they could be), but that's fine because the simpNF of fooEquiv[12] x is actually foo x

[Aaron Liu]

I don't see the lemma that lets me do this

[Kenny Lau]

and I argue that this is the only intended use case of .ofBijective

[Aaron Liu]

I have an example for you too

[Aaron Liu]

I guess making it take just a NonUnitalRingHom doesn't really solve this problem but

def foo : RingHom := ...
def fooAlgHom : AlgHom := { foo with ... }
@[simp] toRingHom_fooAlgHom := ...

def fooRingEquiv : RingEquiv := .ofBijective fooAlgHom <| ...
theorem foo_bar : Bar foo := by
  ...
  -- goal is something complicated containing `fooAlgHom (fooRingEquiv.symm x)`
  simp [fooRingEquiv]
  -- goal now contains `foo ((RingEquiv.ofBijective fooAlgHom ...).symm x)`
  -- which doesn't simplify

[Kenny Lau]

you've done something wrong as soon as you see ofBijective in the goal

[Aaron Liu]

what's wrong with unfolding your definitions while you prove theorems about them

[Kenny Lau]

why would you need to unfold fooRingEquiv?

1. "I need to use the fact that it's a ring equiv": it's a ring equiv already
2. "I need to simplify its application": that's given by foo x

[Aaron Liu]

Kenny Lau said:

2. "I need to simplify its application": that's given by foo x

I don't understand what you mean?

[Kenny Lau]

the simpNF of fooRingEquiv x is foo x, and any property you need can be derived there

[Aaron Liu]

it's symm

[Kenny Lau]

fooRingEquiv.symm x is the simpNF, you gain nothing by unfolding it into ofBijective, because you can't write down its inverse anyway

[Aaron Liu]

I guess with the ofBijective constructors they would reduce to Equiv.ofBijective

[Aaron Liu]

Kenny Lau said:

fooRingEquiv.symm x is the simpNF, you gain nothing by unfolding it into ofBijective, because you can't write down its inverse anyway

want to cancel it with a foo

[Aaron Liu]

I guess this example is a bit contrived

[Kenny Lau]

we need the API that it cancels with foo then...

[Aaron Liu]

but the idea is there

[Kenny Lau]

which again goes back to the hom_lemmas proposal

[Kenny Lau]

Kenny Lau said:

we need the API that it cancels with foo then...

and if you want to apply functions to it, that's another proposal that has been discussed (similar to reassoc)

[Kenny Lau]

ofBijective is never part of the (end result of the) API

[Aaron Liu]

I don't want to come up with another more complicated example that addresses all your points

[Aaron Liu]

what's the benefit you're getting from making it take a FunLike?

[Kenny Lau]

hmm, good point

[Kenny Lau]

yeah there's no need to take anything in a higher hierarchy because at that point you would just use a higher ofBijective

[Kenny Lau]

so, we need to fix:

• RingHom.ker
• Ideal.map
• Ideal.comap
• RingEquiv.ofHomInv
• Ideal.mapHom
• Ideal.orderEmbeddingOfSurjective
• Ideal.relIsoOfBijective
• Ideal.giMapComap
• Ideal.relIsoOfSurjective
• DirectLimit.Ring.of ?
• DirectLimit.Ring.lift ?
• RatFunc.mapRingHom

[Aaron Liu]

is this only the RingHoms?

[Aaron Liu]

for example, I don't see LinearMap.ker on here

[Kenny Lau]

it's not all, i only did RingHomClass

[Kenny Lau]

https://loogle.lean-lang.org/?q=RingHom.codRestrict

RingHom.codRestrict :clipboard: Mathlib.Algebra.Ring.Subsemiring.Basic
{R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] {σS : Type u_2} [SetLike σS S] [SubsemiringClass σS S] (f : R →+* S) (s : σS) (h : ∀ (x : R), f x ∈ s) : R →+* ↥s

Should this take Subsemiring instead of class?

[Kenny Lau]

Also, should we consider this a consensus that with definitions we prefer e.g. RingHom over e.g. RingHomClass? And then we can reference this consensus in future PR's?

[Jireh Loreaux]

@Kenny Lau and @Aaron Liu : I at some point promised this to you: #mathlib4 > Mathlib's morphism hierarchy