cumbersome typeclass in theorem statement

Stream: new members

[Daan van Gent]

I am trying to prove a lemma of the following form.

import order.cover
import ring_theory.simple_module

variables {α : Type*} [lattice α] {x y : α}

open set

lemma covby_iff_simple_order_Icc : x ⋖ y ↔ ∃ hxy : x ≤ y, by {
  letI := Icc.bounded_order hxy, exact is_simple_order (Icc x y) } :=
begin
  rw covby_iff_lt_and_eq_or_eq,
  split;
  rintro ⟨hxy,h⟩, {
    use hxy.le,
    let x' : Icc x y := ⟨x, ⟨le_refl x, hxy.le⟩⟩,
    let y' : Icc x y := ⟨y, ⟨hxy.le, le_refl y⟩⟩,
    letI := Icc.bounded_order hxy.le,
    have hx' : x' = ⊥ := refl x',
    have hy' : y' = ⊤ := refl y',
    haveI : nontrivial (Icc x y) := ⟨⟨⊥, ⊤, λ i, hxy.ne (subtype.mk_eq_mk.mp i)⟩⟩,
    exact ⟨λ ⟨z,hz⟩, begin
      apply (h z hz.1 hz.2).cases_on,
      exact λ h, or.inl begin rw [←hx', subtype.mk_eq_mk, h] end,
      exact λ h, or.inr begin rw [←hy', subtype.mk_eq_mk, h] end,
      end ⟩,
  }, {
    dsimp at h,
    letI := h,
    letI := Icc.bounded_order hxy,
    let x' : Icc x y := ⟨x, ⟨le_refl x, hxy⟩⟩,
    let y' : Icc x y := ⟨y, ⟨hxy, le_refl y⟩⟩,
    have hx' : x' = ⊥ := refl x',
    have hy' : y' = ⊤ := refl y',
    split, {
      apply lt_of_le_of_ne hxy,
      intro hxy,
      have i : x' ≠ y' := bot_ne_top,
      apply i,
      rw [subtype.mk_eq_mk, hxy],
    }, {
      intros z hxz hzy,
      cases eq_bot_or_eq_top (⟨z,⟨hxz,hzy⟩⟩ : Icc x y) with h h, {
        left,
        exact subtype.mk.inj h,
      }, {
        right,
        exact subtype.mk.inj h,
      }
    }
  }
end

Besides the usual question of whether this is already in mathlib (#print instances is_simple_order gives no results), I wonder how to properly deal with the typeclasses in the theorem statement. It feels incorrect to go into tactics mode like this. Similarly, in the proof I need to construct the same typeclass instance. It forces me to duplicate the x' and hx' statements. Could you give me some style hints.

[Alex J. Best]

#print instances will only check the current environment, so unless you have import all (using leanproject mk-all) you won't find all of them.
Fortunately there is an easier way to find all instances: on the website: docs#is_simple_order you can click the arrow to show "instances of this typeclass"

[Daan van Gent]

It seems I was lucky, and my #print instances returned the same list as the docs. The question remains what the pythonic leanic way is to state this lemma.

[Johan Commelin]

One way to improve the statement would be if we refactor is_simple_order α to mean nat.card α = 2.

[Jireh Loreaux]

My short answer is: "don't". The reason it's a bit weird is that bounded_order is a data-carrying class (the data are ⊤ ⊥ : Icc x y), whereas x ⋖ y is a Prop. This is the reason you must have an existential.

But if you must you can make the statement without tactic mode by providing the terms directly.

lemma covby_iff_simple_order_Icc' : x ⋖ y ↔ ∃ hxy : x ≤ y,
  @is_simple_order (Icc x y) _ (Icc.bounded_order hxy) :=
sorry

However, I would instead suggest creating the following instance and lemma:

instance Icc.is_simple_order (h : x ⋖ y) :
  @is_simple_order (Icc x y) _ (Icc.bounded_order h.le) :=
sorry

lemma covby_of_Icc_is_simple_order [bounded_order (Icc x y)] [is_simple_order (Icc x y)] : x ⋖ y :=
sorry

[Johan Commelin]

Lemmas about simple orders can still assume that bounded_order is present, but the defn wouldn't need it.

[Yaël Dillies]

I know the context for this and my answer is: don't

[Yaël Dillies]

The blueprint I gave you carefully dodges trap statements like this one

[Johan Commelin]

@Yaël Dillies Nevertheless, what do you think of making is_simple_order a synonym for nat.card X = 2?

[Eric Wieser]

It seems a bit weird to use is_simple_order as the name if we define it without reference to orders

[Yaël Dillies]

@Johan Commelin, that's wrong. For example, bool with the discrete order (tt and ff are incomparable) is not a simple order.

[Yaël Dillies]

To be fair, the docstring of docs#is_simple_order is misleading.

[Johan Commelin]

I don't know much about order theory...

[Adam Topaz]

Using the word "simple" seems strange to me in this case.

[Yaël Dillies]

Technically, the current definition is wrong too...

[Yaël Dillies]

According to its definition, we could have a preorder where both ⊥ and ⊤ are less than each other (indistinguishable).

[Adam Topaz]

Does this notion agree with nlab#simple+object ?

[Yaël Dillies]

I would need to think it through. I think the correct interpretation for it would be in docs#Lattice

[Adam Topaz]

I guess if you have a simple object X then its lattice of quotients will be "simple" with this definition. But I don't know if that means the lattice itself is simple!

[Adam Topaz]

I'm confused.

[Yaël Dillies]

Hello confused, I'm confused too!

[Junyan Xu]

docs#is_simple_module unfolds to is_simple_order. docs#is_simple_group is definitionally the same as is_simple_order (subgroup G) except for the is_normal condition. I guess it could be defined to be is_simple_order {H : subgroup G // H.is_normal}.

[Adam Topaz]

yeah exactly.

[Eric Wieser]

According to its definition, we could have a preorder where both ⊥ and ⊤ are less than each other (indistinguishable).

Your comment amounts to

[preorder T] [bounded_order T] [is_simple_order T] is meaningless, only [partial_order T] [bounded_order T] [is_simple_order T] has mathematical content

right? I don't think redefining is_simple_order in terms of nat.card changes that

[Pedro Sánchez Terraf]

Adam Topaz said:

Does this notion agree with nlab#simple+object ?

I have not checked what the appropriate morphisms are. But in general (aka "universal") algebra, we treat categories that usually do not have a zero object, and still we call simple those objects with exactly two "congruences" (which is essentially, two quotients).

[Adam Topaz]

Yeah that's essentially what I was saying above. The congruences form a lattice (w.r.t. implication, say), and the lattice of congruences of a simple object is the a simple lattice w.r.t. docs#is_simple_order

[Daan van Gent]

Yaël Dillies said:

The blueprint I gave you carefully dodges trap statements like this one

You are right about what context I am using it, but it is actually for something else. I prove for modules that x ⋖ y iff the quotient is a simple module. However, I think that statement should go (1) x ⋖ y iff Icc x y is simple for lattices and then (2) Icc x y is order isomorphic to the quotient in the case of modules.

[Daan van Gent]

Yaël Dillies said:

Johan Commelin, that's wrong. For example, bool with the discrete order (tt and ff are incomparable) is not a simple order.

Isn't it? My bad I missed the discrete part.

[Daan van Gent]

Junyan Xu said:

docs#is_simple_module unfolds to is_simple_order. docs#is_simple_group is definitionally the same as is_simple_order (subgroup G) except for the is_normal condition. I guess it could be defined to be is_simple_order {H : subgroup G // H.is_normal}.

Working with the 'lattice of normal subgroups' feels unnatural, mostly because Icc x y is not order isomorphic with y / x.

[Daan van Gent]

At the risk of throwing oil at the fire: Is this better? I am also trying to improve my Lean. I have managed to eliminate code duplication.

lemma covby_iff_simple_order_Icc' : x ⋖ y ↔ ∃ hxy : x ≤ y,
  @is_simple_order (Icc x y) _ (Icc.bounded_order hxy) :=
begin
  rw covby_iff_lt_and_eq_or_eq,
  split,
  work_on_goal 1 { rintro ⟨hxy', h⟩, have hxy := hxy'.le },
  work_on_goal 2 { rintro ⟨hxy, h⟩ },
  all_goals
  { letI := Icc.bounded_order hxy,
    have hx : (⊥ : Icc x y) = ⟨x, ⟨le_refl x, hxy⟩⟩ := refl _,
    have hy : (⊤ : Icc x y) = ⟨y, ⟨hxy, le_refl y⟩⟩ := refl _ },
  { use hxy,
    haveI : nontrivial (Icc x y) := ⟨⟨⊥, ⊤, λ i, hxy'.ne (subtype.mk_eq_mk.mp i)⟩⟩,
    exact ⟨λ ⟨z,hz⟩, begin
      apply (h z hz.1 hz.2).cases_on,
      exact λ h, or.inl (by rw [hx,subtype.mk_eq_mk, h]),
      exact λ h, or.inr (by rw [hy, subtype.mk_eq_mk, h]),
      end⟩ },
  { split,
    { apply lt_of_le_of_ne hxy,
      intro hxy,
      apply @bot_ne_top (Icc x y),
      rw [hx, hy, subtype.mk_eq_mk, hxy] },
    { intros z hxz hzy,
      cases eq_bot_or_eq_top (⟨z, ⟨hxz, hzy⟩⟩ : Icc x y) with h h,
      exact or.inl (subtype.mk.inj h),
      exact or.inr (subtype.mk.inj h) } }
end

[Eric Wieser]

Yael's comment above still applies; that lemma permits a more pleasant statement if you state the two directions separately (as this eliminates the exists). You can of course still prove the iff, but you can do so in terms of the separate directions.

[Eric Wieser]

Wrong thread @Yaël Dillies? (fixed)

[Yaël Dillies]

Uh yes :face_palm:

[Daan van Gent]

Eric Wieser said:

Yael's comment above still applies; that lemma permits a more pleasant statement if you state the two directions separately (as this eliminates the exists). You can of course still prove the iff, but you can do so in terms of the separate directions.

Fair point, I will do that.

[Daan van Gent]

Should a lemma like

def Icc_equiv_quot {R : Type*} [ring R] {M : Type*} [add_comm_group M] [module R M] {A B : submodule R M}
  (h : A ≤ B) : (set.Icc A B) ≃o submodule R (B ⧸ comap B.subtype A) := sorry

be added to mathlib? Does it exist? Or does anyone have a better idea for proving that A ⋖ B iff B/A is a simple module?

[Daan van Gent]

At least this one wasn't hard

import order.jordan_holder
import order.cover
import ring_theory.simple_module

open set
open submodule

@[simp]
lemma comap_map_subtype {R M : Type*} [ring R] [add_comm_group M] [module R M] (B : submodule R M)
(A : submodule R B) : comap B.subtype (map B.subtype A) = A :=
comap_map_eq_of_injective subtype.coe_injective A

@[simp]
lemma map_comap_subtype' {R M : Type*} [ring R] [add_comm_group M] [module R M] {B A : submodule R M}
(hab : A ≤ B) : map B.subtype (comap B.subtype A) = A := by {
  rw [map_comap_subtype, inf_eq_right], exact hab }

def Iic_equiv_submodule (R M : Type*) [ring R] [add_comm_group M] [module R M]
  (C : submodule R M) : Iic C ≃o submodule R C := {
  to_fun       := λ ⟨A, hA⟩, comap C.subtype A,
  inv_fun      := λ A, ⟨map C.subtype A, map_subtype_le C A⟩,
  left_inv     := λ ⟨A, hA⟩, subtype.mk_eq_mk.mpr (map_comap_subtype' hA),
  right_inv    := λ A, comap_map_subtype C A,
  map_rel_iff' := begin
    rintros ⟨A, hA⟩ ⟨B, hB⟩,
    change comap C.subtype A ≤ comap C.subtype B ↔ A ≤ B,
    split; intro h,
    { rw [←map_comap_subtype' hA, ←map_comap_subtype' hB],
      exact map_mono h },
    { exact comap_mono h }
  end }

[Eric Wieser]

It would be better to avoid the ⟨⟩ when defining to_fun

[Kevin Buzzard]

Because when defining data this trick can lead to some pretty nasty defeqs under the hood

[Eric Wieser]

I guess the statement above is also true as (C : set X) : Iic C ≃o set C

[Daan van Gent]

So I am trying to prove the Icc version, and I run into some very verbose goals in left_inv, right_inv and map_rel_iff'. Trying to change or dsimp them is very slow, to the point that it gives a deterministic timeout. Any suggestions?

import order.jordan_holder
import order.cover
import ring_theory.simple_module

open set
open submodule
open subtype

@[simp]
lemma comap_map_subtype {R M : Type*} [ring R] [add_comm_group M] [module R M] (B : submodule R M)
(A : submodule R B) : comap B.subtype (map B.subtype A) = A :=
comap_map_eq_of_injective subtype.coe_injective A

@[simp]
lemma map_comap_subtype' {R M : Type*} [ring R] [add_comm_group M] [module R M] {A B : submodule R M}
  (hab : A ≤ B) : map B.subtype (comap B.subtype A) = A := by
{ rw [map_comap_subtype, inf_eq_right], exact hab }

@[simp]
lemma comap_map_mkq' {R M : Type*} [ring R] [add_comm_group M] [module R M] {A B : submodule R M}
  (hab : A ≤ B) : comap A.mkq (map A.mkq B) = B := by
{ rw [comap_map_mkq, sup_eq_right], exact hab }

@[simp]
lemma map_comap_mkq {R M : Type*} [ring R] [add_comm_group M] [module R M] (A : submodule R M)
  (B : submodule R (M ⧸ A)) : map A.mkq (comap A.mkq B) = B :=
map_comap_eq_of_surjective A.mkq_surjective B

def Icc_equiv_quot (R M : Type*) [ring R] [add_comm_group M] [module R M] (A B : submodule R M)
  (hAB : A ≤ B) : (set.Icc A B) ≃o submodule R (B ⧸ comap B.subtype A) := {
  to_fun := λ C, map (comap B.subtype A).mkq (comap B.subtype C.val),
  inv_fun := λ C, ⟨map B.subtype (comap (comap B.subtype A).mkq C), ⟨
    le_trans (map_comap_subtype' hAB).symm.le (map_mono (le_comap_mkq _ C)),
    map_subtype_le B _ ⟩⟩,
  left_inv := λ ⟨C, h⟩, by rw [mk_eq_mk, comap_map_mkq' (comap_mono h.1), map_comap_subtype' h.2],
  right_inv := λ C, begin
    change map (comap B.subtype A).mkq (comap B.subtype (map B.subtype (comap (comap B.subtype A).mkq C))) = C,
    rw [comap_map_subtype, map_comap_mkq],
  end,
  map_rel_iff' := λ C D, begin
    split; intro h, {
      change map (comap B.subtype A).mkq (comap B.subtype C.val) ≤ map (comap B.subtype A).mkq (comap B.subtype D.val) at h,
    }
  end }

[Daan van Gent]

Eric Wieser said:

I guess the statement above is also true as (C : set X) : Iic C ≃o set C

My statement does not follow from that one right? Certainly a submodule C is a set X, but set C is not equal to submodule R C. Or am I missing your point?

[Kevin Buzzard]

dsimp at h, does the change and it seems to do it much more quickly. Wait -- why are you changing C to C.val?

[Kevin Buzzard]

If you do dsimp at h first then the change might work more quickly?

[Kevin Buzzard]

lemma comap_map_mkq' {R M : Type*} [ring R] [add_comm_group M] [module R M] {A B : submodule R M}
  (hab : A ≤ B) : comap A.mkq (map A.mkq B) = B := by rwa [comap_map_mkq, sup_eq_right]

rwa is rw, then assumption

[Kevin Buzzard]

  map_rel_iff' := begin
    rintro ⟨C, hAC, hCB⟩ ⟨D, hAD, hDB⟩,
    dsimp,
    simp only [map_le_iff_le_comap, comap_map_mkq],
    rw sup_eq_right.2 (comap_mono hAD : comap B.subtype A ≤ comap B.subtype D),
    refine ⟨λ h x hxC, _, comap_mono⟩,
    specialize h (_ : B.subtype ⟨x, hCB hxC⟩ ∈ C),
    exacts [hxC, h],
  end

[Kevin Buzzard]

left_inv := λ ⟨C, hAC, hCB⟩, by simp *,

[Kevin Buzzard]

Probably yours is faster though. Note that your h is defeq to A <= C \and C \le B.

[Kevin Buzzard]

Oh -- I changed your to_fun to to_fun := λ C, map (comap B.subtype A).mkq (comap B.subtype (C : submodule R M)), -- my guess is that the coercion is the simp normal form rather than C.val.

[Kevin Buzzard]

To avoid confusion let me just post my version of the full code. It's still slow though and I don't really know why.

def Icc_equiv_quot (R M : Type*) [ring R] [add_comm_group M] [module R M] (A B : submodule R M)
  (hAB : A ≤ B) : (set.Icc A B) ≃o submodule R (B ⧸ comap B.subtype A) := {
  to_fun := λ C, map (comap B.subtype A).mkq (comap B.subtype (C : submodule R M)),
  inv_fun := λ C, ⟨map B.subtype (comap (comap B.subtype A).mkq C), ⟨
    le_trans (map_comap_subtype' hAB).symm.le (map_mono (le_comap_mkq _ C)),
    map_subtype_le B _ ⟩⟩,
  left_inv := λ ⟨C, hAC, hCB⟩, by simp *,
  right_inv := λ C, by simp,
  map_rel_iff' := begin
    rintro ⟨C, hAC, hCB⟩ ⟨D, hAD, hDB⟩,
    dsimp,
    simp only [map_le_iff_le_comap, comap_map_mkq],
    rw sup_eq_right.2 (comap_mono hAD : comap B.subtype A ≤ comap B.subtype D),
    refine ⟨λ h x hxC, _, comap_mono⟩,
    specialize h (_ : B.subtype ⟨x, hCB hxC⟩ ∈ C),
    exacts [hxC, h],
  end }

[Daan van Gent]

Thanks for your effort! I was really struggling with val/coe/etc. Do you mind if I pull request this to mathlib?

[Daan van Gent]

I did some experimenting by moving to_fun and inv_fun to separate definitions, and it becomes way faster. It seems like inv_fun is somewhat slow, and if we leave it inline as in your code it seems like it has to 'parse' (for lack of a better word) that multiple times.

[Daan van Gent]

I am now at the final stages of my proofs. I only require the following instance. However, I seem unable to tell Lean that beta is a bounded_order. Any hints?

import order.cover order.atoms

instance is_simple_order_of_equiv {α : Type*} [has_le α] [bounded_order α] [partial_order α]
  {β : Type*} [has_le β] [bounded_order β] [partial_order β] [h : is_simple_order α] (f : α ≃o β) :
  is_simple_order β := {
  exists_pair_ne := begin
    rcases h.exists_pair_ne with ⟨x, y, h⟩,
    exact ⟨f x, f y, λ i, h ((order_iso.apply_eq_iff_eq f).mp i)⟩,
  end,
  eq_bot_or_eq_top := λ z, begin
    cases h.eq_bot_or_eq_top (f.symm z), {
      left,
      have := congr_arg ⇑f h_1,
      rw f.apply_symm_apply at this,
      --letI : order_bot β := bounded_order.to_order_bot β,
      have := @order_iso.map_bot α β _ _ _ _,
    }
  end }

[Daan van Gent]

Nevermind, I figured it out. has_le and partial_order conflict, so it should be {α : Type*} [partial_order α] [bounded_order α].

[Eric Wieser]

is_simple_order_of_equiv can't be an instance as lean can't find f, but it should be a @[reducible] def.

[Eric Wieser]

You should be able to golf that by using docs#function.injective.nontrivial