English
Under suitable hypotheses on a ring hom f and a nilpotent kernel, an element e₁ in the target which is idempotent and in the range of f comes from an idempotent e' in the domain with prescribed annihilation relations with e₂.
Русский
При подходящих условиях на кольцо-гомоморфизм f и нильпотентное ядро, элемент e₁ в образе (в котором уже идемпотент) порождается идемпотентом e' в области с заданными условиями взаимодействия с e₂.
LaTeX
$$∃ e' ∈ R, IsIdempotentElem e' ∧ f e' = e₁ ∧ e' e₂ = 0 ∧ e₂ e' = 0$$
Lean4
theorem exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) (e₁ : S)
(he : e₁ ∈ f.range) (he₁ : IsIdempotentElem e₁) (e₂ : R) (he₂ : IsIdempotentElem e₂) (he₁e₂ : e₁ * f e₂ = 0) :
∃ e' : R, IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0 :=
by
obtain ⟨e₁, rfl⟩ := he
cases subsingleton_or_nontrivial R
· exact ⟨_, Subsingleton.elim _ _, rfl, Subsingleton.elim _ _⟩
let a := e₁ - e₁ * e₂
have ha : f a = f e₁ := by rw [map_sub, map_mul, he₁e₂, sub_zero]
have ha' : a * e₂ = 0 := by rw [sub_mul, mul_assoc, he₂.eq, sub_self]
have hx' : a - a ^ 2 ∈ RingHom.ker f := by simp [RingHom.mem_ker, pow_two, ha, he₁.eq]
obtain ⟨n, hn⟩ := h _ hx'
refine ⟨_, isIdempotentElem_one_sub_one_sub_pow_pow _ _ hn, ?_, ?_⟩
· rcases n with - | n
· simp at hn
simp only [map_sub, map_one, map_pow, ha, he₁.pow_succ_eq, he₁.one_sub.pow_succ_eq, sub_sub_cancel]
· obtain ⟨k, hk⟩ := (Commute.one_left (MulOpposite.op <| 1 - a ^ n)).sub_dvd_pow_sub_pow n
apply_fun MulOpposite.unop at hk
have : 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n := by simpa using hk
rw [this, mul_assoc]
rcases n with - | n
· simp at hn
rw [pow_succ, mul_assoc, ha', mul_zero, mul_zero]
