English
The diagram diagramcomp provides a natural isomorphism between two ways of composing local cohomology diagrams.
Русский
Диаграмма diagramcomp обеспечивает естественный изоморфизм между двумя способами композиции диаграмм локальной когомологии.
LaTeX
$$$\\text{diagramComp } i : diagram (I' \\cdot I) i \\cong I'.op \\circ diagram I i$$$
Lean4
/-- The diagram of powers of `J` is initial in the diagram of all ideals with
radical containing `J`. This uses Noetherianness. -/
instance ideal_powers_initial [hR : IsNoetherian R R] : Functor.Initial (idealPowersToSelfLERadical J) where
out
J' := by
apply (config := { allowSynthFailures := true }) zigzag_isConnected
· obtain ⟨k, hk⟩ := Ideal.exists_pow_le_of_le_radical_of_fg J'.2 (isNoetherian_def.mp hR _)
exact ⟨CostructuredArrow.mk (⟨⟨hk⟩⟩ : (idealPowersToSelfLERadical J).obj (op k) ⟶ J')⟩
· intro j1 j2
apply Relation.ReflTransGen.single
rcases le_total (unop j1.left) (unop j2.left) with h | h
· right; exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩
· left; exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩
