Convert Multiplicative Z to Z

Stream: new members

[Jakub Nowak]

Is there a simpler way?

import Mathlib

example (i j : Multiplicative ℤ) : i * j = (0 : ℤ) := by
  rw [show i * j = (Multiplicative.toAdd i) + Multiplicative.toAdd j from rfl]
  set i : ℤ := i
  set j : ℤ := j
  unfold Multiplicative.toAdd
  unfold Multiplicative.ofAdd
  simp
  clear_value i j
  clear * -
  guard_hyp i : ℤ
  guard_hyp j : ℤ
  guard_target = i + j = 0

[Ruben Van de Velde]

import Mathlib

example (i j : Multiplicative ℤ) : i * j = 1 := by
  induction i with | ofAdd i =>
  induction j with | ofAdd j =>
  rw [← ofAdd_add, ofAdd_eq_one]
  guard_hyp i : ℤ
  guard_hyp j : ℤ
  guard_target = i + j = 0
  sorry

[Ruben Van de Velde]

(Why isn't docs#ofAdd_add namespaced?)

[Jakub Nowak]

With more complicated expression it's pretty hard to push Multiplicative.ofAdd. For example here's my code:

import Mathlib

variable {T : ℝ} (hT : T ≠ 0)

def intToFundamentalGroupAddCircle : Multiplicative ℤ →ₙ* FundamentalGroup (AddCircle T) 0 where
  toFun (i : ℤ) := .mk {
      toFun x := ((i : ℝ) * T) * (x : ℝ)
      source' := by simp
      target' := by
        simp
        rw [AddCircle.coe_period]
        simp
    }
  map_mul' i j := by
    cases i with | ofAdd i =>
    cases j with | ofAdd j =>
    rw [← ofAdd_add]
    -- ???

[Aaron Liu]

you're commiting defeq abuse

[Jakub Nowak]

Is there a way to have a homeomorphism from AddGroup to Group to avoid this?

[Jakub Nowak]

Or I could try to use Additive (FundamentalGroup (AddCircle T) 0) instead.

[Aaron Liu]

try this instead

import Mathlib

variable {T : ℝ} (hT : T ≠ 0)

def intToFundamentalGroupAddCircle : Multiplicative ℤ →ₙ* FundamentalGroup (AddCircle T) 0 where
  toFun i := .mk {
      toFun x := ((Int.cast (Multiplicative.toAdd i : ℤ)) * T) * (x : ℝ)
      source' := by simp
      target' := by
        simp
        rw [AddCircle.coe_period]
        simp
    }
  map_mul' i j := by
    cases i with | ofAdd i =>
    cases j with | ofAdd j =>
    rw [← ofAdd_add, toAdd_ofAdd, toAdd_ofAdd, toAdd_ofAdd]
    -- I don't know the proof so you'll have to continue from here
    /-
    T : ℝ
    hT : T ≠ 0
    i j : ℤ
    ⊢ Path.Homotopic.Quotient.mk
        { toFun := fun x => ↑(↑(i + j) * T * ↑x), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } =
      Path.Homotopic.Quotient.mk { toFun := fun x => ↑(↑i * T * ↑x), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } *
        Path.Homotopic.Quotient.mk { toFun := fun x => ↑(↑j * T * ↑x), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
    -/
    sorry

[Jakub Nowak]

Thanks! Looks like simp also works instead of manual rw there.