Reflecting real coordinates preserves the fundamental cone

Membership in Mathlib's NumberField.mixedEmbedding.fundamentalCone K depends on a point only through its norms at the infinite places, and so does its mixed norm. Reflecting the real coordinates at a set of real places with negAt changes none of these norms, so it preserves the fundamental cone and every unit translate of the norm-≤-one region normLeOne K.

Main results

• TauCeti.NumberField.mixedEmbedding.negAt_mem_fundamentalCone_iff: negAt s x lies in the fundamental cone exactly when x does.
• TauCeti.NumberField.mixedEmbedding.negAt_mem_unit_smul_normLeOne_iff: the same for the translate u • normLeOne K by a unit u.

@[simp]

theorem TauCeti.NumberField.mixedEmbedding.negAt_mem_fundamentalCone_iff {K : Type u_1} [Field K] [NumberField K] (s : Set { w : NumberField.InfinitePlace K // w.IsReal }) (x : NumberField.mixedEmbedding.mixedSpace K) : (NumberField.mixedEmbedding.negAt s) x ∈ NumberField.mixedEmbedding.fundamentalCone K ↔ x ∈ NumberField.mixedEmbedding.fundamentalCone K

Reflecting real coordinates preserves Mathlib's fundamental cone.

@[simp]

theorem TauCeti.NumberField.mixedEmbedding.negAt_mem_unit_smul_normLeOne_iff {K : Type u_1} [Field K] [NumberField K] (s : Set { w : NumberField.InfinitePlace K // w.IsReal }) (u : (NumberField.RingOfIntegers K)ˣ) (x : NumberField.mixedEmbedding.mixedSpace K) : (NumberField.mixedEmbedding.negAt s) x ∈ u • NumberField.mixedEmbedding.fundamentalCone.normLeOne K ↔ x ∈ u • NumberField.mixedEmbedding.fundamentalCone.normLeOne K

Reflecting real coordinates preserves each unit translate of normLeOne K, since it commutes with the unit action.