mul_one_class, group… instances for dependend pi

Stream: Is there code for X?

[Antoine Chambert-Loir]

Why does not Lean find that some dependent products of groups are groups,

example {I : Type*} {f : I → Type*} {p : I → Prop}  [h : ∀ (i : I), group (f i))] : group (Π i, p i → f i) :=
sorry

The issue often appears when one wants to take a pi-type on a set.

It seems related to the fact that instances such as

 def pi.mul_one_class {I : Type u} {f : I → Type v} [Π (i : I), mul_one_class (f i)] :
mul_one_class (Π (i : I), f i)

that puts a multiplication with one on a pi type, lack a dependent version, such as

def pi.mul_one_class' {I : Type*} {f : I → Type*} {p : I → Prop}
[Π (i : I) (pi : p i), mul_one_class (f i)] :
mul_one_class (Π (i : I) (pi : p i), f i) :=
begin
  refine {
  one := λ i hi, _,
  mul := λ u v i hi,
  begin
    haveI : mul_one_class (f i) := _inst_1 i hi,
    exact (u i hi) * (v i hi),
  end,
  one_mul := λ u, begin
    ext i hi,
    dsimp, convert (_inst_1 i hi).one_mul (u i hi),
    end,
  mul_one := λ u, begin
    ext i hi,
    dsimp, convert (_inst_1 i hi).mul_one (u i hi),
    end, },
end```

Should it be added ?

[Yaël Dillies]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Sort-indexed.20pi.20type

[Yaël Dillies]

I have the full files for groups and modules ready on con-nf if you need them, but the current consensus is that we should not add them if we don't need them

[Antoine Chambert-Loir]

So the consensus is that rather than having some

example {ι : Type*} [decidable_eq ι] (p : α → ι) (s : finset ι) :
(Π i ∈ s, equiv.perm {a | p a = i}) →* equiv.perm α :=

we should work with

def toto {ι : Type*} [decidable_eq ι] (p : α → ι) (s : finset ι) :
(Π (i : s), equiv.perm {a | p a = i}) →* equiv.perm α :=

[Yaël Dillies]

Yes, basically.