automorphizing

Stream: Is there code for X?

[Alex Kontorovich]

I'm trying to port over some Lean3 code and am struggling here. Any help please? Thanks!

import Mathlib.Topology.Algebra.Group.Basic

open BigOperators

/-- Given a group `α` acting on a type `β`, and a function `f : β → M`, we "automorphize" `f` to a
  function `β ⧸ α → M` by summing over `α` orbits, `b ↦ ∑' (a : α), f(a • b)`. -/
def MulAction.automorphize {α β M : Type _} [TopologicalSpace M] [AddCommMonoid M] [T2Space M]
    [Group α] [MulAction α β] (f : β → M) : Quotient (MulAction.orbitRel α β) → M := by
  refine @Quotient.lift ?_ ?_ (mul_action.orbit_rel α β) (fun b ↦ ∑' (a : α), f(a • b))
  -- error : "missing end of character literal"


/-
Working Lean3 code:

def mul_action.automorphize [group α] [mul_action α β] (f : β → M) :
  quotient (mul_action.orbit_rel α β) → M :=
@quotient.lift _ _ (mul_action.orbit_rel α β) (λ b, ∑' (a : α), f(a • b))
begin
  rintros b₁ b₂ ⟨a, (rfl : a • b₂ = b₁)⟩,
  simpa [mul_smul] using (equiv.mul_right a).tsum_eq (λ a', f (a' • b₂)),
end
-/

[Ruben Van de Velde]

Is it because of the apostrophe after the sigma? Do you need to open or import something else? Or does it need to be open scoped BigOperators? (I thought not)

[Alex Kontorovich]

The apostrophe just means tsum; if the sum doesn't converge, then its value is set to 0.
I tried adding scoped and got the same error...

[Anatole Dedecker]

Is it the right sigma? EDIT: yes

[Anatole Dedecker]

Ah, it's just a missing import: you need Mathlib.Topology.Algebra.InfiniteSum.Basic

[Alex Kontorovich]

Heh, well, I didn't import that file because... that's the file I'm working on. But ok, new error message:

import Mathlib.Topology.Algebra.Group.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Basic

open BigOperators

/-- Given a group `α` acting on a type `β`, and a function `f : β → M`, we "automorphize" `f` to a
  function `β ⧸ α → M` by summing over `α` orbits, `b ↦ ∑' (a : α), f(a • b)`. -/
def MulAction.automorphize {α β M : Type _} [TopologicalSpace M] [AddCommMonoid M] [T2Space M]
    [Group α] [MulAction α β] (f : β → M) : Quotient (MulAction.orbitRel α β) → M := by
  refine @Quotient.lift ?_ ?_ (mul_action.orbit_rel α β) (fun b ↦ ∑' (a : α), f(a • b))
  -- error : "expected ')', ',' or ':'"


/-
Working Lean3 code:

def mul_action.automorphize [group α] [mul_action α β] (f : β → M) :
  quotient (mul_action.orbit_rel α β) → M :=
@quotient.lift _ _ (mul_action.orbit_rel α β) (λ b, ∑' (a : α), f(a • b))
begin
  rintros b₁ b₂ ⟨a, (rfl : a • b₂ = b₁)⟩,
  simpa [mul_smul] using (equiv.mul_right a).tsum_eq (λ a', f (a' • b₂)),
end
-/

[Anatole Dedecker]

Here is a working code:

import Mathlib.Topology.Algebra.Group.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Basic

open BigOperators

/-- Given a group `α` acting on a type `β`, and a function `f : β → M`, we "automorphize" `f` to a
  function `β ⧸ α → M` by summing over `α` orbits, `b ↦ ∑' (a : α), f(a • b)`. -/
noncomputable def MulAction.automorphize {α β M : Type _} [TopologicalSpace M] [AddCommMonoid M]
    [T2Space M] [Group α] [MulAction α β] (f : β → M) : Quotient (MulAction.orbitRel α β) → M := by
  refine @Quotient.lift _ _ (MulAction.orbitRel α β) (fun b ↦ ∑' (a : α), f (a • b)) ?_
  sorry

[Anatole Dedecker]

You need a whitespace between the function and the parenthesis. I'm not sure why though.

[Anatole Dedecker]

Note also that it doesn't work if the two first _ are ?_, because if you tell Lean "I'll tell you later" then he fails to unify it with anything that comes up.

[Patrick Massot]

Anatole Dedecker said:

You need a whitespace between the function and the parenthesis. I'm not sure why though.

This is a general fact in Lean 4.

[Alex Kontorovich]

Continuing to have some issues here: why is it not picking up the Setoid with Quotient.mk'? It did it fine in Lean3... (And it does it fine if I use Quotient.mk and feed it the Setoid explicitly...)

import Mathlib.Topology.Algebra.InfiniteSum.Basic

/-- Automorphization of a function into an `R`-`module` distributes, that is, commutes with the `R`
  -scalar multiplication. -/
lemma MulAction.automorphize_smul_left {α β M : Type _} [TopologicalSpace M] [AddCommMonoid M]
    [T2Space M] {R : Type _} [DivisionRing R] [Module R M] [ContinuousConstSMul R M] [Group α]
    [MulAction α β] (f : β → M) (g : Quotient (MulAction.orbitRel α β) → R) :
    MulAction.automorphize ((g ∘ (Quotient.mk')) • f)
      = g • (MulAction.automorphize f : Quotient (MulAction.orbitRel α β) → M) := sorry
-- error : "failed to synthesize instance Setoid β"

lemma MulAction.automorphize_smul_left' {α β M : Type _} [TopologicalSpace M] [AddCommMonoid M]
    [T2Space M] {R : Type _} [DivisionRing R] [Module R M] [ContinuousConstSMul R M] [Group α]
    [MulAction α β] (f : β → M) (g : Quotient (MulAction.orbitRel α β) → R) :
    MulAction.automorphize ((g ∘ (Quotient.mk (MulAction.orbitRel α β))) • f)
      = g • (MulAction.automorphize f : Quotient (MulAction.orbitRel α β) → M) := sorry

[Yakov Pechersky]

The definition of Quotient.mk' changed in lean4, to take an a TC arg instead of an implicit.

[Yakov Pechersky]

docs3#quotient.mk' docs#Quotient.mk'

[Eric Wieser]

Well that's super confusing, the primed versions swapped places with the unprimed one

[Eric Wieser]

Except presumably mathlib still uses the old convention

[Alex Kontorovich]

It's all worked out now, thanks... (for my application, that is...)