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

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

theory Ringoid : base:?Logic = 
	include ?Magma ❙

  theory ringoid_theory : base:?Logic =
    structure addition : ?Magma/magma_theory =
      	universe @ R ❙
		op @ plus ❘ # 1 + 2 prec 5❙
	❚ 
	structure multiplication : ?Magma/magma_theory =
			universe = R ❙
			op  @ times ❘ # 1 ⋅ 2 prec 6❙
	❚
    axiom_distributive : ⊦ prop_distributive plus times ❙
  ❚
  ringoid = Mod ☞?Ringoid/ringoid_theory ❙
❚

/T MiKo: refactor this with Ringoid ❚
theory Rig : base:?Logic =
	include ?AbelianGroup ❙
	
	theory rig_theory : base:?Logic =
		include ☞sets:?SetStructures/setstruct_theory ❙
		structure addition : ?AbelianGroup/abeliangroup_theory =
			universe = ☞sets:?SetStructures/setstruct_theory?universe ❘ # Uadd ❙
			op @ rplus ❘ # 1 + 2 prec 5❙
			unit @ rzero ❘ # O ❙
			inverse @ rminus ❘ # - 1 ❙
		❚ 
		structure multiplication : ?SemiGroup/semigroup_theory =
			universe = ☞sets:?SetStructures/setstruct_theory?universe ❘ # Umult ❙
			op  @ rtimes ❘ # 1 ⋅ 2 prec 6❙
		❚
		unitset = ⟨ x: U | ⊦ x ≠ O ⟩ ❙
		axiom_distributive : ⊦ prop_distributive rplus rtimes ❙
	❚ 
	rig = Mod ☞?Rig/rig_theory ❙
	
	unitsetOf : rig ⟶ type ❘ = [r] r.unitset ❙
	axiom_rigUnitsetSubtype : {r : rig} r.unitset <* r.universe ❙
	
	additiveGroup : rig ⟶ abeliangroup ❘ = [r] [' 
		universe := r.universe,
		op := r.rplus ,
		axiom_associative := r.addition/axiom_associative , 
		unit := r.rzero ,
		axiom_leftUnital := r.addition/axiom_leftUnital ,
		axiom_rightUnital := r.addition/axiom_rightUnital ,
		inverse := r.rminus ,
		axiom_inverse := r.addition/axiom_inverse ,
		axiom_commutative := r.addition/axiom_commutative
		'] ❙
	multiplicative_semigroup : rig ⟶ semigroup ❘ = [r] ['
			universe := r.universe,
			op := (r.rtimes) ,
			axiom_associative := r.multiplication/axiom_associative
		'] ❙ // needs proof that ret type = unitset ❙
❚
		
theory Ring : base:?Logic =
	include ?Rig ❙
		// TODO needs refactoring once structures work ❙
	theory ring_theory : base:?Logic =
		include ?Rig/rig_theory ❙
		rone : U ❘ # I ❙
		axiom_oneNeqZero : ⊦ I ≠ O ❙
		axiom_leftUnital : ⊦ ∀[x : U] I ⋅ x ≐ x ❙
		axiom_rightUnital : ⊦ ∀[x : U] x ⋅ I ≐ x ❙
	❚
	ring = Mod ☞?Ring/ring_theory ❙

	
	multiplicative_monoid : ring ⟶ monoid ❘ = [r] ['
			universe := r.universe,
			op := r.rtimes,
			axiom_associative := r.multiplication/axiom_associative,
			unit := r.rone,
			axiom_leftUnital := r.axiom_leftUnital,
			axiom_rightUnital := r.axiom_rightUnital
		'] ❙
❚
		
theory Field : base:?Logic =
	include ?Ring ❙

	theory field_theory : base:?Logic =
		include ?Ring/ring_theory ❙
		
		inverse : unitset ⟶ unitset ❘ # 1 ⁻¹  prec 24 ❙
		axiom_inverse : ⊦ ∀ [x : unitset] x ⋅ (x ⁻¹) ≐ I ❙
		
		axiom_commutative : ⊦ ∀[x : U]∀[y] (x ⋅ y) ≐ (y ⋅ x) ❙
	❚
	field : kind ❘ = Mod ☞?Field/field_theory ❘ role abbreviation ❙

	
	// multiplicative_group : field ⟶ abeliangroup ❘ = [r] ['
			universe := r.unitset,
			op := r.times,
			isassociative := r.timesisassociative,
			unit := r.timesunit,
			leftunital := r.timesleftunital,
			rightunital := r.timesrightunital,
			inverse := r.timesinverse ,
			inverseproperty := r.timesinverseproperty ,
			abelianax := r.timesabelianax
		'] ❙
❚