English
For I, I.homogeneousCore' 𝒜 equals the supremum over homogeneous ideals J with J.toIdeal ≤ I and J IsHomogeneous 𝒜.
Русский
Для I, I.homogeneousCore' 𝒜 равен верхней границе по однородным идеалам J с J.toIdeal ≤ I и J IsHomogeneous 𝒜.
LaTeX
$$$ I.homogeneousCore' 𝒜 = \sup \{ J : HomogeneousIdeal 𝒜 \mid J.IsHomogeneous 𝒜 ∧ J.toIdeal \le I \}$$$
Lean4
theorem homogeneousCore'_eq_sSup : I.homogeneousCore' 𝒜 = sSup {J : Ideal A | J.IsHomogeneous 𝒜 ∧ J ≤ I} :=
by
refine (IsLUB.sSup_eq ?_).symm
apply IsGreatest.isLUB
have coe_mono : Monotone (toIdeal : HomogeneousIdeal 𝒜 → Ideal A) := fun x y => id
convert coe_mono.map_isGreatest (Ideal.homogeneousCore.gc 𝒜).isGreatest_u using 1
ext x
rw [mem_image, mem_setOf_eq]
refine ⟨fun hI => ⟨⟨x, hI.1⟩, ⟨hI.2, rfl⟩⟩, ?_⟩
rintro ⟨x, ⟨hx, rfl⟩⟩
exact ⟨x.isHomogeneous, hx⟩
