expanding to_fun

Stream: new members

[Jon Eugster]

What am I missing here? How do I access the underlying function of a linear map. I would like to do something like unfold g.to_funin the proof, but that doesn't work.

import algebra.algebra.basic

variables {B: Type*} [comm_ring B]

def g: B→ₗ[B]B :=
  {to_fun := λx, -x,  -- this would be something more elaborate, like ` λx, f(g(h(x)))`
    map_add' :=
    begin
      intros x y,
      exact neg_add x y,
    end,
    map_smul' :=
    begin
      simp,
    end,
  }

example: g.to_fun = (λ(x:B), x) :=
begin
  sorry,
end

example (y:B): g.to_fun y = (λ(x:B), x) y:=
begin
  sorry,
end

[Mario Carneiro]

rfl?

[Jon Eugster]

That's what I thought too, but it doesnt seem to work...

[Mario Carneiro]

probably because you said it is \lam x, x instead of \lam x, -x

[Jon Eugster]

oh, you're right it does work here. Let me see if I can create a valid #mwe where it doesn't work, sorry.

[Jon Eugster]

updated #mwe. Is it the have g := ... that is wrong here?

import ring_theory.integral_closure
import ring_theory.localization -- for fraction_ring


 lemma my_lemma
  (A L : Type*) [field L] [integral_domain A]
  [algebra A L] :
  true :=
begin
  have g: A →ₗ[A] A:=
  {
    to_fun := λ(x:A), -x,
    map_add' :=
    begin
      intros x y,
      exact neg_add x y,
    end,
    map_smul' :=
    begin
      simp,
    end,
  },
  have hg: g.to_fun = λ(x:A), -x :=
  begin
    apply rfl, -- error
    /-
    invalid apply tactic, failed to unify
    g.to_fun = λ (x : A), -x
    with
    ?m_2 = ?m_
    -/
  end,
  exact true,
end

[Mario Carneiro]

yes, if you use have g then lean will not be able to unfold g later, you need let g

[Jon Eugster]

oh, thank you! I've been going completely the wrong way with this