[GOAL]
R : Type u
inst✝¹ : CommRing R
D : Type v
inst✝ : SmallCategory D
I : D ⥤ Ideal R
X✝ Y✝ Z✝ : D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun t => ModuleCat.of R (R ⧸ I.obj t),
          map := fun {X Y} w => Submodule.mapQ (I.obj X) (I.obj Y) LinearMap.id (_ : I.obj X ≤ I.obj Y) }.map
      (f ≫ g) =
    { obj := fun t => ModuleCat.of R (R ⧸ I.obj t),
            map := fun {X Y} w => Submodule.mapQ (I.obj X) (I.obj Y) LinearMap.id (_ : I.obj X ≤ I.obj Y) }.map
        f ≫
      { obj := fun t => ModuleCat.of R (R ⧸ I.obj t),
            map := fun {X Y} w => Submodule.mapQ (I.obj X) (I.obj Y) LinearMap.id (_ : I.obj X ≤ I.obj Y) }.map
        g
[PROOFSTEP]
apply Submodule.linearMap_qext
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
D : Type v
inst✝ : SmallCategory D
I : D ⥤ Ideal R
X✝ Y✝ Z✝ : D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ LinearMap.comp
      ({ obj := fun t => ModuleCat.of R (R ⧸ I.obj t),
            map := fun {X Y} w => Submodule.mapQ (I.obj X) (I.obj Y) LinearMap.id (_ : I.obj X ≤ I.obj Y) }.map
        (f ≫ g))
      (Submodule.mkQ (I.obj X✝)) =
    LinearMap.comp
      ({ obj := fun t => ModuleCat.of R (R ⧸ I.obj t),
              map := fun {X Y} w => Submodule.mapQ (I.obj X) (I.obj Y) LinearMap.id (_ : I.obj X ≤ I.obj Y) }.map
          f ≫
        { obj := fun t => ModuleCat.of R (R ⧸ I.obj t),
              map := fun {X Y} w => Submodule.mapQ (I.obj X) (I.obj Y) LinearMap.id (_ : I.obj X ≤ I.obj Y) }.map
          g)
      (Submodule.mkQ (I.obj X✝))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
J : Ideal R
k : ℕᵒᵖ
⊢ J ≤ Ideal.radical ((idealPowersDiagram J).obj k)
[PROOFSTEP]
change _ ≤ (J ^ unop k).radical
[GOAL]
R : Type u
inst✝ : CommRing R
J : Ideal R
k : ℕᵒᵖ
⊢ J ≤ Ideal.radical (J ^ k.unop)
[PROOFSTEP]
cases' unop k with n
[GOAL]
case zero
R : Type u
inst✝ : CommRing R
J : Ideal R
k : ℕᵒᵖ
⊢ J ≤ Ideal.radical (J ^ Nat.zero)
[PROOFSTEP]
simp [Ideal.radical_top, pow_zero, Ideal.one_eq_top, le_top, Nat.zero_eq]
[GOAL]
case succ
R : Type u
inst✝ : CommRing R
J : Ideal R
k : ℕᵒᵖ
n : ℕ
⊢ J ≤ Ideal.radical (J ^ Nat.succ n)
[PROOFSTEP]
simp only [J.radical_pow _ n.succ_pos, Ideal.le_radical]
[GOAL]
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hIJ : I ≤ Ideal.radical J
hJ : Ideal.FG (Ideal.radical J)
⊢ ∃ k, I ^ k ≤ J
[PROOFSTEP]
obtain ⟨k, hk⟩ := J.exists_radical_pow_le_of_fg hJ
[GOAL]
case intro
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hIJ : I ≤ Ideal.radical J
hJ : Ideal.FG (Ideal.radical J)
k : ℕ
hk : Ideal.radical J ^ k ≤ J
⊢ ∃ k, I ^ k ≤ J
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hIJ : I ≤ Ideal.radical J
hJ : Ideal.FG (Ideal.radical J)
k : ℕ
hk : Ideal.radical J ^ k ≤ J
⊢ I ^ k ≤ J
[PROOFSTEP]
calc
  I ^ k ≤ J.radical ^ k := Ideal.pow_mono hIJ _
  _ ≤ J := hk
[GOAL]
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ IsConnected (CostructuredArrow (idealPowersToSelfLERadical J) J')
[PROOFSTEP]
apply (config := { allowSynthFailures := true }) zigzag_isConnected
[GOAL]
case inst
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ Nonempty (CostructuredArrow (idealPowersToSelfLERadical J) J')
[PROOFSTEP]
obtain ⟨k, hk⟩ := Ideal.exists_pow_le_of_le_radical_of_fG J'.2 (isNoetherian_def.mp hR _)
[GOAL]
case inst.intro
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
k : ℕ
hk : J ^ k ≤ J'.obj
⊢ Nonempty (CostructuredArrow (idealPowersToSelfLERadical J) J')
[PROOFSTEP]
exact ⟨CostructuredArrow.mk (⟨⟨hk⟩⟩ : (idealPowersToSelfLERadical J).obj (op k) ⟶ J')⟩
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ ∀ (j₁ j₂ : CostructuredArrow (idealPowersToSelfLERadical J) J'), Zigzag j₁ j₂
[PROOFSTEP]
intro j1 j2
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
⊢ Zigzag j1 j2
[PROOFSTEP]
apply Relation.ReflTransGen.single
[GOAL]
case h.hab
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
⊢ Zag j1 j2
[PROOFSTEP]
cases' le_total (unop j1.left) (unop j2.left) with h h
[GOAL]
case h.hab.inl
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : j1.left.unop ≤ j2.left.unop
⊢ Zag j1 j2
case h.hab.inr
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : j2.left.unop ≤ j1.left.unop
⊢ Zag j1 j2
[PROOFSTEP]
right
[GOAL]
case h.hab.inl.h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : j1.left.unop ≤ j2.left.unop
⊢ Nonempty (j2 ⟶ j1)
case h.hab.inr
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : j2.left.unop ≤ j1.left.unop
⊢ Zag j1 j2
[PROOFSTEP]
exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩
[GOAL]
case h.hab.inr
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : j2.left.unop ≤ j1.left.unop
⊢ Zag j1 j2
[PROOFSTEP]
left
[GOAL]
case h.hab.inr.h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : j2.left.unop ≤ j1.left.unop
⊢ Nonempty (j1 ⟶ j2)
[PROOFSTEP]
exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩
[GOAL]
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hJK : Ideal.radical J = Ideal.radical K
L : Ideal R
hL : J ≤ Ideal.radical L
⊢ K ≤ Ideal.radical L
[PROOFSTEP]
rw [← Ideal.radical_le_radical_iff] at hL ⊢
[GOAL]
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hJK : Ideal.radical J = Ideal.radical K
L : Ideal R
hL : Ideal.radical J ≤ Ideal.radical L
⊢ Ideal.radical K ≤ Ideal.radical L
[PROOFSTEP]
exact hJK.symm.trans_le hL
