Semibilinear maps as curryied linear maps

semibilin1.lean

structure semibilin_map (R : Type*) (R₂ : Type*) (S : Type*) (S₂ : Type*)
  [semiring R] [semiring R₂] [semiring S] [semiring S₂]
  (M : Type*) (N : Type*) (P : Type*)
  [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P]
  [module R M] [module S N] [module R₂ P] [module S₂ P]
  [smul_comm_class S₂ R₂ P]
  (ρ₁₂ : R →+* R₂) (σ₁₂ : S →+* S₂)
  := (bilin : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P)

namespace semibilin_map

variables {R : Type*} [semiring R] {S : Type*} [semiring S]
variables {R₂ : Type*} [semiring R₂] {S₂ : Type*} [semiring S₂]
variables {M : Type*} {N : Type*} {P : Type*}
variables {Nₗ : Type*} {Pₗ : Type*}
variables {M' : Type*} {N' : Type*} {P' : Type*}

variables [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P]
variables [add_comm_monoid Nₗ] [add_comm_monoid Pₗ]
variables [add_comm_group M'] [add_comm_group N'] [add_comm_group P']
variables [module R M] [module S N] [module R₂ P] [module S₂ P]
variables [module R Pₗ] [module S Pₗ]
variables [module R M'] [module S N'] [module R₂ P'] [module S₂ P']
variables [smul_comm_class S₂ R₂ P] [smul_comm_class S R Pₗ] [smul_comm_class S₂ R₂ P']
variables {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
variables (B : semibilin_map R R₂ S S₂ M N P ρ₁₂ σ₁₂)
variables (D : semibilin_map R R₂ S S₂ M N P ρ₁₂ σ₁₂)
variables (B₁ : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P)

def mk_aux (ρ₁₂ : R →+* R₂) (σ₁₂ : S →+* S₂) (f : M → N → P)
  (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
  (H2 : ∀ (c:R) m n, f (c • m) n = (ρ₁₂ c) • f m n)
  (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
  (H4 : ∀ (c:S) m n, f m (c • n) = (σ₁₂ c) • f m n) : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P :=
{ to_fun := λ m, { to_fun := f m, map_add' := H3 m, map_smul' := λ c, H4 c m},
  map_add' := λ m₁ m₂, linear_map.ext $ H1 m₁ m₂,
  map_smul' := λ c m, linear_map.ext $ H2 c m }

/-- Create a bilinear map from a function that is semilinear in each component.
See `mk₂'` and `mk₂` for the linear case. -/

def mk₂ (ρ₁₂ : R →+* R₂) (σ₁₂ : S →+* S₂) (f : M → N → P)
  (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
  (H2 : ∀ (c:R) m n, f (c • m) n = (ρ₁₂ c) • f m n)
  (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
  (H4 : ∀ (c:S) m n, f m (c • n) = (σ₁₂ c) • f m n) : semibilin_map R R₂ S S₂ M N P ρ₁₂ σ₁₂ :=
{bilin := mk_aux ρ₁₂ σ₁₂ f H1 H2 H3 H4}

instance : has_coe_to_fun (semibilin_map R R₂ S S₂ M N P ρ₁₂ σ₁₂) (λ _, M → N → P)
  := ⟨ λ b x y, b.bilin x y⟩

lemma ext_aux (f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P)
  (H : ∀ m n, f m n = g m n) : f = g :=
linear_map.ext (λ m, linear_map.ext $ λ n, H m n)

@[ext] lemma ext {B D : semibilin_map R R₂ S S₂ M N P ρ₁₂ σ₁₂} (H : ∀ x y, B x y = D x y) : B = D :=
by { cases B, cases D, congr, funext, exact (ext_aux B D H) }

section

local attribute [instance] smul_comm_class.symm
open_locale big_operators

def flip_aux (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) : N →ₛₗ[σ₁₂] M →ₛₗ[ρ₁₂] P :=
mk_aux σ₁₂ ρ₁₂ (λ n m, f m n)
  (λ n₁ n₂ m, (f m).map_add _ _)
  (λ c n m, (f m).map_smulₛₗ _ _)
  (λ n m₁ m₂, by rw f.map_add; refl)
  (λ c n m, by rw f.map_smulₛₗ; refl)

/- Given a linear map from `M` to linear maps from `N` to `P`, i.e., a bilinear map from `M × N` to
`P`, change the order of variables and get a linear map from `N` to linear maps from `M` to `P`. -/
def flip (B : semibilin_map R R₂ S S₂ M N P ρ₁₂ σ₁₂) : semibilin_map S S₂ R R₂ N M P σ₁₂ ρ₁₂ :=
  {bilin := flip_aux B.bilin}