Zulip Chat Archive

Stream: maths

Topic: ideal restatement

view this post on Zulip Patrick Massot (Sep 29 2018 at 14:59):

As often, I find myself moving stuff around without doing anything. I just wrote:

lemma image_subset_iff' {α : Type*} {β : Type*} (f : α  β) (s : set α) (t : set β) :
  f '' s  t   a, a  s  f a  t := image_subset_iff

which is only restating f '' s ⊆ t ↔ s ⊆ f ⁻¹' t in a definitionaly equivalent form, in order to allow rewriting in:

class is_ideal' {α : Type u} [comm_ring α] (s : set α) : Prop :=
(zero : (0:α)  s)
(add  : (λ p : α × α, p.1 + p.2) ''  set.prod s s  s)
(mul :  b, (λ s, b*s) '' s  s)

lemma is_ideal_iff {β : Type*} [comm_ring β] (S : set β) :
 is_ideal S  is_ideal' S :=
  split ; intro h ; haveI := h,
  { split,
    { exact is_ideal.zero S },
    { rintros a ⟨⟨x, y, x_in, y_in, sum,
      rw sum,
      exact is_ideal.add x_in y_in },
    { rintros b s a, a_in, prod⟩⟩,
      rw prod,
      exact is_ideal.mul_left a_in } },
  { exact { zero_ := h.zero,
      add_ := λ x y x_in y_in, have xy : x + y  (λ (p : β × β), p.fst + p.snd) '' set.prod S S :=
          mem_image_of_mem (λ p : β × β, p.1 + p.2) (mk_mem_prod x_in y_in),
        is_ideal'.add S xy,
      smul := λ b, by rw image_subset_iff' ; exact is_ideal'.mul S b }}

which is restating the definition of an ideal in a functional way, which is suitable for topological reasoning in:
instance ideal_closure [topological_ring α] (S : set α) [is_ideal S] : is_ideal (closure S). Am I doing this right? Should we have a more systematic way of doing such things, or even a tactic (probably transforming the functional form into a pointwise form)?

view this post on Zulip Patrick Massot (Sep 29 2018 at 15:01):

Maybe I should also add the instance proof in order to show why the functional form is useful:

instance ideal_closure [topological_ring α] (S : set α) [is_ideal S] : is_ideal (closure S) :=
  rcases (is_ideal_iff S).1 (by apply_instance) with zero, add, mul,
  rw is_ideal_iff,
  { exact subset_closure zero },
  { rw closure_prod_eq,
    exact subset.trans (image_closure_subset_closure_image continuous_add') (closure_mono add) },
  { intro b,
    have : continuous (λ s, b*s) := continuous_mul continuous_const continuous_id,
    exact subset.trans (image_closure_subset_closure_image this) (closure_mono (mul b)) },

view this post on Zulip Patrick Massot (Sep 29 2018 at 15:02):

By the way, I have no idea why split is happy to transform the goal is_ideal' S into the expected three goals, but doesn't want to do anything with the goal is_ideal S

Last updated: May 11 2021 at 15:12 UTC