namespace http://mathhub.info/MitM/core/algebra ❚

import base http://mathhub.info/MitM/Foundation ❚
import num http://mathhub.info/MitM/core/arithmetics ❚
import sets http://mathhub.info/MitM/core/typedsets ❚

theory Module : base:?Logic =
	include ?Ring ❙
	prop_dist1 : {A : type,B : type} (A ⟶ B ⟶ B) ⟶ (B ⟶ B ⟶ B) ⟶ bool ❘ 
		= [A,B,itimes,iplus] ∀[r]∀[x]∀[y] itimes r (iplus x y) ≐ iplus (itimes r x) (itimes r y) ❘ # prop_dist1 3 4❙
	prop_dist2 : {A : type,B : type} (A ⟶ B ⟶ B) ⟶ (A ⟶ A ⟶ A) ⟶ (B ⟶ B ⟶ B) ⟶ bool ❘ 
		= [A,B,itimes,plus1,plus2] ∀[r]∀[s]∀[x] itimes (plus1 r s) x ≐ plus2 (itimes r x) (itimes s x) ❘ # prop_dist2 3 4 5❙
	prop_associative_scalars : {A : type,B : type} (A ⟶ B ⟶ B) ⟶ (A ⟶ A ⟶ A) ⟶ bool ❘
		= [A,B,itimes,stimes] ∀[r]∀[s]∀[x] itimes r (itimes s x) ≐ itimes (stimes r s) x ❘ # prop_associative_scalars 3 4 ❙
	prop_unit_scalars : {A : type, B : type} (A ⟶ B ⟶ B) ⟶ A ⟶ bool ❘
		= [A,B,itimes,u] ∀[x] itimes u x ≐ x ❘ # prop_unit_scalars 3 4❙
	
	theory module_theory : base:?Logic > scalars : ring ❘ =
		scaltp : type ❘ = scalars.universe ❙
		
		include ?AbelianGroup/abeliangroup_theory ❙
		
		scalarmult : scaltp ⟶ U ⟶ U ❘ # 1 ⋅ 2 ❙
		axiom_dist1 : ⊦ prop_dist1 scalarmult op❙
		axiom_dist2 : ⊦ prop_dist2 scalarmult (scalars.rplus) op ❙
		axiom_associative_scalars : ⊦ prop_associative_scalars scalarmult (scalars.rtimes) ❙
		axiom_unit_scalars : ⊦ prop_unit_scalars scalarmult (scalars.rone) ❙
	❚ 
	
	module = [R : ring] Mod ☞?Module/module_theory R ❙
	
	distributive_right : {R : ring} ⊦ prop_dist2 (R.rtimes) (R.rplus) (R.rplus) ❘ # distributive_right 1 ❙
		
	asModule : {F : ring} module F ❘ = [f] ['
		universe := f.universe,
		op := f.rplus,
		axiom_associative := f.addition/axiom_associative,
		unit := f.rzero,
		axiom_leftUnital := f.addition/axiom_leftUnital,
		axiom_rightUnital := f.addition/axiom_rightUnital,
		inverse := f.rminus,
		axiom_inverse := f.addition/axiom_inverse,
		axiom_commutative := f.addition/axiom_commutative,
		scalarmult := f.rtimes,
		axiom_dist1 := f.axiom_distributive,
		axiom_dist2 := distributive_right f,
		axiom_associative_scalars := f.multiplication/axiom_associative,
		axiom_unit_scalars := f.axiom_leftUnital
	'] ❘ # asMod 1 ❙
	
	// include base:?Sequences ❙
	
	// theory finGenFree_module_theory : base:?Logic > scalars : ring ❘ =
		// include ?module/module_theory ❙
		
		// flexary_sum : {n} U^n ⟶ U ❘ = [n,s] foldL op unit n s ❘ # ∑ 2 ❙
		
		// dimension : NAT ❙
		// basis : U^dimension ❙
		// is_basis : ⊦ ∀ [v : U] ∃ [s : scaltp^dimension] v ≐ (∑ ⟨' s..i ⋅ basis..i | i:dimension '⟩) ❙

❚
	
theory Vectorspace : base:?Logic =
	include ?Field ❙
	include ?Module ❙
	theory vectorspace_theory : base:?Logic > scalars : field ❘ =
		include ?Module/module_theory (scalars) ❙       
		bminus : U ⟶ U ⟶ U ❘ = [a,b] op a (inverse b) ❘ # 1 - 2❙
	❚ 
	vectorspace : field ⟶ kind ❘ = [F : field] Mod ☞?Vectorspace/vectorspace_theory F ❙

	include ?Module ❙
	
	asVectorspace : {F : field} vectorspace F ❘ = [f] ['
		universe := f.universe,
		op := f.rplus,
		axiom_associative := f.addition/axiom_associative,
		unit := f.rzero,
		axiom_leftUnital := f.addition/axiom_leftUnital,
		axiom_rightUnital := f.addition/axiom_rightUnital,
		inverse := f.rminus,
		axiom_inverse := f.addition/axiom_inverse,
		axiom_commutative := f.addition/axiom_commutative,
		scalarmult := f.rtimes,
		axiom_dist1 := f.axiom_distributive,
		axiom_dist2 := distributive_right f,
		axiom_associative_scalars := f.multiplication/axiom_associative,
		axiom_unit_scalars := f.axiom_leftUnital
	'] ❘ # asVectorspace 1 ❙
❚

theory Productspace : base:?Logic =
	include ?Vectorspace ❙
	include ☞base:?ProductTypes ❙
	
	product_universe : {F : field} vectorspace F ⟶ vectorspace F ⟶ type ❘ = [F,v1,v2] v1.universe × v2.universe ❘ # 2 x_ 1 3❙
	product_op : {F : field, v1: vectorspace F, v2: vectorspace F} (v1 x_ F v2) ⟶ (v1 x_ F v2) ⟶ (v1 x_ F v2) ❘
		= [F,v1,v2] [a,b] ⟨ ((v1.op) (πl a) (πl b)), ((v2.op) (πr a) (πr b))⟩ ❘ # 2 xop_ 1 3 ❙
	product_unit : {F : field, v1 : vectorspace F, v2 : vectorspace F} v1 x_ F v2 ❘
		= [F,v1,v2] ⟨ (v1.unit), (v2.unit) ⟩ ❘ # product_unit 1 2 3 ❙
	product_inverse : {F : field, v1 : vectorspace F, v2 : vectorspace F}(v1 x_ F v2) ⟶ (v1 x_ F v2) ❘
		= [F,v1,v2] [x] ⟨ (v1.inverse) πl x, (v2.inverse) πr x ⟩ ❘ # product_inverse 1 2 3 ❙
	product_scalarmult : {F : field, v1: vectorspace F, v2: vectorspace F} F.universe ⟶ (v1 x_ F v2) ⟶ (v1 x_ F v2) ❘
		= [F,v1,v2][α,v] ⟨ ((v1.scalarmult) α (πl v)), ((v2.scalarmult) α (πr v)) ⟩ ❘ # product_scalarmult 1 2 3 ❙
		
	product_axiom_associative : {F : field, v1 : vectorspace F, v2 : vectorspace F}
		⊦ prop_associative (v1 xop_ F v2) ❘ # product_axiom_associative 1 2 3 ❙
	product_axiom_leftUnital : {F : field, v1 : vectorspace F, v2 : vectorspace F} 
		⊦ prop_leftUnital	(v1 xop_ F v2) (product_unit F v1 v2) ❘ # product_axiom_leftUnital 1 2 3 ❙
	product_axiom_rightUnital : {F : field, v1 : vectorspace F, v2 : vectorspace F} 
		⊦ prop_rightUnital	(v1 xop_ F v2) (product_unit F v1 v2) ❘ # product_axiom_rightUnital 1 2 3 ❙
	product_axiom_inverse : {F : field, v1 : vectorspace F, v2 : vectorspace F} 
		⊦ prop_inverse (v1 xop_ F v2) (product_inverse F v1 v2) (product_unit F v1 v2)❘ # product_axiom_inverse 1 2 3 ❙
	product_axiom_commutative : {F : field, v1 : vectorspace F, v2 : vectorspace F} 
		⊦ prop_commutative (v1 xop_ F v2) ❘ # product_axiom_commutative 1 2 3 ❙
	product_axiom_dist1 : {F : field, V1 : vectorspace F, V2 : vectorspace F} 
		⊦ prop_dist1 (product_scalarmult F V1 V2) (V1 xop_ F V2) ❘ # product_axiom_dist1 1 2 3 ❙
	product_axiom_dist2 : {F : field, V1 : vectorspace F, V2 : vectorspace F} 
		⊦ prop_dist2 (product_scalarmult F V1 V2) (F.rplus) (V1 xop_ F V2) ❘ # product_axiom_dist2 1 2 3 ❙
	product_axiom_associativeScalars : {F : field, V1 : vectorspace F, V2 : vectorspace F} 
		⊦ prop_associative_scalars (product_scalarmult F V1 V2) (F.rtimes) ❘ # product_axiom_associativeScalars 1 2 3 ❙
	product_axiom_unitScalars : {F : field, V1 : vectorspace F, V2 : vectorspace F} 
		⊦ prop_unit_scalars (product_scalarmult F V1 V2) (F.rone) ❘ # product_axiom_unitScalars 1 2 3 ❙
		
	productspace : {F : field} vectorspace F ⟶ vectorspace F ⟶ vectorspace F ❘ = [F] [v1] [v2] ['
		universe := v1 x_ F v2,
		op := v1 xop_ F v2,
		axiom_associative := product_axiom_associative F v1 v2,
		unit := product_unit F v1 v2,
		axiom_leftUnital := product_axiom_leftUnital F v1 v2,
		axiom_rightUnital := product_axiom_rightUnital F v1 v2,
		inverse := product_inverse F v1 v2,
		axiom_inverse := product_axiom_inverse F v1 v2,
		axiom_commutative := product_axiom_commutative F v1 v2,
		scalarmult := product_scalarmult F v1 v2,
		axiom_dist1 := product_axiom_dist1 F v1 v2,
		axiom_dist2 := product_axiom_dist2 F v1 v2,
		axiom_associative_scalars := product_axiom_associativeScalars F v1 v2,
		axiom_unit_scalars := product_axiom_unitScalars F v1 v2
	'] ❘ # 2 ov 3 ❙
	
	
	finite_vectorspace : {F: field} pos_lit ⟶ vectorspace F ❘ # 1 ^ 2 ❙
	// axiom_finite1 : {F : field} ⊦ eq (vectorspace F) (F ^ 1) (asVectorspace F) ❙
	// axiom_sr : {n} ⊦ finite_real_vectorspace (Succ n) ≐ productspace realField ℝ1 (finite_real_vectorspace n) ❙  
	
❚


theory LinearMaps : base:?Logic =
	include ?Productspace ❙
	
	theory linearMap_theory : base:?Logic > K : field, n1 : ℕ+, n2 : ℕ+ ❘ =
		V1 = K ^ n1 ❙
		V2 = K ^ n2 ❙
		fun : (V1.universe) ⟶ (V2.universe) ❙
		// insert axioms here...
		..
		.. ❙
	❚
	
	linearMap : field ⟶ ℕ+ ⟶ ℕ+ ⟶ type ❘ = [K : field][n1 : ℕ+,n2 : ℕ+] Mod ☞?LinearMaps/linearMap_theory K n1 n2 ❘ # linearMap 1 2 3❙
	// L : linearMap realfield 2 3 ❙
❚