fix left module namespace

algebra/module.hlean

@@ -8,9 +8,7 @@ Modules prod vector spaces over a ring.
 (We use "left_module," which is more precise, because "module" is a keyword.)
 -/
 import algebra.field ..move_to_lib
-open is_trunc pointed function sigma eq
-
-namespace algebra
+open is_trunc pointed function sigma eq algebra
 
 structure has_scalar [class] (F V : Type) :=
 (smul : F → V → V)
@@ -19,6 +17,8 @@ infixl ` • `:73 := has_scalar.smul
 
 /- modules over a ring -/
 
+namespace left_module
+
 structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, ab_group M renaming
   mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg
   mul_left_inv→add_left_inv mul_comm→add_comm :=
@@ -155,7 +155,7 @@ pointed.mk zero
 definition pSet_of_LeftModule [coercion] {R : Ring} (M : LeftModule R) : Set* :=
 pSet.mk' (LeftModule.carrier M)
 
-namespace left_module
+section
   variable {R : Ring}
 
   structure homomorphism (M₁ M₂ : LeftModule R) : Type :=
@@ -219,6 +219,6 @@ namespace left_module
   end
 end
 
-end left_module
+end
 
-end algebra
+end left_module

algebra/module_chain_complex.hlean

@@ -6,7 +6,7 @@ open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc
 open algebra function
 open chain_complex
 open succ_str
-open algebra.left_module
+open left_module
 
 structure module_chain_complex (R : Ring) (N : succ_str) : Type :=
 (mod : N → LeftModule R)

algebra/short_five.hlean

@@ -4,10 +4,7 @@ Author: Jeremy Avigad
 import .module_chain_complex
 open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc
 open algebra function succ_str
-
--- TODO: reconcile these
-open algebra.left_module    -- name in left_module
-open left_module            -- namespace in hott library
+open left_module
 
 section short_five
   variable  {R : Ring}