Skip to content

Instantly share code, notes, and snippets.

@Shamrock-Frost

Shamrock-Frost/terrible terrible goal

Created July 19, 2022 02:14
Show Gist options
  • Save Shamrock-Frost/2326562bfbead0edace30c361bda2f47 to your computer and use it in GitHub Desktop.
Save Shamrock-Frost/2326562bfbead0edace30c361bda2f47 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
terrible terrible goal
R: Type
X: Top
j: ℕ
_inst_2: comm_ring R
i_fst: (singular_chain_complex_basis R (j + 1)).indices
σ: (singular_chain_complex_basis R (j + 1)).models i_fst ⟶ X
⊢ ⇑(((singular_chain_complex R).obj X).d (j + 1) j)
(⇑((singular_chain_complex R ⋙ homological_complex.eval (Module R) (complex_shape.down ℕ) (j + 1)).map σ)
(⇑(cone_construction_hom R
(barycenter
(⟨nat.rec
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
0
punit.star,
punit.star⟩
(λ (n : ℕ)
(ih : pprod ((λ (ᾰ : ℕ), ℕ → ℕ) n) (nat.below (λ (ᾰ : ℕ), ℕ → ℕ) n)),
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
n.succ
⟨ih, punit.star⟩,
⟨ih, punit.star⟩⟩)
0,
punit.star⟩.fst.fst
j +
1))
(_.contraction
(barycenter
(⟨nat.rec
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
0
punit.star,
punit.star⟩
(λ (n : ℕ)
(ih : pprod ((λ (ᾰ : ℕ), ℕ → ℕ) n) (nat.below (λ (ᾰ : ℕ), ℕ → ℕ) n)),
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
n.succ
⟨ih, punit.star⟩,
⟨ih, punit.star⟩⟩)
0,
punit.star⟩.fst.fst
j +
1)))
(⟨nat.rec
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
0
punit.star,
punit.star⟩
(λ (n : ℕ)
(ih : pprod ((λ (ᾰ : ℕ), ℕ → ℕ) n) (nat.below (λ (ᾰ : ℕ), ℕ → ℕ) n)),
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
n.succ
⟨ih, punit.star⟩,
⟨ih, punit.star⟩⟩)
0,
punit.star⟩.fst.fst
j))
(⇑(⟨nat.rec
⟨(λ (n : ℕ)
(_F :
nat.below
(λ (n : ℕ),
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n ⟶
singular_chain_complex R ⋙ homological_complex.eval (Module R) (complex_shape.down ℕ) n)
n),
(λ (n : ℕ)
(_F :
nat.below
(λ (n : ℕ),
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n ⟶
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n)
n),
n.cases_on
(λ
(_F :
nat.below
(λ (n : ℕ),
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n ⟶
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n)
0),
id_rhs
(singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) 0 ⟶
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) 0)
((singular_chain_complex_basis R 0).map_out
(singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) 0)
(λ (_x : (singular_chain_complex_basis R 0).indices),
simplex_to_chain (continuous_map.id ↥(topological_simplex 0)) R)))
(λ (n : ℕ)
(_F :
nat.below
(λ (n : ℕ),
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n ⟶
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n)
n.succ),
id_rhs
(singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) (n + 1) ⟶
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) (n + 1))
((singular_chain_complex_basis R (n + 1)).map_out
(singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) (n + 1))
(λ (_x : (singular_chain_complex_basis R (n + 1)).indices),
⇑(cone_construction_hom R (barycenter (n + 1))
(_.contraction (barycenter (n + 1)))
n)
(⇑(_F.fst.fst.app (Top.of ↥(topological_simplex (n + 1))))
(⇑(((singular_chain_complex R).obj
(Top.of ↥(topological_simplex (n + 1)))).d
(n + 1)
n)
(simplex_to_chain (continuous_map.id ↥(topological_simplex (n + 1)))
R))))))
_F)
n
_F)
0
punit.star,
punit.star⟩
(λ (n : ℕ)
(ih :
pprod
((λ (n : ℕ),
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n ⟶
singular_chain_complex R ⋙ homological_complex.eval (Module R) (complex_shape.down ℕ) n)
n)
(nat.below
(λ (n : ℕ),
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n ⟶
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n)
n)),
⟨(λ (n : ℕ)
(_F :
nat.below
(λ (n : ℕ),
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n ⟶
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n)
n),
(λ (n : ℕ)
(_F :
nat.below
(λ (n : ℕ),
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n ⟶
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n)
n),
n.cases_on
(λ
(_F :
nat.below
(λ (n : ℕ),
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n ⟶
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n)
0),
id_rhs
(singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) 0 ⟶
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) 0)
((singular_chain_complex_basis R 0).map_out
(singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) 0)
(λ (_x : (singular_chain_complex_basis R 0).indices),
simplex_to_chain (continuous_map.id ↥(topological_simplex 0)) R)))
(λ (n : ℕ)
(_F :
nat.below
(λ (n : ℕ),
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n ⟶
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) n)
n.succ),
id_rhs
(singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) (n + 1) ⟶
singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) (n + 1))
((singular_chain_complex_basis R (n + 1)).map_out
(singular_chain_complex R ⋙
homological_complex.eval (Module R) (complex_shape.down ℕ) (n + 1))
(λ (_x : (singular_chain_complex_basis R (n + 1)).indices),
⇑(cone_construction_hom R (barycenter (n + 1))
(_.contraction (barycenter (n + 1)))
n)
(⇑(_F.fst.fst.app (Top.of ↥(topological_simplex (n + 1))))
(⇑(((singular_chain_complex R).obj
(Top.of ↥(topological_simplex (n + 1)))).d
(n + 1)
n)
(simplex_to_chain (continuous_map.id ↥(topological_simplex (n + 1)))
R))))))
_F)
n
_F)
n.succ
⟨ih, punit.star⟩,
⟨ih, punit.star⟩⟩)
(⟨nat.rec
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
0
punit.star,
punit.star⟩
(λ (n : ℕ)
(ih : pprod ((λ (ᾰ : ℕ), ℕ → ℕ) n) (nat.below (λ (ᾰ : ℕ), ℕ → ℕ) n)),
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
n.succ
⟨ih, punit.star⟩,
⟨ih, punit.star⟩⟩)
0,
punit.star⟩.fst.fst
j),
punit.star⟩.fst.fst.app
(Top.of
↥(topological_simplex
(⟨nat.rec
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on
(λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
0
punit.star,
punit.star⟩
(λ (n : ℕ)
(ih :
pprod ((λ (ᾰ : ℕ), ℕ → ℕ) n) (nat.below (λ (ᾰ : ℕ), ℕ → ℕ) n)),
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on
(λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
n.succ
⟨ih, punit.star⟩,
⟨ih, punit.star⟩⟩)
0,
punit.star⟩.fst.fst
j +
1))))
(⇑(((singular_chain_complex R).obj
(Top.of
↥(topological_simplex
(⟨nat.rec
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on
(λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
0
punit.star,
punit.star⟩
(λ (n : ℕ)
(ih :
pprod ((λ (ᾰ : ℕ), ℕ → ℕ) n)
(nat.below (λ (ᾰ : ℕ), ℕ → ℕ) n)),
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ)
(ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on
(λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ)
(_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
n.succ
⟨ih, punit.star⟩,
⟨ih, punit.star⟩⟩)
0,
punit.star⟩.fst.fst
j +
1)))).d
(⟨nat.rec
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
0
punit.star,
punit.star⟩
(λ (n : ℕ)
(ih : pprod ((λ (ᾰ : ℕ), ℕ → ℕ) n) (nat.below (λ (ᾰ : ℕ), ℕ → ℕ) n)),
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
n.succ
⟨ih, punit.star⟩,
⟨ih, punit.star⟩⟩)
0,
punit.star⟩.fst.fst
j +
1)
(⟨nat.rec
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
0
punit.star,
punit.star⟩
(λ (n : ℕ)
(ih : pprod ((λ (ᾰ : ℕ), ℕ → ℕ) n) (nat.below (λ (ᾰ : ℕ), ℕ → ℕ) n)),
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
n.succ
⟨ih, punit.star⟩,
⟨ih, punit.star⟩⟩)
0,
punit.star⟩.fst.fst
j))
(simplex_to_chain
(continuous_map.id
↥(topological_simplex
(⟨nat.rec
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on
(λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
0
punit.star,
punit.star⟩
(λ (n : ℕ)
(ih :
pprod ((λ (ᾰ : ℕ), ℕ → ℕ) n)
(nat.below (λ (ᾰ : ℕ), ℕ → ℕ) n)),
⟨(λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ ᾰ_1 : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1),
ᾰ_1.cases_on
(λ (_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) 0), id_rhs ℕ ᾰ)
(λ (ᾰ_1 : ℕ)
(_F : nat.below (λ (ᾰ : ℕ), ℕ → ℕ) ᾰ_1.succ),
id_rhs ℕ (_F.fst.fst ᾰ).succ)
_F)
ᾰ_1
ᾰ
_F)
n.succ
⟨ih, punit.star⟩,
⟨ih, punit.star⟩⟩)
0,
punit.star⟩.fst.fst
j +
1)))
R))))) =
⇑(((singular_chain_complex R).obj X).d (j + 1) j ≫ (barycentric_subdivision_in_deg R j).app X)
(⇑((singular_chain_complex_basis R (j + 1)).get_basis X) ⟨i_fst, σ⟩)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment