Adjoining elements with matching squares

An intermediate field contains the field generated by a set as soon as it contains, for each element of the set, an element with the same square. Consequently, two sets of elements generate the same intermediate field if every element of either set has the same square as some element of the other. This makes square-root composita independent of the choices of signs, as needed to identify explicit genus fields with their canonical prime-discriminant composita. No restriction on the characteristic is needed.

theorem TauCeti.IntermediateField.adjoin_le_of_forall_sq_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {s : Set L} {F : IntermediateField K L} (h : ∀ x ∈ s, ∃ y ∈ F, x ^ 2 = y ^ 2) : IntermediateField.adjoin K s ≤ F

An intermediate field containing, for each element of s, an element with the same square contains the field generated by s. The set need not be finite, and the field may have any characteristic.

theorem TauCeti.IntermediateField.adjoin_eq_adjoin_of_forall_sq_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {s t : Set L} (hst : ∀ x ∈ s, ∃ y ∈ t, x ^ 2 = y ^ 2) (hts : ∀ y ∈ t, ∃ x ∈ s, y ^ 2 = x ^ 2) : IntermediateField.adjoin K s = IntermediateField.adjoin K t

Two sets with square-matching witnesses in both directions generate the same intermediate field. The sets need not be finite, and the field may have any characteristic.