[Merged by Bors] - feat: quasi-isomorphisms of short complexes#7262
[Merged by Bors] - feat: quasi-isomorphisms of short complexes#7262
Conversation
joelriou
commented
Sep 19, 2023
joelriou
commented
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
| lemma quasiIso_comp' (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) (hφ : QuasiIso φ) (hφ' : QuasiIso φ') : | ||
| QuasiIso (φ ≫ φ') := by | ||
| rw [quasiIso_iff] at hφ hφ' ⊢ | ||
| rw [homologyMap_comp] | ||
| infer_instance | ||
|
|
||
| instance quasiIso_comp (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [QuasiIso φ] [QuasiIso φ'] : | ||
| QuasiIso (φ ≫ φ') := | ||
| quasiIso_comp' φ φ' inferInstance inferInstance |
There was a problem hiding this comment.
You are essentially duplicating every instance as a lemma. But since Lean 4 permits named variables, I wonder whether it is enough to just provide the instances and give nice names to the instance variables:
| lemma quasiIso_comp' (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) (hφ : QuasiIso φ) (hφ' : QuasiIso φ') : | |
| QuasiIso (φ ≫ φ') := by | |
| rw [quasiIso_iff] at hφ hφ' ⊢ | |
| rw [homologyMap_comp] | |
| infer_instance | |
| instance quasiIso_comp (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [QuasiIso φ] [QuasiIso φ'] : | |
| QuasiIso (φ ≫ φ') := | |
| quasiIso_comp' φ φ' inferInstance inferInstance | |
| instance quasiIso_comp (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ : QuasiIso φ] [hφ' : QuasiIso φ'] : | |
| QuasiIso (φ ≫ φ') := by | |
| rw [quasiIso_iff] at hφ hφ' ⊢ | |
| rw [homologyMap_comp] | |
| infer_instance |
This can then be used as quasiIso_comp φ φ' (hφ := foo) (hφ' := bar) when needed.
There was a problem hiding this comment.
Thanks! I have struggled a little bit with the syntax to make this work downstream, but it works. (It seems the exact syntax would be quasiIso_comp (hφ := foo) (hφ' := bar) because from the type of hφ, Lean would find the type of φ!)
jcommelin
added
awaiting-author
joelriou
added
awaiting-review
and removed
awaiting-author
ghost
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
2 participants
