Zulip Chat Archive

Stream: general

Topic: Projection is a def, should be lemma


view this post on Zulip Johan Commelin (Oct 04 2019 at 18:00):

#sanity_check gave me the following complaint:

/- An subring of a Huber ring is called a “ring of integral elements”
if it is open, integrally closed, and power bounded. See [Wedhorn, Def 7.14].-/
structure is_ring_of_integral_elements (Rplus : Type u) (R : Type u)
  [comm_ring Rplus] [topological_space Rplus] [Huber_ring R] [algebra Rplus R]
  extends is_integrally_closed Rplus R, open_embedding (algebra_map R : Rplus  R) : Prop :=
(is_power_bounded : set.range (algebra_map R : Rplus  R)  R)
/- INCORRECT DEF/LEMMA: -/
#print is_ring_of_integral_elements.to_is_integrally_closed /- is a def, should be a lemma/theorem -/
#print is_ring_of_integral_elements.to_open_embedding /- is a def, should be a lemma/theorem -/

view this post on Zulip Johan Commelin (Oct 04 2019 at 18:01):

@Simon Hudon Is this a known issue?

view this post on Zulip Johan Commelin (Oct 04 2019 at 18:07):

@Sebastian Ullrich Just cc-ing you, in case this isn't known.

view this post on Zulip Simon Hudon (Oct 04 2019 at 18:07):

I was not involved in writing #sanity_check. I don't know what the policy is with regards to projections


Last updated: May 14 2021 at 07:19 UTC