## Stream: new members

### Topic: range of ring morphism ?

#### Nicolás Ojeda Bär (Oct 13 2019 at 18:10):

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 (Oct 13 2019 at 18:25):

it should be a ring already.

#### Kenny Lau (Oct 13 2019 at 18:42):

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 (Oct 13 2019 at 18:42):

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 (Oct 13 2019 at 19:23):

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 (Oct 13 2019 at 19:25):

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 (Oct 13 2019 at 19:56):

Thanks, this clarifies things a bit.

Last updated: May 14 2021 at 04:22 UTC