Zulip Chat Archive

Stream: general

Topic: display of setoid.r


ZHAO Jinxiang (Jun 11 2022 at 08:57):

import group_theory.quotient_group

variables {α β : Type*} (f : α  β)

noncomputable def my_setoid_comap_quotient_equiv (f : α  β) (r : setoid β) :
  quotient (setoid.comap f r)  set.range (@quotient.mk _ r  f) :=
begin
  symmetry,
  apply (setoid.quotient_ker_equiv_range (quotient.mk  f)).symm.trans,
  dunfold setoid.ker function.on_fun function.comp setoid.comap setoid.rel,
  apply quotient.congr_right,
  intros a b,
  convert_to f a = f b  setoid.r (f a) (f b),
  convert_to f a = f b  f a  f b,
  simp,
end

image.png

You can find it shows setoid.r a b ↔ setoid.r a b and I should search the setoid and convert it to ⟦f a⟧ = ⟦f b⟧ ↔ setoid.r (f a) (f b) by hand.

Can we unfold the setoid.r definitions by tactics?

Eric Wieser (Jun 11 2022 at 09:04):

convert_to is a tactic, so I'm not sure of your question

ZHAO Jinxiang (Jun 11 2022 at 09:08):

I want to use dunfold setoid.r, but it fails.
If I need to use convert_to , I should search the context and know which is the setoid.r's definition.
convert_to requires me to query the setoid.r's definition in context every time, which is inconvenient.

Eric Wieser (Jun 11 2022 at 09:10):

setoid.r is a field, there's nothing to unfold

ZHAO Jinxiang (Jun 11 2022 at 09:11):

But setoid.r a b could be simplify.

Eric Wieser (Jun 11 2022 at 09:11):

Your term is probably @setoid.r some_s x y, which means you actually need to unfold some_s

Eric Wieser (Jun 11 2022 at 09:11):

You can hover over the goal in the infoview to find out

Eric Wieser (Jun 11 2022 at 09:12):

Note that ≈ unfolds to setoid.r, not the other way around

Kevin Buzzard (Jun 11 2022 at 09:24):

I've always felt that there was something wrong here. It's hard to get from a goal with in to the actual definition of the equivalence relation, unless you know it already and just do it yourself with change.

ZHAO Jinxiang (Jun 11 2022 at 09:26):

Yes. Every time I want to proof theorem about quotient and setoid, I need to use change tactic a lot.

ZHAO Jinxiang (Jun 11 2022 at 09:27):

Especially setoid.r x y

ZHAO Jinxiang (Jun 11 2022 at 09:31):

import group_theory.quotient_group

variables {α β : Type*} (f : α  β)

def function_to_image (f : α  β):  α  {x // x  set.range f} := λ x , f x, set.mem_range_self x
noncomputable def my_quotient_ker_equiv_range : @quotient α (setoid.ker f)  set.range f :=
begin
  refine equiv.of_bijective (λ k , @quotient.lift _ _ (setoid.ker f) (function_to_image f) (λ a b h , subtype.ext_val h) k)  _,
  split,
  {
    intros x y, simp,
    intro h,
    simp [function_to_image] at h,
    rcases x,
    rcases y,
    simp at h,
    apply quotient.sound,
    unfold has_equiv.equiv,
    -- Why exact h
    exact h,
  },
  {
    rintro y, z, hz⟩,
    simp,
    use @quotient.mk _ (setoid.ker f) z,
    rw quotient.lift_mk,
    rw function_to_image,
    simp,
    exact hz,
  }
end

image.png

I don't know why I can use exact h here, unless I search the definition of setoid.ker. I need some tactic to unfold the definition of setoid.r a d setoid.ker.

Eric Wieser (Jun 11 2022 at 09:37):

dunfold setoid.ker should work

ZHAO Jinxiang (Jun 11 2022 at 09:39):

Thank you. I try dunfold setoid.ker function.on_fun setoid.r, and it works.

Kevin Buzzard (Jun 11 2022 at 09:39):

By the way, here is the same proof as yours, but re-arranged so that it takes far fewer lines:

begin
  refine equiv.of_bijective (λ k , @quotient.lift _ _ (setoid.ker f) (function_to_image f) (λ a b h , subtype.ext_val h) k)  _,
  split,
  {
    rintros x y h,
    apply quotient.sound,
    simpa [function_to_image] using h,
  },
  {
    rintro y, z, hz⟩,
    use @quotient.mk _ (setoid.ker f) z,
    simpa [function_to_image] using hz,
  }
end

Kyle Miller (Jun 11 2022 at 14:11):

Does tactic#unfold_projs help here to unfold setoid.r?

ZHAO Jinxiang (Jun 11 2022 at 15:42):

Kyle Miller said:

Does tactic#unfold_projs help here to unfold setoid.r?

Thank you a lot. That is the static I need.


Last updated: Dec 20 2023 at 11:08 UTC