Spectral/algebra/tensor.hlean

41 lines
1.2 KiB
Text
Raw Permalink Normal View History

/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
2016-05-12 20:57:33 +00:00
Authors: Floris van Doorn, Egbert Rijke
2017-07-04 15:11:21 +00:00
Tensor group
-/
2017-07-04 15:11:21 +00:00
import .free_abelian_group
open eq algebra is_trunc sigma sigma.ops prod trunc function equiv
namespace group
variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
/- Tensor group (WIP) -/
2015-12-10 20:46:09 +00:00
2015-12-11 02:17:29 +00:00
/- namespace tensor_group
variables {A B}
local abbreviation ι := @free_ab_group_inclusion
2015-12-10 20:46:09 +00:00
inductive tensor_rel_type : free_ab_group (Set_of_Group A ×t Set_of_Group B) → Type :=
2015-12-11 02:17:29 +00:00
| mul_left : Π(a₁ a₂ : A) (b : B), tensor_rel_type (ι (a₁, b) * ι (a₂, b) * (ι (a₁ * a₂, b))⁻¹)
| mul_right : Π(a : A) (b₁ b₂ : B), tensor_rel_type (ι (a, b₁) * ι (a, b₂) * (ι (a, b₁ * b₂))⁻¹)
2015-12-10 20:46:09 +00:00
2015-12-11 02:17:29 +00:00
open tensor_rel_type
2015-12-10 20:46:09 +00:00
definition tensor_rel' (x : free_ab_group (Set_of_Group A ×t Set_of_Group B)) : Prop :=
2015-12-11 02:17:29 +00:00
∥ tensor_rel_type x ∥
2015-12-10 20:46:09 +00:00
definition tensor_group_rel (A B : AbGroup)
: normal_subgroup_rel (free_ab_group (Set_of_Group A ×t Set_of_Group B)) :=
2015-12-11 02:17:29 +00:00
sorry /- relation generated by tensor_rel'-/
2015-12-10 20:46:09 +00:00
definition tensor_group [constructor] : AbGroup :=
quotient_ab_group (tensor_group_rel A B)
2015-12-11 02:17:29 +00:00
end tensor_group-/
2015-12-10 20:46:09 +00:00
end group