-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(algebraic_topology/dold_kan): construction of idempotent endomorphisms #15616
Conversation
def Q (q : ℕ) : K[X] ⟶ K[X] := 𝟙 _ - P q | ||
|
||
lemma P_add_Q (q : ℕ) : P q + Q q = 𝟙 K[X] := by { rw Q, abel, } | ||
|
||
lemma P_add_Q_f (q n : ℕ) : (P q).f n + (Q q).f n = 𝟙 (X _[n]) := | ||
homological_complex.congr_hom (P_add_Q q) n | ||
|
||
@[simp] | ||
lemma Q_eq_zero : (Q 0 : K[X] ⟶ _) = 0 := sub_self _ | ||
|
||
lemma Q_eq (q : ℕ) : (Q (q+1) : K[X] ⟶ _) = Q q - P q ≫ Hσ q := | ||
by { unfold Q P, simp only [comp_add, comp_id], abel, } | ||
|
||
/-- All the `Q q` coincide with `0` in degree 0. -/ | ||
@[simp] | ||
lemma Q_f_0_eq (q : ℕ) : ((Q q).f 0 : X _[0] ⟶ X _[0]) = 0 := | ||
by simp only [homological_complex.sub_f_apply, homological_complex.id_f, Q, P_f_0_eq, sub_self] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What is the purpose of introducing Q
? Will you use it in later PRs?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the review. Indeed, for a few statements and proofs, it will be more convenient to have Q
also.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
…phisms (#15616) This PR introduces a sequence of idempotent endomorphisms of the alternating face map complex of a simplicial object in a preadditive category. In a future PR, by taking the "limit" of this sequence, we shall get the projection on the normalized subcomplex, parallel to the degenerate sucomplex.
Pull request successfully merged into master. Build succeeded: |
…phisms (leanprover-community#15616) This PR introduces a sequence of idempotent endomorphisms of the alternating face map complex of a simplicial object in a preadditive category. In a future PR, by taking the "limit" of this sequence, we shall get the projection on the normalized subcomplex, parallel to the degenerate sucomplex.
…phisms (#15616) This PR introduces a sequence of idempotent endomorphisms of the alternating face map complex of a simplicial object in a preadditive category. In a future PR, by taking the "limit" of this sequence, we shall get the projection on the normalized subcomplex, parallel to the degenerate sucomplex.
…phisms (#15616) This PR introduces a sequence of idempotent endomorphisms of the alternating face map complex of a simplicial object in a preadditive category. In a future PR, by taking the "limit" of this sequence, we shall get the projection on the normalized subcomplex, parallel to the degenerate sucomplex.
This PR introduces a sequence of idempotent endomorphisms of the alternating face map complex of a simplicial object in a preadditive category. In a future PR, by taking the "limit" of this sequence, we shall get the projection on the normalized subcomplex, parallel to the degenerate sucomplex.