97 lines
3 KiB
Text
97 lines
3 KiB
Text
/-
|
||
Copyright (c) 2016 Floris van Doorn. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Floris van Doorn
|
||
|
||
-/
|
||
|
||
-- to be moved to algebra/homotopy_group in the Lean library
|
||
|
||
import group_theory.basic algebra.homotopy_group
|
||
|
||
open eq algebra pointed group trunc is_trunc nat algebra equiv is_equiv
|
||
|
||
namespace my
|
||
|
||
section
|
||
variables {A B C : Type*}
|
||
definition apn_compose (n : ℕ) (g : B →* C) (f : A →* B) : apn n (g ∘* f) ~* apn n g ∘* apn n f :=
|
||
begin
|
||
induction n with n IH,
|
||
{ reflexivity},
|
||
{ refine ap1_phomotopy IH ⬝* _, apply ap1_compose}
|
||
end
|
||
|
||
theorem ap1_con (f : A →* B) (p q : Ω A) : ap1 f (p ⬝ q) = ap1 f p ⬝ ap1 f q :=
|
||
begin
|
||
rewrite [▸*, ap_con, +con.assoc, con_inv_cancel_left]
|
||
end
|
||
|
||
definition apn_con {n : ℕ} (f : A →* B) (p q : Ω[n + 1] A)
|
||
: apn (n+1) f (p ⬝ q) = apn (n+1) f p ⬝ apn (n+1) f q :=
|
||
ap1_con (apn n f) p q
|
||
|
||
definition tr_mul {n : ℕ} (p q : Ω[n + 1] A) : @mul (πg[n+1] A) _ (tr p ) (tr q) = tr (p ⬝ q) :=
|
||
by reflexivity
|
||
end
|
||
|
||
section
|
||
|
||
parameters {A B : Type} (f : A ≃ B) [group A]
|
||
|
||
definition group_equiv_mul (b b' : B) : B := f (f⁻¹ᶠ b * f⁻¹ᶠ b')
|
||
|
||
definition group_equiv_one : B := f one
|
||
|
||
definition group_equiv_inv (b : B) : B := f (f⁻¹ᶠ b)⁻¹
|
||
|
||
local infix * := my.group_equiv_mul f
|
||
local postfix ^ := my.group_equiv_inv f
|
||
local notation 1 := my.group_equiv_one f
|
||
|
||
theorem group_equiv_mul_assoc (b₁ b₂ b₃ : B) : (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) :=
|
||
by rewrite [↑group_equiv_mul, +left_inv f, mul.assoc]
|
||
|
||
theorem group_equiv_one_mul (b : B) : 1 * b = b :=
|
||
by rewrite [↑group_equiv_mul, ↑group_equiv_one, left_inv f, one_mul, right_inv f]
|
||
|
||
theorem group_equiv_mul_one (b : B) : b * 1 = b :=
|
||
by rewrite [↑group_equiv_mul, ↑group_equiv_one, left_inv f, mul_one, right_inv f]
|
||
|
||
theorem group_equiv_mul_left_inv (b : B) : b^ * b = 1 :=
|
||
by rewrite [↑group_equiv_mul, ↑group_equiv_one, ↑group_equiv_inv,
|
||
+left_inv f, mul.left_inv]
|
||
|
||
definition group_equiv_closed : group B :=
|
||
⦃group,
|
||
mul := group_equiv_mul,
|
||
mul_assoc := group_equiv_mul_assoc,
|
||
one := group_equiv_one,
|
||
one_mul := group_equiv_one_mul,
|
||
mul_one := group_equiv_mul_one,
|
||
inv := group_equiv_inv,
|
||
mul_left_inv := group_equiv_mul_left_inv,
|
||
is_set_carrier := is_trunc_equiv_closed 0 f⦄
|
||
|
||
end
|
||
|
||
end my open my
|
||
|
||
namespace eq
|
||
|
||
local attribute mul [unfold 2]
|
||
definition homotopy_group_homomorphism [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
|
||
: πg[n+1] A →g πg[n+1] B :=
|
||
begin
|
||
fconstructor,
|
||
{ exact phomotopy_group_functor (n+1) f},
|
||
{ intro g,
|
||
refine @trunc.rec _ _ _ (λx, !is_trunc_eq) _, intro h,
|
||
refine @trunc.rec _ _ _ (λx, !is_trunc_eq) _ g, clear g, intro g,
|
||
rewrite [tr_mul, ▸*],
|
||
apply ap tr, apply apn_con}
|
||
end
|
||
|
||
notation `π→g[`:95 n:0 ` +1] `:0 f:95 := homotopy_group_homomorphism n f
|
||
|
||
end eq
|