Normalizing a competing unit at a real place

At a real infinite place, an absolute value forgets the sign of an embedding. To turn the rank-one minimality criterion for logarithmic embeddings into a search among real roots in an interval, invert a unit if its absolute value is below one and multiply it by a torsion unit to make its real embedding positive. Given a suitable bound B, the resulting unit has a real image strictly between 1 and B.

The normalization is used before enumerating possible minimal polynomials: it accounts for both the inversion and the sign that are invisible in the absolute-value criterion.

Main results

• exists_normalized_unit_between: a unit detected by the chosen place, with sufficiently small logarithmic absolute value, yields a unit whose real embedding lies in the search interval.
• generates_mod_torsion_iff_no_unit_between_real: at rank one, a unit expanding at a real place generates modulo torsion exactly when that interval contains no unit.

theorem TauCeti.NumberField.Units.exists_normalized_unit_between {K : Type u_1} [Field K] (B : ℝ) (v : (NumberField.RingOfIntegers K)ˣ) (w : NumberField.InfinitePlace K) (hw : w.IsReal) (hBpos : 0 < B) (hv : w ((algebraMap (NumberField.RingOfIntegers K) K) ↑v) ≠ 1) (hvbound : |Real.log (w ((algebraMap (NumberField.RingOfIntegers K) K) ↑v))| < Real.log B) : ∃ (ε : ↥(NumberField.Units.torsion K)) (δ : (NumberField.RingOfIntegers K)ˣ), (δ = v ∨ δ = v⁻¹) ∧ 1 < (NumberField.InfinitePlace.embedding_of_isReal hw) ((algebraMap (NumberField.RingOfIntegers K) K) ↑(↑ε * δ)) ∧ (NumberField.InfinitePlace.embedding_of_isReal hw) ((algebraMap (NumberField.RingOfIntegers K) K) ↑(↑ε * δ)) < B

A unit with w v ≠ 1 whose logarithmic absolute value is below log B can be inverted and multiplied by a torsion unit so that its real image lies in the open interval from 1 to B.

theorem TauCeti.NumberField.Units.generates_mod_torsion_iff_no_unit_between_real {K : Type u_1} [Field K] [NumberField K] (hr : NumberField.Units.rank K = 1) (u : (NumberField.RingOfIntegers K)ˣ) (w : NumberField.InfinitePlace K) (hw : w.IsReal) (hu : 1 < w ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) : Subgroup.closure {u} ⊔ NumberField.Units.torsion K = ⊤ ↔ ¬∃ (v : (NumberField.RingOfIntegers K)ˣ), 1 < (NumberField.InfinitePlace.embedding_of_isReal hw) ((algebraMap (NumberField.RingOfIntegers K) K) ↑v) ∧ (NumberField.InfinitePlace.embedding_of_isReal hw) ((algebraMap (NumberField.RingOfIntegers K) K) ↑v) < w ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)

At unit rank one, a unit expanding at a real place generates the units modulo torsion if and only if no unit has real image strictly between 1 and w u, the absolute value of the generator's real embedding. The equivalence includes the torsion sign and inversion needed to pass from the intrinsic logarithmic criterion to this one-sided interval.