Commit b4a7af8f authored by Jakob von Raumer's avatar Jakob von Raumer

add omega for free group thing

parent b3287924
......@@ -187,7 +187,6 @@ end
-- CvW Theorem 46
@[hott] def cycle_induction
(C : is_locally_confluent R)
(N : well_founded (λ a b, R b a))
(Q : Π x, Rs* x x → Type w)
(Qnil : Π x (p : Rs* x x), trc_length _ p = 0 → Q x p)
(Qconf : Π a b c (s : R b a) (t : R b c),
......
import .util .confluence
import .util .confluence .trsc_glue
open hott hott.trunc hott.is_equiv hott.quotient hott.equiv hott.eq
open hott.is_trunc hott.pi
......@@ -91,6 +91,48 @@ by { hinduction x, refl, refl }
λ l l', Σ (xs ys : list (A ⊎ A)) (x : A ⊎ A),
(l = xs ++ x :: flip x :: ys) × (l' = xs ++ ys)
local notation `R ` := freegrp_rel.{u}
local notation `R* ` := trc.{u u} R
local notation `Rs*` := trc (sc R)
local notation c`::`r := trc.snoc.{u u} c r
local notation c`:::`:100d := trc.trans.{u u} _ c d
local notation r`⁺`:1200 := trc.sc.pos.{u u} r
local notation r`⁻`:1200 := trc.sc.neg.{u u} r
@[hott] def freegrp_obj := @quotient unit (λ _ _, A)
@[hott] def freegrp_loops := @eq (@freegrp_obj A)
(class_of _ ⋆) (class_of _ ⋆)
@[hott] def omega0 : A ⊎ A → (@freegrp_loops A) :=
begin
intro x, hinduction x with x x,
{ exact eq_of_rel _ x },
{ exact (eq_of_rel _ x)⁻¹ᵖ }
end
@[hott] def omega0_flip_right (x : A ⊎ A) :
(omega0 x) ⬝ (omega0 (flip x)) = idp :=
by { hinduction x, apply con.right_inv, apply con.left_inv }
@[hott] def omega0_flip_left (x : A ⊎ A) :
(omega0 (flip x)) ⬝ (omega0 x) = idp :=
by { hinduction x, apply eq.con.left_inv, apply eq.con.right_inv }
@[hott] def omega : quotient (@freegrp_rel A) → (@freegrp_loops A) :=
begin
intro x, hinduction x with xs xs ys H,
{ hinduction xs with x xs ih, exact idp, exact ih ⬝ omega0 x },
{ hinduction H with xs' H, hinduction H with ys' H,
hinduction H with x H, hinduction H with eH eH', dsimp,
rwr eH, clear eH xs, rwr eH', clear eH' ys,
hinduction xs' with x' xs' ih,
{ transitivity, apply con.assoc,
transitivity, rwr omega0_flip_left x, refl }, --TODO replace rwr
{ change _ ⬝ _ = _ ⬝ _, apply ap (λ x, x ⬝ omega0 x'),
exact ih } }
end
-- CvW Lemma 25
@[hott] def freegrp_rel_confluent :
@is_locally_confluent.{u u} (list (A ⊎ A)) (@freegrp_rel A) :=
......@@ -109,7 +151,7 @@ begin
{ rwr [es', p2, list.append_assoc],
apply trc.base, exact ⟨xs' ++ zs, ys, x, idp, idp⟩ } },
hinduction H with H H,
{ fconstructor, exact xs' ++ x' :: ys, fconstructor,
{ fconstructor, exact xs' ++ (list.cons x' ys), fconstructor,
{ rwr [er', H.1, ←list.append_assoc], apply trc.refl },
{ rwr [es', ←flip_flip x', ←H.2.1, ←H.2.2], apply trc.refl } },
hinduction H with H H,
......@@ -117,7 +159,7 @@ begin
{ rwr [er'], apply trc.refl },
{ rwr [es', ←H.1, ←H.2.2.2], apply trc.refl } },
hinduction H with H H,
{ fconstructor, exact xs ++ x :: ys', fconstructor,
{ fconstructor, exact xs ++ (list.cons x ys'), fconstructor,
{ rwr [er', H.2.2, H.2.1, flip_flip], apply trc.refl },
{ rwr [es', H.1, ←list.append_assoc], dsimp,
rwr [←flip_flip x, ←H.2.1, ←H.2.2], apply trc.refl } },
......
......@@ -214,6 +214,10 @@ end
@[hott] def trsc_of_trc_pos {a b : A} (r : R* a b) : Rs* a b :=
by { hinduction r with a a b c r s ih, fconstructor, exact ih :: s⁺ }
@[hott] def trsc_of_trc_pos_base {a b : A} (r : R a b) :
trsc_of_trc_pos _ (trc.base _ r) = trc.base _ (sc.pos r) :=
idp
@[hott] def is_increasing_trsc_of_trc_pos {a b : A} (r : R* a b) :
is_increasing R (trsc_of_trc_pos R r) :=
by { hinduction r, fconstructor, fconstructor, assumption }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment