[GOAL]
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N
[PROOFSTEP]
convert congr_arg LinearMap.range (underlyingIso_arrow (↾N.subtype : of R { x // x ∈ N } ⟶ M)) using 1
[GOAL]
case h.e'_2
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) =
    LinearMap.range ((underlyingIso (↾(Submodule.subtype N))).inv ≫ arrow (Subobject.mk (↾(Submodule.subtype N))))
[PROOFSTEP]
have :
  -- Porting note: added the `.toLinearEquiv.toLinearMap`(underlyingIso (↾N.subtype : of R _ ⟶ M)).inv =
    (underlyingIso (↾N.subtype : of R _ ⟶ M)).symm.toLinearEquiv.toLinearMap :=
  by
  apply LinearMap.ext
  intro x
  rfl
[GOAL]
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ (underlyingIso (↾(Submodule.subtype N))).inv = ↑(Iso.toLinearEquiv (underlyingIso (↾(Submodule.subtype N))).symm)
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case h
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ ∀ (x : ↑(of R { x // x ∈ N })),
    ↑(underlyingIso (↾(Submodule.subtype N))).inv x =
      ↑↑(Iso.toLinearEquiv (underlyingIso (↾(Submodule.subtype N))).symm) x
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
x : ↑(of R { x // x ∈ N })
⊢ ↑(underlyingIso (↾(Submodule.subtype N))).inv x =
    ↑↑(Iso.toLinearEquiv (underlyingIso (↾(Submodule.subtype N))).symm) x
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
this : (underlyingIso (↾(Submodule.subtype N))).inv = ↑(Iso.toLinearEquiv (underlyingIso (↾(Submodule.subtype N))).symm)
⊢ (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) =
    LinearMap.range ((underlyingIso (↾(Submodule.subtype N))).inv ≫ arrow (Subobject.mk (↾(Submodule.subtype N))))
[PROOFSTEP]
rw [this, comp_def, LinearEquiv.range_comp]
[GOAL]
case h.e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ N = LinearMap.range (↾(Submodule.subtype N))
[PROOFSTEP]
exact (Submodule.range_subtype _).symm
[GOAL]
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ S = (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S)
[PROOFSTEP]
fapply eq_mk_of_comm
[GOAL]
case i
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ underlying.obj S ≅ of R { x // x ∈ (fun S => LinearMap.range (arrow S)) S }
[PROOFSTEP]
apply LinearEquiv.toModuleIso'Left
[GOAL]
case i.e
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ↑(underlying.obj S) ≃ₗ[R] { x // x ∈ (fun S => LinearMap.range (arrow S)) S }
[PROOFSTEP]
apply LinearEquiv.ofBijective (LinearMap.codRestrict (LinearMap.range S.arrow) S.arrow _)
[GOAL]
case i.e
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ Function.Bijective ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S) ?m.95491)
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ∀ (c : ↑(underlying.obj S)), ↑(arrow S) c ∈ LinearMap.range (arrow S)
[PROOFSTEP]
constructor
[GOAL]
case i.e.left
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ Function.Injective ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S) ?m.95491)
[PROOFSTEP]
simp [← LinearMap.ker_eq_bot, LinearMap.ker_codRestrict]
[GOAL]
case i.e.left
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ LinearMap.ker (arrow S) = ⊥
[PROOFSTEP]
rw [ker_eq_bot_of_mono]
[GOAL]
case i.e.right
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ Function.Surjective ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S) ?m.95491)
[PROOFSTEP]
rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict, Submodule.comap_subtype_self]
[GOAL]
case i.e.right.hf
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ∀ (c : ↑(underlying.obj S)), ↑(arrow S) c ∈ LinearMap.range (arrow S)
[PROOFSTEP]
exact LinearMap.mem_range_self _
[GOAL]
case w
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ (LinearEquiv.toModuleIso'Left
          (LinearEquiv.ofBijective
            (LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
              (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S)))
            (_ :
              Function.Injective
                  ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                      (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S))) ∧
                Function.Surjective
                  ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                      (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S)))))).hom ≫
      ↾(Submodule.subtype ((fun S => LinearMap.range (arrow S)) S)) =
    arrow S
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
case w.h
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ∀ (x : ↑(underlying.obj S)),
    ↑((LinearEquiv.toModuleIso'Left
                (LinearEquiv.ofBijective
                  (LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                    (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S)))
                  (_ :
                    Function.Injective
                        ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                            (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S))) ∧
                      Function.Surjective
                        ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                            (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S)))))).hom ≫
            ↾(Submodule.subtype ((fun S => LinearMap.range (arrow S)) S)))
        x =
      ↑(arrow S) x
