range of ring morphism ?

Stream: new members

[Nicolás Ojeda Bär]

Hello, suppose that f is a ring morphism, I want to consider the image of f as a ring. With set.range f I get it only as a set. Is this already available somewhere? Thanks!

[Kenny Lau]

it should be a ring already.

[Kenny Lau]

import ring_theory.subring

universes u v

#check λ {α : Type u} {β : Type v} [comm_ring α] [comm_ring β],
  λ (f : α → β) [is_ring_hom f], (by apply_instance : ring (set.range f))

[Kenny Lau]

Output:

λ {α : Type u} {β : Type v} [_inst_1 : comm_ring α] [_inst_2 : comm_ring β] (f : α → β)
[_inst_3 : is_ring_hom f], subset.ring :
  Π {α : Type u} {β : Type v} [_inst_1 : comm_ring α] [_inst_2 : comm_ring β] (f : α → β)
  [_inst_3 : is_ring_hom f], ring ↥(set.range f)

[Kevin Buzzard]

There's a subtlety here. set.range f is a term of type set beta, but not itself a type. The way rings work in Lean is via the typeclass system. In other words, if R is a type then the way to make it a ring is to get a term of type ring R. But ring (set.range f) does not literally make sense. However Lean makes set.range f into a type under the hood, namely a subtype of beta, and then ring (\u set.range f) does make sense (with \u being a little up-arrow to indicate that something subtle just happened) and, as Kenny shows, type class inference then magics up the term of this type automatically.

[Kevin Buzzard]

You are talking about "a set" and "a ring" as if they were the same sort of thing, but in Lean they are not at all the same. There's no such thing as a set, there's only a subset of a type, and stuff like groups and rings etc are all done using type class inference, they are not at all "a set plus some axioms" like in set theory.

[Nicolás Ojeda Bär]

Thanks, this clarifies things a bit.