Zulip Chat Archive

Stream: new members

Topic: Easy way to lift the entire structure?

view this post on Zulip Joe (Mar 11 2019 at 20:17):

I have some algebraic structure, say a vector space. Then I take a quotient on the structure, and the equivalence relation is respected by all the operations of the algebraic structure (like addition and scalar multiplication). Then I want to say that the quotient space has the same algebraic structure, and there is a natural homomorphism between the original space and the quotient space. Do I need to prove everything again?

view this post on Zulip Patrick Massot (Mar 11 2019 at 20:25):

Currently we don't have a tactic automating this. But there are many examples in mathlib (including the one of vector spaces).

Last updated: May 12 2021 at 23:13 UTC