Semibilinear maps raw

semibilin2.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)
  (bilin_add_left : ∀ x y z, bilin (x + y) z = bilin x z + bilin y z)
  (bilin_smul_left : ∀ (a : R) x y, bilin (a • x) y = ρ₁₂ a • (bilin x y))
  (bilin_add_right : ∀ x y z, bilin x (y + z) = bilin x y + bilin x z)
  (bilin_smul_right : ∀ (a : S) x y, bilin x (a • y) = σ₁₂ a • (bilin x y))

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 ρ₁₂ σ₁₂)

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

@[ext] lemma ext (H : ∀ x y, B x y = D x y) : B = D :=
by { cases B, cases D, congr, funext, exact H _ _ }

local attribute [instance] smul_comm_class.symm

def flip (A : semibilin_map R R₂ S S₂ M N P ρ₁₂ σ₁₂) : semibilin_map S S₂ R R₂ N M P σ₁₂ ρ₁₂ :=
  { bilin := λ x y, A y x,
    bilin_add_left := λ x y z, A.bilin_add_right z x y,
    bilin_smul_left := λ a x y, A.bilin_smul_right a y x,
    bilin_add_right := λ x y z, A.bilin_add_left y z x,
    bilin_smul_right := λ a x y, A.bilin_smul_left a y x }

end semibilin_map