[GOAL]
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
⊢ ∃ y, 0 ≠ y
[PROOFSTEP]
have h : (⊥ : Submodule R M) ≠ ⊤ := bot_ne_top
[GOAL]
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ⊥ ≠ ⊤
⊢ ∃ y, 0 ≠ y
[PROOFSTEP]
contrapose! h
[GOAL]
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ∀ (y : M), 0 = y
⊢ ⊥ = ⊤
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ∀ (y : M), 0 = y
x : M
⊢ x ∈ ⊥ ↔ x ∈ ⊤
[PROOFSTEP]
simp [Submodule.mem_bot, Submodule.mem_top, h x]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsSimpleModule R { x // x ∈ m } ↔ IsAtom m
[PROOFSTEP]
rw [← Set.isSimpleOrder_Iic_iff_isAtom]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsSimpleModule R { x // x ∈ m } ↔ IsSimpleOrder ↑(Set.Iic m)
[PROOFSTEP]
apply OrderIso.isSimpleOrder_iff
[GOAL]
case f
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ Submodule R { x // x ∈ m } ≃o ↑(Set.Iic m)
[PROOFSTEP]
exact Submodule.MapSubtype.relIso m
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsSimpleModule R (M ⧸ m) ↔ IsCoatom m
[PROOFSTEP]
rw [← Set.isSimpleOrder_Ici_iff_isCoatom]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsSimpleModule R (M ⧸ m) ↔ IsSimpleOrder ↑(Set.Ici m)
[PROOFSTEP]
apply OrderIso.isSimpleOrder_iff
[GOAL]
case f
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ Submodule R (M ⧸ m) ≃o ↑(Set.Ici m)
[PROOFSTEP]
exact Submodule.comapMkQRelIso m
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A B : Submodule R M
hAB : A ≤ B
⊢ A ⋖ B ↔ IsSimpleModule R ({ x // x ∈ B } ⧸ Submodule.comap (Submodule.subtype B) A)
[PROOFSTEP]
set f : Submodule R B ≃o Set.Iic B := Submodule.MapSubtype.relIso B with hf
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A B : Submodule R M
hAB : A ≤ B
f : Submodule R { x // x ∈ B } ≃o ↑(Set.Iic B) := Submodule.MapSubtype.relIso B
hf : f = Submodule.MapSubtype.relIso B
⊢ A ⋖ B ↔ IsSimpleModule R ({ x // x ∈ B } ⧸ Submodule.comap (Submodule.subtype B) A)
[PROOFSTEP]
rw [covby_iff_coatom_Iic hAB, isSimpleModule_iff_isCoatom, ← OrderIso.isCoatom_iff f, hf]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A B : Submodule R M
hAB : A ≤ B
f : Submodule R { x // x ∈ B } ≃o ↑(Set.Iic B) := Submodule.MapSubtype.relIso B
hf : f = Submodule.MapSubtype.relIso B
⊢ IsCoatom { val := A, property := hAB } ↔
    IsCoatom (↑(Submodule.MapSubtype.relIso B) (Submodule.comap (Submodule.subtype B) A))
[PROOFSTEP]
simp [-OrderIso.isCoatom_iff, Submodule.MapSubtype.relIso, Submodule.map_comap_subtype, inf_eq_right.2 hAB]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤
⊢ sSup {a | IsAtom a} = ⊤
[PROOFSTEP]
simp_rw [← h, isSimpleModule_iff_isAtom]
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSemisimpleModule R M
⊢ sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤
[PROOFSTEP]
simp_rw [isSimpleModule_iff_isAtom]
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSemisimpleModule R M
⊢ sSup {m | IsAtom m} = ⊤
[PROOFSTEP]
exact sSup_atoms_eq_top
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsSemisimpleModule R M → sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤
[PROOFSTEP]
intro
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
a✝ : IsSemisimpleModule R M
⊢ sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤
[PROOFSTEP]
exact IsSemisimpleModule.sSup_simples_eq_top
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
f : M →ₗ[R] N
⊢ Function.Injective ↑f ∨ f = 0
[PROOFSTEP]
rw [← ker_eq_bot, ← ker_eq_top]
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
f : M →ₗ[R] N
⊢ ker f = ⊥ ∨ ker f = ⊤
[PROOFSTEP]
apply eq_bot_or_eq_top
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
⊢ Function.Surjective ↑f ∨ f = 0
[PROOFSTEP]
rw [← range_eq_top, ← range_eq_bot, or_comm]
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
⊢ range f = ⊥ ∨ range f = ⊤
[PROOFSTEP]
apply eq_bot_or_eq_top
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
⊢ Function.Bijective ↑f ∨ f = 0
[PROOFSTEP]
by_cases h : f = 0
[GOAL]
case pos
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
h : f = 0
⊢ Function.Bijective ↑f ∨ f = 0
[PROOFSTEP]
right
[GOAL]
case pos.h
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
h : f = 0
⊢ f = 0
[PROOFSTEP]
exact h
[GOAL]
case neg
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
h : ¬f = 0
⊢ Function.Bijective ↑f ∨ f = 0
[PROOFSTEP]
exact Or.intro_left _ ⟨injective_of_ne_zero h, surjective_of_ne_zero h⟩
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective ↑f
⊢ IsCoatom (ker f)
[PROOFSTEP]
rw [← isSimpleModule_iff_isCoatom]
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective ↑f
⊢ IsSimpleModule R (M ⧸ ker f)
[PROOFSTEP]
exact IsSimpleModule.congr (f.quotKerEquivOfSurjective hf)
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
⊢ 0 ≠ 1
[PROOFSTEP]
haveI := IsSimpleModule.nontrivial R M
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
this : Nontrivial M
⊢ 0 ≠ 1
[PROOFSTEP]
have h := exists_pair_ne M
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
this : Nontrivial M
h : ∃ x y, x ≠ y
⊢ 0 ≠ 1
[PROOFSTEP]
contrapose! h
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
this : Nontrivial M
h : 0 = 1
⊢ ∀ (x y : M), x = y
[PROOFSTEP]
intro x y
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
this : Nontrivial M
h : 0 = 1
x y : M
⊢ x = y
[PROOFSTEP]
simp_rw [ext_iff, one_apply, zero_apply] at h 
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
this : Nontrivial M
x y : M
h : ∀ (x : M), 0 = x
⊢ x = y
[PROOFSTEP]
rw [← h x, h y]
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
⊢ ∀ (a : Module.End R M), a ≠ 0 → a * a⁻¹ = 1
[PROOFSTEP]
intro a a0
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
a : Module.End R M
a0 : a ≠ 0
⊢ a * a⁻¹ = 1
[PROOFSTEP]
change a * dite _ _ _ = 1
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
a : Module.End R M
a0 : a ≠ 0
⊢ (a *
      if h : a = 0 then 0
      else
        inverse a (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
          (_ :
            Function.LeftInverse (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
              (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).toFun)
          (_ :
            Function.RightInverse (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
              (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).toFun)) =
    1
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
a : Module.End R M
a0 : a ≠ 0
x : M
⊢ ↑(a *
          if h : a = 0 then 0
          else
            inverse a (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
              (_ :
                Function.LeftInverse (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
                  (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).toFun)
              (_ :
                Function.RightInverse (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
                  (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).toFun))
      x =
    ↑1 x
[PROOFSTEP]
rw [dif_neg a0, mul_eq_comp, one_apply, comp_apply]
[GOAL]
case h
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
a : Module.End R M
a0 : a ≠ 0
x : M
⊢ ↑a
      (↑(inverse a (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
            (_ :
              Function.LeftInverse (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
                (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).toFun)
            (_ :
              Function.RightInverse (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
                (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).toFun))
        x) =
    x
[PROOFSTEP]
exact (Equiv.ofBijective _ (bijective_of_ne_zero a0)).right_inv x
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ Iso (X, X ⊔ Y) (X ⊓ Y, Y)
[PROOFSTEP]
constructor
[GOAL]
case val
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ ({ x // x ∈ (X, X ⊔ Y).snd } ⧸ Submodule.comap (Submodule.subtype (X, X ⊔ Y).snd) (X, X ⊔ Y).fst) ≃ₗ[R]
    { x // x ∈ (X ⊓ Y, Y).snd } ⧸ Submodule.comap (Submodule.subtype (X ⊓ Y, Y).snd) (X ⊓ Y, Y).fst
[PROOFSTEP]
rw [sup_comm, inf_comm]
[GOAL]
case val
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ ({ x // x ∈ (X, Y ⊔ X).snd } ⧸ Submodule.comap (Submodule.subtype (X, Y ⊔ X).snd) (X, Y ⊔ X).fst) ≃ₗ[R]
    { x // x ∈ (Y ⊓ X, Y).snd } ⧸ Submodule.comap (Submodule.subtype (Y ⊓ X, Y).snd) (Y ⊓ X, Y).fst
[PROOFSTEP]
dsimp
[GOAL]
case val
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ ({ x // x ∈ Y ⊔ X } ⧸ Submodule.comap (Submodule.subtype (Y ⊔ X)) X) ≃ₗ[R]
    { x // x ∈ Y } ⧸ Submodule.comap (Submodule.subtype Y) Y ⊓ Submodule.comap (Submodule.subtype Y) X
[PROOFSTEP]
exact (LinearMap.quotientInfEquivSupQuotient Y X).symm
