English
A fractional ideal J is ≤ 1 iff it is the image of some ideal I under the embedding.
Русский
Дробный идеал J ≤ 1 тогда и только тогда, когда он является образoм некоторого идеала I через встроение.
LaTeX
$$J \le 1 \iff \exists I: \mathrm{Ideal}(R), \uparrow I = J$$
Lean4
theorem le_one_iff_exists_coeIdeal {J : FractionalIdeal S P} : J ≤ (1 : FractionalIdeal S P) ↔ ∃ I : Ideal R, ↑I = J :=
by
constructor
· intro hJ
refine ⟨⟨⟨⟨{x : R | algebraMap R P x ∈ J}, ?_⟩, ?_⟩, ?_⟩, ?_⟩
· intro a b ha hb
rw [mem_setOf, RingHom.map_add]
exact J.val.add_mem ha hb
· rw [mem_setOf, RingHom.map_zero]
exact J.zero_mem
· intro c x hx
rw [smul_eq_mul, mem_setOf, RingHom.map_mul, ← Algebra.smul_def]
exact J.val.smul_mem c hx
· ext x
constructor
· rintro ⟨y, hy, eq_y⟩
rwa [← eq_y]
· intro hx
obtain ⟨y, rfl⟩ := (mem_one_iff S).mp (hJ hx)
exact mem_setOf.mpr ⟨y, hx, rfl⟩
· rintro ⟨I, hI⟩
rw [← hI]
apply coeIdeal_le_one
