Zulip Chat Archive

Stream: Is there code for X?

Topic: Swapping quotients


Jason KY. (Jan 31 2021 at 15:09):

Hi, does this definition exist in mathlib?

import linear_algebra.basic

variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]

def foo (P Q : submodule R M) (f : P.quotient ≃ₗ[R] Q) : Q.quotient ≃ₗ[R] P :=
begin
  sorry
end

Yury G. Kudryashov (Feb 02 2021 at 04:35):

This is false: take M = ℕ → R, P = {f | ∀ n, f (2 * n) = 0}, Q = ⊤.


Last updated: Dec 20 2023 at 11:08 UTC