michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

construct the derived couple for graded modules

Browse source
This commit is contained in:
Floris van Doorn 2017-05-22 21:27:34 -04:00
parent 73a34e9edf
commit 798a57e546
6 changed files with 465 additions and 164 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

348
algebra/graded.hlean
View file

@ -4,13 +4,14 @@
import .left_module .direct_sum .submodule --..heq
open is_trunc algebra eq left_module pointed function equiv is_equiv prod group sigma nat
open is_trunc algebra eq left_module pointed function equiv is_equiv prod group sigma sigma.ops nat
trunc_index
namespace left_module
definition graded [reducible] (str : Type) (I : Type) : Type := I → str
definition graded_module [reducible] (R : Ring) : Type → Type := graded (LeftModule R)
-- TODO: We can (probably) make I a type everywhere
variables {R : Ring} {I : Set} {M M₁ M₂ M₃ : graded_module R I}
/-
@ -58,7 +59,37 @@ f ↘ idp
definition graded_hom_fn_out [reducible] [unfold 5] (f : M₁ →gm M₂) (i : I) : M₁ ((deg f)⁻¹ i) →lm M₂ i :=
f ↘ (to_right_inv (deg f) i)
infix ` ← `:101 := graded_hom_fn_out -- todo: change notation
infix ` ← `:max := graded_hom_fn_out -- todo: change notation
-- definition graded_hom_fn_out_rec (f : M₁ →gm M₂)
-- (P : Π{i j} (p : deg f i = j) (m : M₁ i) (n : M₂ j), Type)
-- (H : Πi m, P (right_inv (deg f) i) m (f ← i m)) {i j : I}
-- (p : deg f i = j) (m : M₁ i) (n : M₂ j) : P p m (f ↘ p m) :=
-- begin
-- revert i j p m n, refine equiv_rect (deg f)⁻¹ᵉ _ _, intro i,
-- refine eq.rec_to (right_inv (deg f) i) _,
-- intro m n, exact H i m
-- end
-- definition graded_hom_fn_rec (f : M₁ →gm M₂)
-- {P : Π{i j} (p : deg f i = j) (m : M₁ i) (n : M₂ j), Type}
-- (H : Πi m, P idp m (f i m)) ⦃i j : I⦄
-- (p : deg f i = j) (m : M₁ i) : P p m (f ↘ p m) :=
-- begin
-- induction p, apply H
-- end
-- definition graded_hom_fn_out_rec (f : M₁ →gm M₂)
-- {P : Π{i j} (p : deg f i = j) (m : M₁ i) (n : M₂ j), Type}
-- (H : Πi m, P idp m (f i m)) ⦃i : I⦄ (m : M₁ ((deg f)⁻¹ᵉ i)) :
-- P (right_inv (deg f) i) m (f ← i m) :=
-- graded_hom_fn_rec f H (right_inv (deg f) i) m
-- definition graded_hom_fn_out_rec_simple (f : M₁ →gm M₂)
-- {P : Π{j} (n : M₂ j), Type}
-- (H : Πi m, P (f i m)) ⦃i : I⦄ (m : M₁ ((deg f)⁻¹ᵉ i)) :
-- P (f ← i m) :=
-- graded_hom_fn_out_rec f H m
definition graded_hom.mk [constructor] (d : I ≃ I)
(fn : Πi, M₁ i →lm M₂ (d i)) : M₁ →gm M₂ :=
@ -85,21 +116,30 @@ definition graded_hom_mk_refl (d : I ≃ I)
(fn : Πi, M₁ i →lm M₂ (d i)) {i : I} (m : M₁ i) : graded_hom.mk d fn i m = fn i m :=
by reflexivity
lemma graded_hom_mk_out'_left_inv (d : I ≃ I)
lemma graded_hom_mk_out'_destruct (d : I ≃ I)
(fn : Πi, M₁ (d i) →lm M₂ i) {i : I} (m : M₁ (d i)) :
graded_hom.mk_out' d fn ↘ (left_inv d i) m = fn i m :=
begin
unfold [graded_hom.mk_out'],
apply ap (λx, fn i (cast x m)),
refine !ap_compose⁻¹ ⬝ ap02 _ _,
apply is_set.elim --we can also prove this in arbitrary types
apply is_set.elim --TODO: we can also prove this if I is not a set
end
lemma graded_hom_mk_out_right_inv (d : I ≃ I)
lemma graded_hom_mk_out_destruct (d : I ≃ I)
(fn : Πi, M₁ (d⁻¹ i) →lm M₂ i) {i : I} (m : M₁ (d⁻¹ i)) :
graded_hom.mk_out d fn ↘ (right_inv d i) m = fn i m :=
begin
rexact graded_hom_mk_out'_left_inv d⁻¹ᵉ fn m
rexact graded_hom_mk_out'_destruct d⁻¹ᵉ fn m
end
lemma graded_hom_mk_out_in_destruct (d₁ : I ≃ I) (d₂ : I ≃ I)
(fn : Πi, M₁ (d₁ i) →lm M₂ (d₂ i)) {i : I} (m : M₁ (d₁ i)) :
graded_hom.mk_out_in d₁ d₂ fn ↘ (ap d₂ (left_inv d₁ i)) m = fn i m :=
begin
unfold [graded_hom.mk_out_in],
rewrite [adj d₁, -ap_inv, - +ap_compose, ],
refine cast_fn_cast_square fn _ _ !con.left_inv m
end
definition graded_hom_eq_zero {f : M₁ →gm M₂} {i j k : I} {q : deg f i = j} {p : deg f i = k}
@ -107,16 +147,48 @@ definition graded_hom_eq_zero {f : M₁ →gm M₂} {i j k : I} {q : deg f i = j
have f ↘ p m = transport M₂ (q⁻¹ ⬝ p) (f ↘ q m), begin induction p, induction q, reflexivity end,
this ⬝ ap (transport M₂ (q⁻¹ ⬝ p)) r ⬝ tr_eq_of_pathover (apd (λi, 0) (q⁻¹ ⬝ p))
definition graded_hom_change_image {f : M₁ →gm M₂} {i j k : I} {m : M₂ k} (p : deg f i = k)
(q : deg f j = k) (h : image (f ↘ p) m) : image (f ↘ q) m :=
begin
have Σ(r : i = j), ap (deg f) r = p ⬝ q⁻¹,
from ⟨eq_of_fn_eq_fn (deg f) (p ⬝ q⁻¹), !ap_eq_of_fn_eq_fn'⟩,
induction this with r s, induction r, induction q, esimp at s, induction s, exact h
end
definition graded_hom_codom_rec {f : M₁ →gm M₂} {j : I} {P : Π⦃i⦄, deg f i = j → Type}
{i i' : I} (p : deg f i = j) (h : P p) (q : deg f i' = j) : P q :=
begin
have Σ(r : i = i'), ap (deg f) r = p ⬝ q⁻¹,
from ⟨eq_of_fn_eq_fn (deg f) (p ⬝ q⁻¹), !ap_eq_of_fn_eq_fn'⟩,
induction this with r s, induction r, induction q, esimp at s, induction s, exact h
end
variables {f' : M₂ →gm M₃} {f g h : M₁ →gm M₂}
definition graded_hom_compose [constructor] (f' : M₂ →gm M₃) (f : M₁ →gm M₂) : M₁ →gm M₃ :=
graded_hom.mk (deg f ⬝e deg f') (λi, f' (deg f i) ∘lm f i)
graded_hom.mk' (deg f ⬝e deg f') (λi j p, f' ↘ p ∘lm f i)
infixr ` ∘gm `:75 := graded_hom_compose
definition graded_hom_compose_fn (f' : M₂ →gm M₃) (f : M₁ →gm M₂) (i : I) (m : M₁ i) :
(f' ∘gm f) i m = f' (deg f i) (f i m) :=
proof idp qed
by reflexivity
definition graded_hom_compose_fn_ext (f' : M₂ →gm M₃) (f : M₁ →gm M₂) ⦃i j k : I⦄
(p : deg f i = j) (q : deg f' j = k) (r : (deg f ⬝e deg f') i = k) (s : ap (deg f') p ⬝ q = r)
(m : M₁ i) : ((f' ∘gm f) ↘ r) m = (f' ↘ q) (f ↘ p m) :=
by induction s; induction q; induction p; reflexivity
definition graded_hom_compose_fn_out (f' : M₂ →gm M₃) (f : M₁ →gm M₂) (i : I)
(m : M₁ ((deg f ⬝e deg f')⁻¹ᵉ i)) : (f' ∘gm f) ← i m = f' ← i (f ← ((deg f')⁻¹ᵉ i) m) :=
graded_hom_compose_fn_ext f' f _ _ _ idp m
-- the following composition might be useful if you want tight control over the paths to which f and f' are applied
definition graded_hom_compose_ext [constructor] (f' : M₂ →gm M₃) (f : M₁ →gm M₂)
(d : Π⦃i j⦄ (p : (deg f ⬝e deg f') i = j), I)
(pf : Π⦃i j⦄ (p : (deg f ⬝e deg f') i = j), deg f i = d p)
(pf' : Π⦃i j⦄ (p : (deg f ⬝e deg f') i = j), deg f' (d p) = j) : M₁ →gm M₃ :=
graded_hom.mk' (deg f ⬝e deg f') (λi j p, (f' ↘ (pf' p)) ∘lm (f ↘ (pf p)))
variable (M)
definition graded_hom_id [constructor] [refl] : M →gm M :=
@ -245,27 +317,27 @@ end
-- graded_hom.mk_out_in d₁⁻¹ᵉ d₂ _ :=
-- _
definition graded_hom_out_in_compose_out {d₁ d₂ d₃ : I ≃ I} (f₂ : Πi, M₂ (d₂ i) →lm M₃ (d₃ i))
(f₁ : Πi, M₁ (d₁⁻¹ i) →lm M₂ i) : graded_hom.mk_out_in d₂ d₃ f₂ ∘gm graded_hom.mk_out d₁ f₁ ~gm
graded_hom.mk_out_in (d₂ ⬝e d₁⁻¹ᵉ) d₃ (λi, f₂ i ∘lm (f₁ (d₂ i))) :=
begin
apply graded_homotopy.mk, intro i m, exact sorry
end
-- definition graded_hom_out_in_compose_out {d₁ d₂ d₃ : I ≃ I} (f₂ : Πi, M₂ (d₂ i) →lm M₃ (d₃ i))
-- (f₁ : Πi, M₁ (d₁⁻¹ i) →lm M₂ i) : graded_hom.mk_out_in d₂ d₃ f₂ ∘gm graded_hom.mk_out d₁ f₁ ~gm
-- graded_hom.mk_out_in (d₂ ⬝e d₁⁻¹ᵉ) d₃ (λi, f₂ i ∘lm (f₁ (d₂ i))) :=
-- begin
-- apply graded_homotopy.mk, intro i m, exact sorry
-- end
definition graded_hom_out_in_rfl {d₁ d₂ : I ≃ I} (f : Πi, M₁ i →lm M₂ (d₂ i))
(p : Πi, d₁ i = i) :
graded_hom.mk_out_in d₁ d₂ (λi, sorry) ~gm graded_hom.mk d₂ f :=
begin
apply graded_homotopy.mk, intro i m, exact sorry
end
-- definition graded_hom_out_in_rfl {d₁ d₂ : I ≃ I} (f : Πi, M₁ i →lm M₂ (d₂ i))
-- (p : Πi, d₁ i = i) :
-- graded_hom.mk_out_in d₁ d₂ (λi, sorry) ~gm graded_hom.mk d₂ f :=
-- begin
-- apply graded_homotopy.mk, intro i m, exact sorry
-- end
definition graded_homotopy.trans (h₁ : f ~gm g) (h₂ : g ~gm h) : f ~gm h :=
begin
exact sorry
end
-- definition graded_homotopy.trans (h₁ : f ~gm g) (h₂ : g ~gm h) : f ~gm h :=
-- begin
-- exact sorry
-- end
-- postfix `⁻¹ᵍᵐ`:(max + 1) := graded_iso.symm
infixl ` ⬝gm `:75 := graded_homotopy.trans
--infixl ` ⬝gm `:75 := graded_homotopy.trans
-- infixl ` ⬝gmp `:75 := graded_iso.trans_eq
-- infixl ` ⬝pgm `:75 := graded_iso.eq_trans
@ -361,11 +433,52 @@ definition graded_hom_lift [constructor] {S : Πi, submodule_rel (M₂ i)}
(h : Π(i : I) (m : M₁ i), S (deg φ i) (φ i m)) : M₁ →gm graded_submodule S :=
graded_hom.mk (deg φ) (λi, hom_lift (φ i) (h i))
definition graded_submodule_functor [constructor] {S : Πi, submodule_rel (M₁ i)}
{T : Πi, submodule_rel (M₂ i)} (φ : M₁ →gm M₂)
(h : Π(i : I) (m : M₁ i), S i m → T (deg φ i) (φ i m)) :
graded_submodule S →gm graded_submodule T :=
graded_hom.mk (deg φ) (λi, submodule_functor (φ i) (h i))
definition graded_image (f : M₁ →gm M₂) : graded_module R I :=
λi, image_module (f ← i)
lemma graded_image_lift_lemma (f : M₁ →gm M₂) {i j: I} (p : deg f i = j) (m : M₁ i) :
image (f ← j) (f ↘ p m) :=
graded_hom_change_image p (right_inv (deg f) j) (image.mk m idp)
definition graded_image_lift [constructor] (f : M₁ →gm M₂) : M₁ →gm graded_image f :=
graded_hom.mk_out (deg f) (λi, image_lift (f ← i))
graded_hom.mk' (deg f) (λi j p, hom_lift (f ↘ p) (graded_image_lift_lemma f p))
definition graded_image_lift_destruct (f : M₁ →gm M₂) {i : I}
(m : M₁ ((deg f)⁻¹ᵉ i)) : graded_image_lift f ← i m = image_lift (f ← i) m :=
subtype_eq idp
definition graded_image.rec {f : M₁ →gm M₂} {i : I} {P : graded_image f (deg f i) → Type}
[h : Πx, is_prop (P x)] (H : Πm, P (graded_image_lift f i m)) : Πm, P m :=
begin
assert H₂ : Πi' (p : deg f i' = deg f i) (m : M₁ i'),
P ⟨f ↘ p m, graded_hom_change_image p _ (image.mk m idp)⟩,
{ refine eq.rec_equiv_symm (deg f) _, intro m,
refine transport P _ (H m), apply subtype_eq, reflexivity },
refine @total_image.rec _ _ _ _ h _, intro m,
refine transport P _ (H₂ _ (right_inv (deg f) (deg f i)) m),
apply subtype_eq, reflexivity
end
definition image_graded_image_lift {f : M₁ →gm M₂} {i j : I} (p : deg f i = j)
(m : graded_image f j)
(h : image (f ↘ p) m.1) : image (graded_image_lift f ↘ p) m :=
begin
induction p,
revert m h, refine total_image.rec _, intro m h,
induction h with n q, refine image.mk n (subtype_eq q)
end
lemma is_surjective_graded_image_lift ⦃x y⦄ (f : M₁ →gm M₂)
(p : deg f x = y) : is_surjective (graded_image_lift f ↘ p) :=
begin
intro m, apply image_graded_image_lift, exact graded_hom_change_image (right_inv (deg f) y) _ m.2
end
definition graded_image_elim [constructor] {f : M₁ →gm M₂} (g : M₁ →gm M₃)
(h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
@ -374,85 +487,103 @@ begin
apply graded_hom.mk_out_in (deg f) (deg g),
intro i,
apply image_elim (g ↘ (ap (deg g) (to_left_inv (deg f) i))),
intro m p,
refine graded_hom_eq_zero m (h _),
exact graded_hom_eq_zero m p
exact abstract begin
intro m p,
refine graded_hom_eq_zero m (h _),
exact graded_hom_eq_zero m p end end
end
definition is_surjective_graded_image_lift ⦃x y⦄ (f : M₁ →gm M₂)
(p : deg f x = y) : is_surjective (graded_image_lift f ↘ p) :=
lemma graded_image_elim_destruct {f : M₁ →gm M₂} {g : M₁ →gm M₃}
(h : Π⦃i m⦄, f i m = 0 → g i m = 0) {i j k : I}
(p' : deg f i = j) (p : deg g ((deg f)⁻¹ᵉ j) = k)
(q : deg g i = k) (r : ap (deg g) (to_left_inv (deg f) i) ⬝ q = ap ((deg f)⁻¹ᵉ ⬝e deg g) p' ⬝ p)
(m : M₁ i) : graded_image_elim g h ↘ p (graded_image_lift f ↘ p' m) =
g ↘ q m :=
begin
exact sorry
revert i j p' k p q r m,
refine equiv_rect (deg f ⬝e (deg f)⁻¹ᵉ) _ _,
intro i, refine eq.rec_grading _ (deg f) (right_inv (deg f) (deg f i)) _,
intro k p q r m,
assert r' : q = p,
{ refine cancel_left _ (r ⬝ whisker_right _ _), refine !ap_compose ⬝ ap02 (deg g) _,
exact !adj_inv⁻¹ },
induction r', clear r,
revert k q m, refine eq.rec_to (ap (deg g) (to_left_inv (deg f) i)) _, intro m,
refine graded_hom_mk_out_in_destruct (deg f) (deg g) _ (graded_image_lift f ← (deg f i) m) ⬝ _,
refine ap (image_elim _ _) !graded_image_lift_destruct ⬝ _, reflexivity
end
definition graded_image' (f : M₁ →gm M₂) : graded_module R I :=
λi, image_module (f i)
/- alternative (easier) definition of graded_image with "wrong" grading -/
definition graded_image'_lift [constructor] (f : M₁ →gm M₂) : M₁ →gm graded_image' f :=
graded_hom.mk erfl (λi, image_lift (f i))
-- definition graded_image' (f : M₁ →gm M₂) : graded_module R I :=
-- λi, image_module (f i)
definition graded_image'_elim [constructor] {f : M₁ →gm M₂} (g : M₁ →gm M₃)
(h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
graded_image' f →gm M₃ :=
begin
apply graded_hom.mk (deg g),
intro i,
apply image_elim (g i),
intro m p, exact h p
end
-- definition graded_image'_lift [constructor] (f : M₁ →gm M₂) : M₁ →gm graded_image' f :=
-- graded_hom.mk erfl (λi, image_lift (f i))
theorem graded_image'_elim_compute {f : M₁ →gm M₂} {g : M₁ →gm M₃}
(h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
graded_image'_elim g h ∘gm graded_image'_lift f ~gm g :=
begin
apply graded_homotopy.mk,
intro i m, exact sorry --reflexivity
end
-- definition graded_image'_elim [constructor] {f : M₁ →gm M₂} (g : M₁ →gm M₃)
-- (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
-- graded_image' f →gm M₃ :=
-- begin
-- apply graded_hom.mk (deg g),
-- intro i,
-- apply image_elim (g i),
-- intro m p, exact h p
-- end
theorem graded_image_elim_compute {f : M₁ →gm M₂} {g : M₁ →gm M₃}
(h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
graded_image_elim g h ∘gm graded_image_lift f ~gm g :=
begin
refine _ ⬝gm graded_image'_elim_compute h,
esimp, exact sorry
-- refine graded_hom_out_in_compose_out _ _ ⬝gm _, exact sorry
-- -- apply graded_homotopy.mk,
-- -- intro i m,
end
variables {α β : I ≃ I}
definition gen_image (f : M₁ →gm M₂) (p : Πi, deg f (α i) = β i) : graded_module R I :=
λi, image_module (f ↘ (p i))
-- theorem graded_image'_elim_compute {f : M₁ →gm M₂} {g : M₁ →gm M₃}
-- (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
-- graded_image'_elim g h ∘gm graded_image'_lift f ~gm g :=
-- begin
-- apply graded_homotopy.mk,
-- intro i m, exact sorry --reflexivity
-- end
definition gen_image_lift [constructor] (f : M₁ →gm M₂) (p : Πi, deg f (α i) = β i) : M₁ →gm gen_image f p :=
graded_hom.mk_out α⁻¹ᵉ (λi, image_lift (f ↘ (p i)))
-- theorem graded_image_elim_compute {f : M₁ →gm M₂} {g : M₁ →gm M₃}
-- (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
-- graded_image_elim g h ∘gm graded_image_lift f ~gm g :=
-- begin
-- refine _ ⬝gm graded_image'_elim_compute h,
-- esimp, exact sorry
-- -- refine graded_hom_out_in_compose_out _ _ ⬝gm _, exact sorry
-- -- -- apply graded_homotopy.mk,
-- -- -- intro i m,
-- end
definition gen_image_elim [constructor] {f : M₁ →gm M₂} (p : Πi, deg f (α i) = β i) (g : M₁ →gm M₃)
(h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
gen_image f p →gm M₃ :=
begin
apply graded_hom.mk_out_in α⁻¹ᵉ (deg g),
intro i,
apply image_elim (g ↘ (ap (deg g) (to_right_inv α i))),
intro m p,
refine graded_hom_eq_zero m (h _),
exact graded_hom_eq_zero m p
end
-- variables {α β : I ≃ I}
-- definition gen_image (f : M₁ →gm M₂) (p : Πi, deg f (α i) = β i) : graded_module R I :=
-- λi, image_module (f ↘ (p i))
theorem gen_image_elim_compute {f : M₁ →gm M₂} {p : deg f ∘ α ~ β} {g : M₁ →gm M₃}
(h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
gen_image_elim p g h ∘gm gen_image_lift f p ~gm g :=
begin
-- induction β with β βe, esimp at *, induction p using homotopy.rec_on_idp,
assert q : β ⬝e (deg f)⁻¹ᵉ = α,
{ apply equiv_eq, intro i, apply inv_eq_of_eq, exact (p i)⁻¹ },
induction q,
-- unfold [gen_image_elim, gen_image_lift],
-- definition gen_image_lift [constructor] (f : M₁ →gm M₂) (p : Πi, deg f (α i) = β i) : M₁ →gm gen_image f p :=
-- graded_hom.mk_out α⁻¹ᵉ (λi, image_lift (f ↘ (p i)))
-- induction (is_prop.elim (λi, to_right_inv (deg f) (β i)) p),
-- apply graded_homotopy.mk,
-- intro i m, reflexivity
exact sorry
end
-- definition gen_image_elim [constructor] {f : M₁ →gm M₂} (p : Πi, deg f (α i) = β i) (g : M₁ →gm M₃)
-- (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
-- gen_image f p →gm M₃ :=
-- begin
-- apply graded_hom.mk_out_in α⁻¹ᵉ (deg g),
-- intro i,
-- apply image_elim (g ↘ (ap (deg g) (to_right_inv α i))),
-- intro m p,
-- refine graded_hom_eq_zero m (h _),
-- exact graded_hom_eq_zero m p
-- end
-- theorem gen_image_elim_compute {f : M₁ →gm M₂} {p : deg f ∘ α ~ β} {g : M₁ →gm M₃}
-- (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
-- gen_image_elim p g h ∘gm gen_image_lift f p ~gm g :=
-- begin
-- -- induction β with β βe, esimp at *, induction p using homotopy.rec_on_idp,
-- assert q : β ⬝e (deg f)⁻¹ᵉ = α,
-- { apply equiv_eq, intro i, apply inv_eq_of_eq, exact (p i)⁻¹ },
-- induction q,
-- -- unfold [gen_image_elim, gen_image_lift],
-- -- induction (is_prop.elim (λi, to_right_inv (deg f) (β i)) p),
-- -- apply graded_homotopy.mk,
-- -- intro i m, reflexivity
-- exact sorry
-- end
definition graded_kernel (f : M₁ →gm M₂) : graded_module R I :=
λi, kernel_module (f i)
@ -464,8 +595,21 @@ definition graded_quotient_map [constructor] (S : Πi, submodule_rel (M i)) :
M →gm graded_quotient S :=
graded_hom.mk erfl (λi, quotient_map (S i))
definition graded_quotient_elim [constructor] {S : Πi, submodule_rel (M i)} (φ : M →gm M₂)
(H : Πi ⦃m⦄, S i m → φ i m = 0) : graded_quotient S →gm M₂ :=
graded_hom.mk (deg φ) (λi, quotient_elim (φ i) (H i))
definition graded_homology (g : M₂ →gm M₃) (f : M₁ →gm M₂) : graded_module R I :=
λi, homology (g i) (f ← i)
graded_quotient (λi, submodule_rel_submodule (kernel_rel (g i)) (image_rel (f ← i)))
-- the two reasonable definitions of graded_homology are definitionally equal
example (g : M₂ →gm M₃) (f : M₁ →gm M₂) :
(λi, homology (g i) (f ← i)) =
graded_quotient (λi, submodule_rel_submodule (kernel_rel (g i)) (image_rel (f ← i))) := idp
definition graded_homology.mk (g : M₂ →gm M₃) (f : M₁ →gm M₂) {i : I} (m : M₂ i) (h : g i m = 0) :
graded_homology g f i :=
homology.mk _ m h
definition graded_homology_intro [constructor] (g : M₂ →gm M₃) (f : M₁ →gm M₂) :
graded_kernel g →gm graded_homology g f :=
@ -475,6 +619,14 @@ definition graded_homology_elim {g : M₂ →gm M₃} {f : M₁ →gm M₂} (h :
(H : compose_constant h f) : graded_homology g f →gm M :=
graded_hom.mk (deg h) (λi, homology_elim (h i) (H _ _))
open trunc
definition image_of_graded_homology_intro_eq_zero {g : M₂ →gm M₃} {f : M₁ →gm M₂}
⦃i j : I⦄ (p : deg f i = j) (m : graded_kernel g j) (H : graded_homology_intro g f j m = 0) :
image (f ↘ p) m.1 :=
begin
induction p, exact graded_hom_change_image _ _ (rel_of_quotient_map_eq_zero m H)
end
definition is_exact_gmod (f : M₁ →gm M₂) (f' : M₂ →gm M₃) : Type :=
Π⦃i j k⦄ (p : deg f i = j) (q : deg f' j = k), is_exact_mod (f ↘ p) (f' ↘ q)
@ -486,11 +638,9 @@ begin intro i j k p q; induction p; induction q; split, apply h₁, apply h₂ e
definition gmod_im_in_ker (h : is_exact_gmod f f') : compose_constant f' f :=
λi j k p q, is_exact.im_in_ker (h p q)
-- definition is_exact_gmod_mk_mk_out' {d₁ d₂ : I ≃ I} (fn₁ : Πi, M₁ i →lm M₂ (d₁ i))
-- (fn₂ : Πi, M₂ (d₂ i) →lm M₃ i) (H : Πi, is_exact_mod (fn₁ i) _) : is_exact_gmod (graded_hom.mk d₁ fn₁) (graded_hom.mk_out' d₂ fn₂) :=
-- begin
-- end
definition gmod_ker_in_im (h : is_exact_gmod f f') ⦃i : I⦄ (m : M₂ i) (p : f' i m = 0) :
image (f ← i) m :=
is_exact.ker_in_im (h (right_inv (deg f) i) idp) m p
end left_module

7
algebra/left_module.hlean
View file

@ -234,6 +234,9 @@ section
definition to_respect_smul (a : R) (x : M₁) : φ (a • x) = a • (φ x) :=
respect_smul R φ a x
definition to_respect_sub (x y : M₁) : φ (x - y) = φ x - φ y :=
respect_sub φ x y
definition is_embedding_of_homomorphism /- φ -/ (H : Π{x}, φ x = 0 → x = 0) : is_embedding φ :=
is_embedding_of_is_add_hom φ @H
@ -391,6 +394,10 @@ end
definition is_exact_mod (f : M₁ →lm M₂) (f' : M₂ →lm M₃) : Type :=
@is_exact M₁ M₂ M₃ (homomorphism_fn f) (homomorphism_fn f')
definition is_exact_mod.mk {f : M₁ →lm M₂} {f' : M₂ →lm M₃}
(h₁ : Πm, f' (f m) = 0) (h₂ : Πm, f' m = 0 → image f m) : is_exact_mod f f' :=
is_exact.mk h₁ h₂
structure short_exact_mod (A B C : LeftModule R) :=
(f : A →lm B)
(g : B →lm C)

155
algebra/module_exact_couple.hlean
View file

@ -1,10 +1,13 @@
/- Exact couples of graded (left-) R-modules. -/
/- Exact couples of graded (left-) R-modules. This file includes:
- Constructing exact couples from sequences of maps
- Deriving an exact couple
- The convergence theorem for exact couples -/
-- Author: Floris van Doorn
import .graded ..homotopy.spectrum .product_group
open algebra is_trunc left_module is_equiv equiv eq function nat
open algebra is_trunc left_module is_equiv equiv eq function nat sigma sigma.ops set_quotient
/- exact couples -/
@ -17,9 +20,10 @@ namespace left_module
(jk : is_exact_gmod j k)
(ki : is_exact_gmod k i)
open exact_couple
namespace derived_couple
section
open exact_couple
parameters {R : Ring} {I : Set} (X : exact_couple R I)
local abbreviation D := D X
@ -42,7 +46,7 @@ namespace left_module
!is_contr_image_module
definition i' : D' →gm D' :=
graded_image_lift i ∘gm graded_submodule_incl _
graded_image_lift i ∘gm graded_submodule_incl (λx, image_rel (i ← x))
-- degree i + 0
lemma is_surjective_i' {x y : I} (p : deg i' x = y)
@ -93,70 +97,126 @@ namespace left_module
graded_image_elim (graded_homology_intro d d ∘gm graded_hom_lift j j_lemma1) j_lemma2
-- degree deg j - deg i
lemma k_lemma1 ⦃x : I⦄ (m : E x) : image (i ← (deg k x)) (k x m) :=
begin
exact sorry
end
-- mk_out_in (deg f) (deg g)
lemma k_lemma2 : compose_constant (graded_hom_lift k k_lemma1 : E →gm D') d :=
lemma k_lemma1 ⦃x : I⦄ (m : E x) (p : d x m = 0) : image (i ← (deg k x)) (k x m) :=
gmod_ker_in_im (exact_couple.ij X) (k x m) p
definition k₂ : graded_kernel d →gm D' := graded_submodule_functor k k_lemma1
lemma k_lemma2 ⦃x : I⦄ (m : E x) (h₁ : kernel_rel (d x) m) (h₂ : image (d ← x) m) :
k₂ x ⟨m, h₁⟩ = 0 :=
begin
-- apply compose_constant.mk, intro x m,
-- rewrite [graded_hom_compose_fn],
-- refine ap (graded_hom_fn (graded_image_lift i) (deg k (deg d x))) _ ⬝ !to_respect_zero,
-- exact compose_constant.elim (gmod_im_in_ker jk) (deg k x) (k x m)
exact sorry
assert H₁ : Π⦃x' y z w : I⦄ (p : deg k x' = y) (q : deg j y = z) (r : deg k z = w) (n : E x'),
k ↘ r (j ↘ q (k ↘ p n)) = 0,
{ intros, exact gmod_im_in_ker (exact_couple.jk X) q r (k ↘ p n) },
induction h₂ with n p,
assert H₂ : k x m = 0,
{ rewrite [-p], refine ap (k x) (graded_hom_compose_fn_out j k x n) ⬝ _, apply H₁ },
exact subtype_eq H₂
end
definition k' : E' →gm D' :=
graded_homology_elim (graded_hom_lift k k_lemma1) k_lemma2
graded_quotient_elim (graded_submodule_functor k k_lemma1)
(by intro x m h; exact k_lemma2 m.1 m.2 h)
definition i'_eq ⦃x : I⦄ (m : D x) (h : image (i ← x) m) : (i' x ⟨m, h⟩).1 = i x m :=
by reflexivity
definition k'_eq ⦃x : I⦄ (m : E x) (h : d x m = 0) : (k' x (class_of ⟨m, h⟩)).1 = k x m :=
by reflexivity
lemma j'_eq {x : I} (m : D x) : j' ↘ (ap (deg j) (left_inv (deg i) x)) (graded_image_lift i x m) =
class_of (graded_hom_lift j proof j_lemma1 qed x m) :=
begin
refine graded_image_elim_destruct _ _ _ idp _ m,
apply is_set.elim,
end
definition deg_i' : deg i' ~ deg i := by reflexivity
definition deg_j' : deg j' ~ deg j ∘ (deg i)⁻¹ := by reflexivity
definition deg_k' : deg k' ~ deg k := by reflexivity
open group
lemma i'j' : is_exact_gmod i' j' :=
begin
apply is_exact_gmod.mk,
{ intro x, refine total_image.rec _, intro m, exact sorry
-- exact calc
-- j' (deg i' x) (i' x ⟨(i ← x) m, image.mk m idp⟩)
-- = j' (deg i' x) (graded_image_lift i x ((i ← x) m)) : idp
-- ... = graded_homology_intro d d (deg j ((deg i)⁻¹ᵉ (deg i x)))
-- (graded_hom_lift j j_lemma1 ((deg i)⁻¹ᵉ (deg i x))
-- (i ↘ (!to_right_inv ⬝ !to_left_inv⁻¹) m)) : _
-- ... = graded_homology_intro d d (deg j ((deg i)⁻¹ᵉ (deg i x)))
-- (graded_hom_lift j j_lemma1 ((deg i)⁻¹ᵉ (deg i x))
-- (i ↘ (!to_right_inv ⬝ !to_left_inv⁻¹) m)) : _
-- ... = 0 : _
},
{ exact sorry }
intro x, refine equiv_rect (deg i) _ _,
intros y z p q, revert z q x p,
refine eq.rec_grading (deg i ⬝e deg j') (deg j) (ap (deg j) (left_inv (deg i) y)) _,
intro x, revert y, refine eq.rec_equiv (deg i) _,
apply transport (λx, is_exact_mod x _) (idpath (i' x)),
apply transport (λx, is_exact_mod _ (j' ↘ (ap (deg j) (left_inv (deg i) x)))) (idpath x),
apply is_exact_mod.mk,
{ revert x, refine equiv_rect (deg i) _ _, intro x,
refine graded_image.rec _, intro m,
transitivity j' ↘ _ (graded_image_lift i (deg i x) (i x m)),
apply ap (λx, j' ↘ _ x), apply subtype_eq, apply i'_eq,
refine !j'_eq ⬝ _,
apply ap class_of, apply subtype_eq, exact is_exact.im_in_ker (exact_couple.ij X idp idp) m },
{ revert x, refine equiv_rect (deg k) _ _, intro x,
refine graded_image.rec _, intro m p,
assert q : graded_homology_intro d d (deg j (deg k x))
(graded_hom_lift j j_lemma1 (deg k x) m) = 0,
{ exact !j'_eq⁻¹ ⬝ p },
note q2 := image_of_graded_homology_intro_eq_zero idp (graded_hom_lift j _ _ m) q,
induction q2 with n r,
assert s : j (deg k x) (m - k x n) = 0,
{ refine respect_sub (j (deg k x)) m (k x n) ⬝ _,
refine ap (sub _) r ⬝ _, apply sub_self },
assert t : trunctype.carrier (image (i ← (deg k x)) (m - k x n)),
{ exact is_exact.ker_in_im (exact_couple.ij X _ _) _ s },
refine image.mk ⟨m - k x n, t⟩ _,
apply subtype_eq, refine !i'_eq ⬝ !to_respect_sub ⬝ _,
refine ap (sub _) _ ⬝ !sub_zero,
apply is_exact.im_in_ker (exact_couple.ki X _ _) }
end
lemma j'k' : is_exact_gmod j' k' :=
begin
apply is_exact_gmod.mk,
{ exact sorry },
{ exact sorry }
refine equiv_rect (deg i) _ _,
intros x y z p, revert y p z,
refine eq.rec_grading (deg i ⬝e deg j') (deg j) (ap (deg j) (left_inv (deg i) x)) _,
intro z q, induction q,
apply is_exact_mod.mk,
{ refine graded_image.rec _, intro m,
refine ap (k' _) (j'_eq m) ⬝ _,
apply subtype_eq,
refine k'_eq _ _ ⬝ _,
exact is_exact.im_in_ker (exact_couple.jk X idp idp) m },
{ intro m p, induction m using set_quotient.rec_prop with m,
induction m with m h, note q := (k'_eq m h)⁻¹ ⬝ ap pr1 p,
induction is_exact.ker_in_im (exact_couple.jk X idp idp) m q with n r,
apply image.mk (graded_image_lift i x n),
refine !j'_eq ⬝ _,
apply ap class_of, apply subtype_eq, exact r }
end
lemma k'i' : is_exact_gmod k' i' :=
begin
apply is_exact_gmod.mk,
{ intro x m, exact sorry },
{ exact sorry }
{ intro x m, induction m using set_quotient.rec_prop with m,
cases m with m p, apply subtype_eq,
change i (deg k x) (k x m) = 0,
exact is_exact.im_in_ker (exact_couple.ki X idp idp) m },
{ intro x m, induction m with m h, intro p,
have i (deg k x) m = 0, from ap pr1 p,
induction is_exact.ker_in_im (exact_couple.ki X idp idp) m this with n q,
have j (deg k x) m = 0, from @(is_exact.im_in_ker2 (exact_couple.ij X _ _)) m h,
have d x n = 0, from ap (j (deg k x)) q ⬝ this,
exact image.mk (class_of ⟨n, this⟩) (subtype_eq q) }
end
end
end derived_couple
section
open derived_couple exact_couple
open derived_couple
definition derived_couple [constructor] {R : Ring} {I : Set}
(X : exact_couple R I) : exact_couple R I :=
⦃exact_couple, D := D' X, E := E' X, i := i' X, j := j' X, k := k' X,
ij := i'j' X, jk := j'k' X, ki := k'i' X⦄
/- if an exact couple is bounded, we can prove the convergence theorem for it -/
structure is_bounded {R : Ring} {I : Set} (X : exact_couple R I) : Type :=
mk' :: (B B' : I → ℕ)
(Dub : Π⦃x y⦄ ⦃s : ℕ⦄, (deg (i X))^[s] x = y → B x ≤ s → is_contr (D X y))
@ -166,7 +226,7 @@ namespace left_module
(deg_ij_commute : hsquare (deg (j X)) (deg (j X)) (deg (i X)) (deg (i X)))
/- Note: Elb proves Dlb for some bound B', but we want tight control over when B' = 0 -/
definition is_bounded.mk [constructor] {R : Ring} {I : Set} {X : exact_couple R I}
protected definition is_bounded.mk [constructor] {R : Ring} {I : Set} {X : exact_couple R I}
(B B' B'' : I → ℕ)
(Dub : Π⦃x : I⦄ ⦃s : ℕ⦄, B x ≤ s → is_contr (D X ((deg (i X))^[s] x)))
(Dlb : Π⦃x : I⦄ ⦃s : ℕ⦄, B' x ≤ s → is_surjective (i X (((deg (i X))⁻¹ᵉ^[s + 1] x))))
@ -184,6 +244,9 @@ namespace left_module
{ assumption }
end
namespace convergence_theorem
section
open is_bounded
parameters {R : Ring} {I : Set} (X : exact_couple R I) (HH : is_bounded X)
@ -213,7 +276,7 @@ namespace left_module
exact Dub !deg_iterate_ik_commute (le.trans !le_max_left h)
end
-- we start counting pages at 0, not at 2.
-- we start counting pages at 0
definition page (r : ℕ) : exact_couple R I :=
iterate derived_couple r X
@ -283,7 +346,8 @@ namespace left_module
begin
revert x y z s H p q, induction r with r IH: intro x y z s H p q,
{ exact Dlb p q H },
-- the following is a start of the proof that i is surjective from the contractibility of E
/- the following is a start of the proof that i is surjective using that E is contractible (but this
makes the bound 1 higher than necessary -/
-- induction p, change is_surjective (i X x),
-- apply @(is_surjective_of_is_exact_of_is_contr (exact_couple.ij X idp idp)),
-- refine Elb _ H,
@ -304,6 +368,7 @@ namespace left_module
reflexivity
end
/- the infinity pages of E and D -/
definition Einf : graded_module R I :=
λx, E (page (B3 x)) x
@ -363,6 +428,7 @@ namespace left_module
{ apply ij (page (r n)) }
end
/- the convergence theorem is a combination of the following three results -/
definition short_exact_mod_infpage (n : ℕ) :
short_exact_mod (Einfdiag n) (Dinfdiag n) (Dinfdiag (n+1)) :=
begin
@ -375,11 +441,16 @@ namespace left_module
definition Dinfdiag0 (bound_zero : B' (deg (k X) x) = 0) : Dinfdiag 0 ≃lm D X (deg (k X) x) :=
Dinfstable (le_of_eq bound_zero) idp
definition Dinfdiag_stable {s : ℕ} (h : B (deg (k X) x) ≤ s) : is_contr (Dinfdiag s) :=
lemma Dinfdiag_stable {s : ℕ} (h : B (deg (k X) x) ≤ s) : is_contr (Dinfdiag s) :=
is_contr_D _ _ (Dub !deg_iterate_ik_commute h)
end
end convergence_theorem
-- open convergence_theorem
-- print axioms short_exact_mod_infpage
-- print axioms Dinfdiag0
-- print axioms Dinfdiag_stable
end left_module
open left_module
@ -486,7 +557,7 @@ namespace spectrum
revert t q, refine eq.rec_equiv (add_right_action (- 1)) _,
induction p using eq.rec_symm,
apply is_exact_homotopy homotopy.rfl,
{ symmetry, intro m, exact graded_hom_mk_out_right_inv deg_j_seq_inv⁻¹ᵉ fn_j_sequence m },
{ symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ fn_j_sequence },
rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (m, 2)),
end
@ -496,7 +567,7 @@ namespace spectrum
revert x y p, refine eq.rec_right_inv (deg j_sequence) _,
intro x, induction x with n s,
apply is_exact_homotopy,
{ symmetry, intro m, exact graded_hom_mk_out_right_inv deg_j_seq_inv⁻¹ᵉ fn_j_sequence m },
{ symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ fn_j_sequence },
{ reflexivity },
rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (n, 1)),
end

27
algebra/submodule.hlean
View file

@ -5,7 +5,7 @@
import .left_module .quotient_group
open algebra eq group sigma is_trunc function trunc equiv is_equiv
open algebra eq group sigma sigma.ops is_trunc function trunc equiv is_equiv
-- move to subgroup
attribute normal_subgroup_rel._trans_of_to_subgroup_rel [unfold 2]
@ -122,6 +122,10 @@ lm_homomorphism_of_group_homomorphism (hom_lift (group_homomorphism_of_lm_homomo
intro r g, exact subtype_eq (to_respect_smul φ r g)
end
definition submodule_functor [constructor] {S : submodule_rel M₁} {K : submodule_rel M₂}
(φ : M₁ →lm M₂) (h : Π (m : M₁), S m → K (φ m)) : submodule S →lm submodule K :=
hom_lift (φ ∘lm submodule_incl S) (by intro m; exact h m.1 m.2)
definition hom_lift_compose {K : submodule_rel M₃}
(φ : M₂ →lm M₃) (h : Π (m : M₂), K (φ m)) (ψ : M₁ →lm M₂) :
hom_lift φ h ∘lm ψ ~ hom_lift (φ ∘lm ψ) proof (λm, h (ψ m)) qed :=
@ -210,6 +214,9 @@ lm_homomorphism_of_group_homomorphism (ab_qg_map _) (λr g, idp)
definition quotient_map_eq_zero (m : M) (H : S m) : quotient_map S m = 0 :=
qg_map_eq_one _ H
definition rel_of_quotient_map_eq_zero (m : M) (H : quotient_map S m = 0) : S m :=
rel_of_qg_map_eq_one m H
definition quotient_elim [constructor] (φ : M →lm M₂) (H : Π⦃m⦄, S m → φ m = 0) :
quotient_module S →lm M₂ :=
lm_homomorphism_of_group_homomorphism
@ -286,6 +293,12 @@ begin
reflexivity
end
-- definition image_elim_hom_lift (ψ : M →lm M₂) (h : Π⦃g⦄, φ g = 0 → θ g = 0) :
-- image_elim θ h ∘lm hom_lift ψ _ ~ _ :=
-- begin
-- reflexivity
-- end
definition is_contr_image_module [instance] (φ : M₁ →lm M₂) [is_contr M₂] :
is_contr (image_module φ) :=
!is_contr_submodule
@ -332,19 +345,19 @@ submodule_isomorphism _ (kernel_rel_full φ)
definition homology (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) : LeftModule R :=
@quotient_module R (submodule (kernel_rel ψ)) (submodule_rel_submodule _ (image_rel φ))
definition homology.mk (m : M₂) (h : ψ m = 0) : homology ψ φ :=
definition homology.mk (φ : M₁ →lm M₂) (m : M₂) (h : ψ m = 0) : homology ψ φ :=
quotient_map _ ⟨m, h⟩
definition homology_eq0 {m : M₂} {hm : ψ m = 0} (h : image φ m) :
homology.mk m hm = 0 :> homology ψ φ :=
homology.mk φ m hm = 0 :=
ab_qg_map_eq_one _ h
definition homology_eq0' {m : M₂} {hm : ψ m = 0} (h : image φ m):
homology.mk m hm = homology.mk 0 (to_respect_zero ψ) :> homology ψ φ :=
homology.mk φ m hm = homology.mk φ 0 (to_respect_zero ψ) :=
ab_qg_map_eq_one _ h
definition homology_eq {m n : M₂} {hm : ψ m = 0} {hn : ψ n = 0} (h : image φ (m - n)) :
homology.mk m hm = homology.mk n hn :> homology ψ φ :=
homology.mk φ m hm = homology.mk φ n hn :=
eq_of_sub_eq_zero (homology_eq0 h)
definition homology_elim [constructor] (θ : M₂ →lm M) (H : Πm, θ (φ m) = 0) :
@ -362,8 +375,8 @@ definition is_contr_homology [instance] (ψ : M₂ →lm M₃) (φ : M₁ →lm
is_contr (homology ψ φ) :=
begin apply @is_contr_quotient_module end
definition homology_isomorphism [constructor] (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) [is_contr M₁] [is_contr M₃] :
homology ψ φ ≃lm M₂ :=
definition homology_isomorphism [constructor] (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂)
[is_contr M₁] [is_contr M₃] : homology ψ φ ≃lm M₂ :=
quotient_module_isomorphism _ (submodule_rel_submodule_trivial (image_rel_trivial φ)) ⬝lm
!kernel_module_isomorphism

62
move_to_lib.hlean
View file

@ -29,6 +29,12 @@ definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
(H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g :=
is_exact.mk H₁ H₂
definition is_exact.im_in_ker2 {A B : Type} {C : Set*} {f : A → B} {g : B → C} (H : is_exact f g)
{b : B} (h : image f b) : g b = pt :=
begin
induction h with a p, exact ap g p⁻¹ ⬝ is_exact.im_in_ker H a
end
-- TO DO: give less univalency proof
definition is_exact_homotopy {A B : Type} {C : Type*} {f f' : A → B} {g g' : B → C}
(p : f ~ f') (q : g ~ g') (H : is_exact f g) : is_exact f' g' :=
@ -99,7 +105,7 @@ end algebra
namespace eq
definition eq.rec_to {A : Type} {a₀ : A} {P : Π⦃a₁⦄, a₀ = a₁ → Type}
{a₁ : A} (p₀ : a₀ = a₁) (H : P p₀) {a₂ : A} (p : a₀ = a₂) : P p :=
{a₁ : A} (p₀ : a₀ = a₁) (H : P p₀) ⦃a₂ : A⦄ (p : a₀ = a₂) : P p :=
begin
induction p₀, induction p, exact H
end
@ -125,6 +131,54 @@ namespace eq
cases qr with q r, apply transport P r, induction q, exact H
end
definition eq.rec_equiv_symm {A B : Type} {a₁ : A} (f : A ≃ B) {P : Π{a₀}, f a₀ = f a₁ → Type}
(H : P (idpath (f a₁))) ⦃a₀ : A⦄ (p : f a₀ = f a₁) : P p :=
begin
assert qr : Σ(q : a₀ = a₁), ap f q = p,
{ exact ⟨eq_of_fn_eq_fn f p, ap_eq_of_fn_eq_fn' f p⟩ },
cases qr with q r, apply transport P r, induction q, exact H
end
definition eq.rec_equiv_to_same {A B : Type} {a₀ : A} (f : A ≃ B) {P : Π{a₁}, f a₀ = f a₁ → Type}
⦃a₁' : A⦄ (p' : f a₀ = f a₁') (H : P p') ⦃a₁ : A⦄ (p : f a₀ = f a₁) : P p :=
begin
revert a₁' p' H a₁ p,
refine eq.rec_equiv f _,
exact eq.rec_equiv f
end
definition eq.rec_equiv_to {A A' B : Type} {a₀ : A} (f : A ≃ B) (g : A' ≃ B)
{P : Π{a₁}, f a₀ = g a₁ → Type}
⦃a₁' : A'⦄ (p' : f a₀ = g a₁') (H : P p') ⦃a₁ : A'⦄ (p : f a₀ = g a₁) : P p :=
begin
assert qr : Σ(q : g⁻¹ (f a₀) = a₁), (right_inv g (f a₀))⁻¹ ⬝ ap g q = p,
{ exact ⟨eq_of_fn_eq_fn g (right_inv g (f a₀) ⬝ p),
whisker_left _ (ap_eq_of_fn_eq_fn' g _) ⬝ !inv_con_cancel_left⟩ },
assert q'r' : Σ(q' : g⁻¹ (f a₀) = a₁'), (right_inv g (f a₀))⁻¹ ⬝ ap g q' = p',
{ exact ⟨eq_of_fn_eq_fn g (right_inv g (f a₀) ⬝ p'),
whisker_left _ (ap_eq_of_fn_eq_fn' g _) ⬝ !inv_con_cancel_left⟩ },
induction qr with q r, induction q'r' with q' r',
induction q, induction q',
induction r, induction r',
exact H
end
definition eq.rec_grading {A A' B : Type} {a : A} (f : A ≃ B) (g : A' ≃ B)
{P : Π{b}, f a = b → Type}
{a' : A'} (p' : f a = g a') (H : P p') ⦃b : B⦄ (p : f a = b) : P p :=
begin
revert b p, refine equiv_rect g _ _,
exact eq.rec_equiv_to f g p' H
end
definition eq.rec_grading_unbased {A B B' C : Type} (f : A ≃ B) (g : B ≃ C) (h : B' ≃ C)
{P : Π{b c}, g b = c → Type}
{a' : A} {b' : B'} (p' : g (f a') = h b') (H : P p') ⦃b : B⦄ ⦃c : C⦄ (q : f a' = b)
(p : g b = c) : P p :=
begin
induction q, exact eq.rec_grading (f ⬝e g) h p' H p
end
definition eq.rec_symm {A : Type} {a₀ : A} {P : Π⦃a₁⦄, a₁ = a₀ → Type}
(H : P idp) ⦃a₁ : A⦄ (p : a₁ = a₀) : P p :=
begin
@ -138,6 +192,12 @@ namespace eq
apply is_trunc_of_is_contr
end
definition cast_fn_cast_square {A : Type} {B C : A → Type} (f : Π⦃a⦄, B a → C a) {a₁ a₂ : A}
(p : a₁ = a₂) (q : a₂ = a₁) (r : p ⬝ q = idp) (b : B a₁) :
cast (ap C q) (f (cast (ap B p) b)) = f b :=
have q⁻¹ = p, from inv_eq_of_idp_eq_con r⁻¹,
begin induction this, induction q, reflexivity end
section -- squares
variables {A B : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ a₃ a₄ : A}
/-a₀₀-/ {p₁₀ p₁₀' : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/