English
Under a positivity assumption on n, the lifted map from R/n to the Selmer group is injective.
Русский
При условии, что n положительно, пробужденное отображение из R/n в Selmer-группу инъективно.
LaTeX
$$fromUnitLift_injective [Fact (0 < n)] : Function.Injective (fromUnitLift n)$$
Lean4
theorem fromUnit_ker [hn : Fact <| 0 < n] : (@fromUnit R _ _ K _ _ _ n).ker = (powMonoidHom n : Rˣ →* Rˣ).range :=
by
ext ⟨_, _, _, _⟩
constructor
· intro hx
rcases (QuotientGroup.eq_one_iff _).mp (Subtype.mk.inj hx) with ⟨⟨v, i, vi, iv⟩, hx⟩
have hv : ↑(_ ^ n : Kˣ) = algebraMap R K _ := congr_arg Units.val hx
have hi : ↑(_ ^ n : Kˣ)⁻¹ = algebraMap R K _ := congr_arg Units.inv hx
rw [Units.val_pow_eq_pow_val] at hv
rw [← inv_pow, Units.inv_mk, Units.val_pow_eq_pow_val] at hi
rcases
IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow (R := R) (x := v) hn.out
(hv.symm ▸ isIntegral_algebraMap) with
⟨v', rfl⟩
rcases
IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow (R := R) (x := i) hn.out
(hi.symm ▸ isIntegral_algebraMap) with
⟨i', rfl⟩
rw [← map_mul, map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R K] at vi
rw [← map_mul, map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R K] at iv
rw [Units.val_mk, ← map_pow] at hv
exact
⟨⟨v', i', vi, iv⟩, by
simpa only [Units.ext_iff, powMonoidHom_apply, Units.val_pow_eq_pow_val] using
FaithfulSMul.algebraMap_injective R K hv⟩
· rintro ⟨x, hx⟩
rw [← hx]
exact
Subtype.mk_eq_mk.mpr <|
(QuotientGroup.eq_one_iff _).mpr
⟨Units.map (algebraMap R K) x, by simp only [powMonoidHom_apply, RingHom.toMonoidHom_eq_coe, map_pow]⟩