[PROOFSTEP]
intro x
[GOAL]
case w.h
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
x : ↑(underlying.obj S)
⊢ ↑((LinearEquiv.toModuleIso'Left
              (LinearEquiv.ofBijective
                (LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                  (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S)))
                (_ :
                  Function.Injective
                      ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                          (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S))) ∧
                    Function.Surjective
                      ↑(LinearMap.codRestrict (LinearMap.range (arrow S)) (arrow S)
                          (_ : ∀ (x : ↑(underlying.obj S)), ↑(arrow S) x ∈ LinearMap.range (arrow S)))))).hom ≫
          ↾(Submodule.subtype ((fun S => LinearMap.range (arrow S)) S)))
      x =
    ↑(arrow S) x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
⊢ ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
            left_inv :=
              (_ :
                ∀ (N : Submodule R ↑M),
                  (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
            right_inv :=
              (_ :
                ∀ (S : Subobject M),
                  (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
        S ≤
      ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
            left_inv :=
              (_ :
                ∀ (N : Submodule R ↑M),
                  (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
            right_inv :=
              (_ :
                ∀ (S : Subobject M),
                  (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
        T ↔
    S ≤ T
[PROOFSTEP]
refine' ⟨fun h => _, fun h => mk_le_mk_of_comm (↟(Submodule.ofLe h)) rfl⟩
[GOAL]
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
          left_inv :=
            (_ :
              ∀ (N : Submodule R ↑M),
                (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
          right_inv :=
            (_ :
              ∀ (S : Subobject M),
                (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
      S ≤
    ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
          left_inv :=
            (_ :
              ∀ (N : Submodule R ↑M),
                (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
          right_inv :=
            (_ :
              ∀ (S : Subobject M),
                (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
      T
⊢ S ≤ T
[PROOFSTEP]
convert LinearMap.range_comp_le_range (ofMkLEMk _ _ h) (↾T.subtype)
[GOAL]
case h.e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
          left_inv :=
            (_ :
              ∀ (N : Submodule R ↑M),
                (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
          right_inv :=
            (_ :
              ∀ (S : Subobject M),
                (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
      S ≤
    ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
          left_inv :=
            (_ :
              ∀ (N : Submodule R ↑M),
                (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
          right_inv :=
            (_ :
              ∀ (S : Subobject M),
                (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
      T
⊢ S =
    LinearMap.range
      (LinearMap.comp (↾(Submodule.subtype T)) (ofMkLEMk (↾(Submodule.subtype S)) (↾(Submodule.subtype T)) h))
[PROOFSTEP]
simpa only [← comp_def, ofMkLEMk_comp] using (Submodule.range_subtype _).symm
[GOAL]
case h.e'_4
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
          left_inv :=
            (_ :
              ∀ (N : Submodule R ↑M),
                (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
          right_inv :=
            (_ :
              ∀ (S : Subobject M),
                (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
      S ≤
    ↑{ toFun := fun N => Subobject.mk (↾(Submodule.subtype N)), invFun := fun S => LinearMap.range (arrow S),
          left_inv :=
            (_ :
              ∀ (N : Submodule R ↑M),
                (fun S => LinearMap.range (arrow S)) ((fun N => Subobject.mk (↾(Submodule.subtype N))) N) = N),
          right_inv :=
            (_ :
              ∀ (S : Subobject M),
                (fun N => Subobject.mk (↾(Submodule.subtype N))) ((fun S => LinearMap.range (arrow S)) S) = S) }
      T
⊢ T = LinearMap.range (↾(Submodule.subtype T))
[PROOFSTEP]
exact (Submodule.range_subtype _).symm
[GOAL]
R : Type u
inst✝ : Ring R
M✝ : ModuleCat R
M N : ModuleCat R
f : M ⟶ N
x : { x // x ∈ LinearMap.ker f }
⊢ ↑(arrow (kernelSubobject f)) (↑toKernelSubobject x) = ↑x
[PROOFSTEP]
suffices ((arrow ((kernelSubobject f))) ∘ (kernelSubobjectIso f ≪≫ kernelIsoKer f).inv) x = x by convert this
[GOAL]
R : Type u
inst✝ : Ring R
M✝ : ModuleCat R
M N : ModuleCat R
f : M ⟶ N
x : { x // x ∈ LinearMap.ker f }
this : (↑(arrow (kernelSubobject f)) ∘ ↑(kernelSubobjectIso f ≪≫ kernelIsoKer f).inv) x = ↑x
⊢ ↑(arrow (kernelSubobject f)) (↑toKernelSubobject x) = ↑x
[PROOFSTEP]
convert this
[GOAL]
R : Type u
inst✝ : Ring R
M✝ : ModuleCat R
M N : ModuleCat R
f : M ⟶ N
x : { x // x ∈ LinearMap.ker f }
⊢ (↑(arrow (kernelSubobject f)) ∘ ↑(kernelSubobjectIso f ≪≫ kernelIsoKer f).inv) x = ↑x
[PROOFSTEP]
rw [Iso.trans_inv, ← coe_comp, Category.assoc]
[GOAL]
R : Type u
inst✝ : Ring R
M✝ : ModuleCat R
M N : ModuleCat R
f : M ⟶ N
x : { x // x ∈ LinearMap.ker f }
⊢ ↑((kernelIsoKer f).inv ≫ (kernelSubobjectIso f).inv ≫ arrow (kernelSubobject f)) x = ↑x
[PROOFSTEP]
simp only [Category.assoc, kernelSubobject_arrow', kernelIsoKer_inv_kernel_ι]
[GOAL]
R : Type u
inst✝ : Ring R
M✝ : ModuleCat R
M N : ModuleCat R
f : M ⟶ N
x : { x // x ∈ LinearMap.ker f }
⊢ ↑(Submodule.subtype (LinearMap.ker f)) x = ↑x
[PROOFSTEP]
aesop_cat
[GOAL]
R : Type u
inst✝² : Ring R
M✝ L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
x y : ↑N
l : ↑L
w : x = y + ↑g (↑(factorThruImageSubobject f) l)
⊢ ↑(cokernel.π g) x = ↑(cokernel.π g) y
[PROOFSTEP]
subst w
[GOAL]
R : Type u
inst✝² : Ring R
M✝ L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
y : ↑N
l : ↑L
⊢ ↑(cokernel.π g) (y + ↑g (↑(factorThruImageSubobject f) l)) = ↑(cokernel.π g) y
[PROOFSTEP]
simp only [map_add, add_right_eq_self]
[GOAL]
R : Type u
inst✝² : Ring R
M✝ L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
y : ↑N
l : ↑L
⊢ ↑(cokernel.π g) (↑g (↑(factorThruImageSubobject f) l)) = 0
[PROOFSTEP]
change ((cokernel.π g) ∘ (g) ∘ (factorThruImageSubobject f)) l = 0
[GOAL]
R : Type u
inst✝² : Ring R
M✝ L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
y : ↑N
l : ↑L
⊢ (↑(cokernel.π g) ∘ ↑g ∘ ↑(factorThruImageSubobject f)) l = 0
[PROOFSTEP]
rw [← coe_comp, ← coe_comp, Category.assoc]
[GOAL]
R : Type u
inst✝² : Ring R
M✝ L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
y : ↑N
l : ↑L
⊢ ↑(factorThruImageSubobject f ≫ g ≫ cokernel.π g) l = 0
[PROOFSTEP]
simp only [cokernel.condition, comp_zero]
[GOAL]
R : Type u
inst✝² : Ring R
M✝ L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
y : ↑N
l : ↑L
⊢ ↑0 l = 0
[PROOFSTEP]
rfl
