Mathlib.Algebra.Field.Subfield.Basic

Subfield.list_prod_mem theorem

{l : List K} : (∀ x ∈ l, x ∈ s) → l.prod ∈ s

Full source

/-- Product of a list of elements in a subfield is in the subfield. -/
protected theorem list_prod_mem {l : List K} : (∀ x ∈ l, x ∈ s) → l.prod ∈ s :=
  list_prod_mem

Product of Subfield Elements in a List Belongs to Subfield

Informal description

Let $K$ be a division ring and $s$ a subfield of $K$. For any list $l$ of elements in $K$, if every element $x \in l$ belongs to $s$, then the product of all elements in $l$ (computed in $K$) also belongs to $s$.

Subfield.list_sum_mem theorem

{l : List K} : (∀ x ∈ l, x ∈ s) → l.sum ∈ s

Full source

/-- Sum of a list of elements in a subfield is in the subfield. -/
protected theorem list_sum_mem {l : List K} : (∀ x ∈ l, x ∈ s) → l.sum ∈ s :=
  list_sum_mem

Sum of List Elements in Subfield Belongs to Subfield

Informal description

For any list $l$ of elements in a division ring $K$, if every element $x$ in $l$ belongs to a subfield $s$ of $K$, then the sum of all elements in $l$ also belongs to $s$.

Subfield.multiset_sum_mem theorem

(m : Multiset K) : (∀ a ∈ m, a ∈ s) → m.sum ∈ s

Full source

/-- Sum of a multiset of elements in a `Subfield` is in the `Subfield`. -/
protected theorem multiset_sum_mem (m : Multiset K) : (∀ a ∈ m, a ∈ s) → m.sum ∈ s :=
  multiset_sum_mem m

Sum of Multiset Elements in a Subfield Belongs to the Subfield

Informal description

For any multiset $m$ of elements in a division ring $K$, if every element $a$ in $m$ belongs to a subfield $s$ of $K$, then the sum of all elements in $m$ also belongs to $s$.

Subfield.sum_mem theorem

{ι : Type*} {t : Finset ι} {f : ι → K} (h : ∀ c ∈ t, f c ∈ s) : (∑ i ∈ t, f i) ∈ s

Full source

/-- Sum of elements in a `Subfield` indexed by a `Finset` is in the `Subfield`. -/
protected theorem sum_mem {ι : Type*} {t : Finset ι} {f : ι → K} (h : ∀ c ∈ t, f c ∈ s) :
    (∑ i ∈ t, f i) ∈ s :=
  sum_mem h

Sum of Subfield Elements Belongs to Subfield

Informal description

Let $K$ be a division ring and $s$ a subfield of $K$. For any finite set $t$ (indexed by type $\iota$) and function $f : \iota \to K$, if $f(c) \in s$ for all $c \in t$, then the sum $\sum_{i \in t} f(i)$ belongs to $s$.

Subfield.instTop instance

: Top (Subfield K)

Full source

/-- The subfield of `K` containing all elements of `K`. -/
instance : Top (Subfield K) :=
  ⟨{ (⊤ : Subring K) with inv_mem' := fun x _ => Subring.mem_top x }⟩

The Full Subfield as Top Element

Informal description

The subfield of $K$ consisting of all elements of $K$ is the top element in the lattice of subfields of $K$.

Subfield.instInhabited instance

: Inhabited (Subfield K)

Full source

instance : Inhabited (Subfield K) :=
  ⟨⊤⟩

Existence of Subfields in a Division Ring

Informal description

The type of subfields of a division ring $K$ is inhabited, meaning there exists at least one subfield of $K$.

Subfield.mem_top theorem

(x : K) : x ∈ (⊤ : Subfield K)

Full source

@[simp]
theorem mem_top (x : K) : x ∈ (⊤ : Subfield K) :=
  Set.mem_univ x

Membership in the Full Subfield of a Division Ring

Informal description

For any element $x$ in a division ring $K$, $x$ belongs to the top subfield of $K$, which is the entire division ring itself.

Subfield.coe_top theorem

: ((⊤ : Subfield K) : Set K) = Set.univ

Full source

@[simp]
theorem coe_top : ((⊤ : Subfield K) : Set K) = Set.univ :=
  rfl

Top Subfield as Universal Set

Informal description

The underlying set of the top subfield (the entire field $K$) is equal to the universal set of $K$, i.e., $(\top : \text{Subfield } K) = \text{univ}$.

Subfield.topEquiv definition

: (⊤ : Subfield K) ≃+* K

Full source

/-- The ring equiv between the top element of `Subfield K` and `K`. -/
def topEquiv : (⊤ : Subfield K) ≃+* K :=
  Subsemiring.topEquiv

Ring isomorphism between the top subfield and the division ring

Informal description

The ring isomorphism between the top element of the lattice of subfields of a division ring $K$ (which is $K$ itself) and $K$. This equivalence preserves both the additive and multiplicative structures.

Subfield.comap definition

(s : Subfield L) : Subfield K

Full source

/-- The preimage of a subfield along a ring homomorphism is a subfield. -/
def comap (s : Subfield L) : Subfield K :=
  { s.toSubring.comap f with
    inv_mem' := fun x hx =>
      show f x⁻¹ ∈ s by
        rw [map_inv₀ f]
        exact s.inv_mem hx }

Preimage of a subfield under a ring homomorphism

Informal description

Given a ring homomorphism $f : K \to L$ and a subfield $B$ of $L$, the preimage of $B$ under $f$ is a subfield of $K$. This subfield consists of all elements $x \in K$ such that $f(x) \in B$.

Subfield.coe_comap theorem

(s : Subfield L) : (s.comap f : Set K) = f ⁻¹' s

Full source

@[simp]
theorem coe_comap (s : Subfield L) : (s.comap f : Set K) = f ⁻¹' s :=
  rfl

Preimage of Subfield as Set Preimage

Informal description

For any subfield $B$ of $L$ and ring homomorphism $f : K \to L$, the underlying set of the preimage subfield $B.\text{comap}\ f$ is equal to the preimage of $B$ under $f$, i.e., $(B.\text{comap}\ f) = f^{-1}(B)$.

Subfield.mem_comap theorem

{s : Subfield L} {f : K →+* L} {x : K} : x ∈ s.comap f ↔ f x ∈ s

Full source

@[simp]
theorem mem_comap {s : Subfield L} {f : K →+* L} {x : K} : x ∈ s.comap fx ∈ s.comap f ↔ f x ∈ s :=
  Iff.rfl

Membership Criterion for Preimage Subfield

Informal description

For any subfield $B$ of $L$, ring homomorphism $f : K \to L$, and element $x \in K$, we have $x \in B.\text{comap}\ f$ if and only if $f(x) \in B$.

Subfield.comap_comap theorem

(s : Subfield M) (g : L →+* M) (f : K →+* L) : (s.comap g).comap f = s.comap (g.comp f)

Full source

theorem comap_comap (s : Subfield M) (g : L →+* M) (f : K →+* L) :
    (s.comap g).comap f = s.comap (g.comp f) :=
  rfl

Composition of Preimages of Subfields under Ring Homomorphisms

Informal description

For any subfield $s$ of $M$ and ring homomorphisms $g : L \to M$ and $f : K \to L$, the preimage of the preimage of $s$ under $g$ and then under $f$ is equal to the preimage of $s$ under the composition $g \circ f$. In other words, $(s.\text{comap}\ g).\text{comap}\ f = s.\text{comap}\ (g \circ f)$.

Subfield.map definition

(s : Subfield K) : Subfield L

Full source

/-- The image of a subfield along a ring homomorphism is a subfield. -/
def map (s : Subfield K) : Subfield L :=
  { s.toSubring.map f with
    inv_mem' := by
      rintro _ ⟨x, hx, rfl⟩
      exact ⟨x⁻¹, s.inv_mem hx, map_inv₀ f x⟩ }

Image of a subfield under a ring homomorphism

Informal description

Given a ring homomorphism $ f : K \to L $ between division rings (or fields) and a subfield $ s $ of $ K $, the image of $ s $ under $ f $ is a subfield of $ L $. More precisely, the subfield $ \text{map}(f, s) $ consists of all elements $ y \in L $ such that there exists $ x \in s $ with $ f(x) = y $.

Subfield.coe_map theorem

: (s.map f : Set L) = f '' s

Full source

@[simp]
theorem coe_map : (s.map f : Set L) = f '' s :=
  rfl

Image of Subfield Under Ring Homomorphism as Set Image

Informal description

For a subfield $s$ of $K$ and a ring homomorphism $f : K \to L$, the underlying set of the image subfield $\text{map}(f, s)$ is equal to the image of $s$ under $f$, i.e., $(s.\text{map}\ f : \text{Set}\ L) = f '' s$.

Subfield.mem_map theorem

{f : K →+* L} {s : Subfield K} {y : L} : y ∈ s.map f ↔ ∃ x ∈ s, f x = y

Full source

@[simp]
theorem mem_map {f : K →+* L} {s : Subfield K} {y : L} : y ∈ s.map fy ∈ s.map f ↔ ∃ x ∈ s, f x = y := by
  unfold map
  simp only [mem_mk, Subring.mem_mk, Subring.mem_toSubsemiring, Subring.mem_map, mem_toSubring]

Characterization of Elements in the Image of a Subfield under a Ring Homomorphism

Informal description

Let $K$ and $L$ be division rings (or fields), $f : K \to L$ a ring homomorphism, $s$ a subfield of $K$, and $y \in L$. Then $y$ belongs to the image subfield $s.map(f)$ if and only if there exists $x \in s$ such that $f(x) = y$.

Subfield.map_map theorem

(g : L →+* M) (f : K →+* L) : (s.map f).map g = s.map (g.comp f)

Full source

theorem map_map (g : L →+* M) (f : K →+* L) : (s.map f).map g = s.map (g.comp f) :=
  SetLike.ext' <| Set.image_image _ _ _

Image of Subfield under Composition of Ring Homomorphisms Equals Composition of Images

Informal description

Let $K$, $L$, and $M$ be division rings (or fields), and let $f \colon K \to L$ and $g \colon L \to M$ be ring homomorphisms. For any subfield $s$ of $K$, the image of the image of $s$ under $f$ under $g$ is equal to the image of $s$ under the composition $g \circ f$. In symbols: $$g(f(s)) = (g \circ f)(s).$$

Subfield.map_le_iff_le_comap theorem

{f : K →+* L} {s : Subfield K} {t : Subfield L} : s.map f ≤ t ↔ s ≤ t.comap f

Full source

theorem map_le_iff_le_comap {f : K →+* L} {s : Subfield K} {t : Subfield L} :
    s.map f ≤ t ↔ s ≤ t.comap f :=
  Set.image_subset_iff

Image-Preimage Containment Criterion for Subfields

Informal description

Let $K$ and $L$ be division rings (or fields), $f \colon K \to L$ a ring homomorphism, $s$ a subfield of $K$, and $t$ a subfield of $L$. Then the image of $s$ under $f$ is contained in $t$ if and only if $s$ is contained in the preimage of $t$ under $f$. In symbols: \[ f(s) \subseteq t \leftrightarrow s \subseteq f^{-1}(t). \]

Subfield.gc_map_comap theorem

(f : K →+* L) : GaloisConnection (map f) (comap f)

Full source

theorem gc_map_comap (f : K →+* L) : GaloisConnection (map f) (comap f) := fun _ _ =>
  map_le_iff_le_comap

Galois Connection Between Subfield Image and Preimage

Informal description

For any ring homomorphism $f \colon K \to L$ between division rings (or fields), the pair of functions $\mathrm{map}(f)$ and $\mathrm{comap}(f)$ forms a Galois connection between the complete lattices of subfields of $K$ and $L$. That is, for any subfield $A$ of $K$ and any subfield $B$ of $L$, we have: \[ \mathrm{map}(f)(A) \leq B \quad \text{if and only if} \quad A \leq \mathrm{comap}(f)(B). \]

RingHom.fieldRange definition

: Subfield L

Full source

/-- The range of a ring homomorphism, as a subfield of the target. See Note [range copy pattern]. -/
def fieldRange : Subfield L :=
  ((⊤ : Subfield K).map f).copy (Set.range f) Set.image_univ.symm

Range of a ring homomorphism as a subfield

Informal description

The range of a ring homomorphism $f : K \to L$ between division rings (or fields), viewed as a subfield of $L$. It consists of all elements $y \in L$ such that there exists $x \in K$ with $f(x) = y$.

RingHom.coe_fieldRange theorem

: (f.fieldRange : Set L) = Set.range f

Full source

@[simp]
theorem coe_fieldRange : (f.fieldRange : Set L) = Set.range f :=
  rfl

Range of Ring Homomorphism as Subfield Equals Function Range

Informal description

For any ring homomorphism $f \colon K \to L$ between division rings (or fields), the underlying set of the range subfield $\mathrm{fieldRange}(f)$ is equal to the range of $f$ as a function, i.e., $\{f(x) \mid x \in K\}$.

RingHom.mem_fieldRange theorem

{f : K →+* L} {y : L} : y ∈ f.fieldRange ↔ ∃ x, f x = y

Full source

@[simp]
theorem mem_fieldRange {f : K →+* L} {y : L} : y ∈ f.fieldRangey ∈ f.fieldRange ↔ ∃ x, f x = y :=
  Iff.rfl

Characterization of Elements in the Range of a Ring Homomorphism

Informal description

For any ring homomorphism $f \colon K \to L$ between division rings (or fields) and any element $y \in L$, we have $y \in \mathrm{fieldRange}(f)$ if and only if there exists $x \in K$ such that $f(x) = y$.

RingHom.fieldRange_eq_map theorem

: f.fieldRange = Subfield.map f ⊤

Full source

theorem fieldRange_eq_map : f.fieldRange = Subfield.map f ⊤ := by
  ext
  simp

Range of Ring Homomorphism as Image of Top Subfield

Informal description

The range of a ring homomorphism $f \colon K \to L$ between division rings (or fields) is equal to the image of the entire field $K$ (as the top subfield $\top$) under $f$. In other words, $f.\text{fieldRange} = \text{map}(f, \top)$.

RingHom.map_fieldRange theorem

: f.fieldRange.map g = (g.comp f).fieldRange

Full source

theorem map_fieldRange : f.fieldRange.map g = (g.comp f).fieldRange := by
  simpa only [fieldRange_eq_map] using (⊤ : Subfield K).map_map g f

Image of Field Range under Composition: $g(f.\text{fieldRange}) = (g \circ f).\text{fieldRange}$

Informal description

For ring homomorphisms $f \colon K \to L$ and $g \colon L \to M$ between division rings (or fields), the image of the range of $f$ under $g$ equals the range of the composition $g \circ f$. In symbols: $$g(f.\text{fieldRange}) = (g \circ f).\text{fieldRange}.$$

RingHom.mem_fieldRange_self theorem

(x : K) : f x ∈ f.fieldRange

Full source

theorem mem_fieldRange_self (x : K) : f x ∈ f.fieldRange :=
  exists_apply_eq_apply _ _

Image of Element Belongs to Field Range of Ring Homomorphism

Informal description

For any ring homomorphism $f \colon K \to L$ between division rings and any element $x \in K$, the image $f(x)$ belongs to the range of $f$ (viewed as a subfield of $L$).

RingHom.fieldRange_eq_top_iff theorem

{f : K →+* L} : f.fieldRange = ⊤ ↔ Function.Surjective f

Full source

theorem fieldRange_eq_top_iff {f : K →+* L} :
    f.fieldRange = ⊤ ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans Set.range_eq_univ

Range of Ring Homomorphism is Entire Field iff Surjective

Informal description

For a ring homomorphism $f \colon K \to L$ between division rings, the range of $f$ is equal to the entire field $L$ if and only if $f$ is surjective. In other words, $f.\text{fieldRange} = \top \leftrightarrow \text{Surjective}(f)$.

RingHom.fintypeFieldRange instance

[Fintype K] [DecidableEq L] (f : K →+* L) : Fintype f.fieldRange

Full source

/-- The range of a morphism of fields is a fintype, if the domain is a fintype.

Note that this instance can cause a diamond with `Subtype.Fintype` if `L` is also a fintype. -/
instance fintypeFieldRange [Fintype K] [DecidableEq L] (f : K →+* L) : Fintype f.fieldRange :=
  Set.fintypeRange f

Finiteness of the Range of a Ring Homomorphism between Finite Division Rings

Informal description

For any ring homomorphism $f \colon K \to L$ between division rings, if $K$ is finite and $L$ has decidable equality, then the range of $f$ is finite.

Subfield.instMin instance

: Min (Subfield K)

Full source

/-- The inf of two subfields is their intersection. -/
instance : Min (Subfield K) :=
  ⟨fun s t =>
    { s.toSubring ⊓ t.toSubring with
      inv_mem' := fun _ hx =>
        Subring.mem_inf.mpr
          ⟨s.inv_mem (Subring.mem_inf.mp hx).1, t.inv_mem (Subring.mem_inf.mp hx).2⟩ }⟩

Intersection of Subfields is a Subfield

Informal description

The intersection of two subfields of a division ring $K$ forms a subfield. For any two subfields $p$ and $p'$ of $K$, the infimum $p \sqcap p'$ is the subfield whose underlying set is the intersection of the underlying sets of $p$ and $p'$.

Subfield.coe_inf theorem

(p p' : Subfield K) : ((p ⊓ p' : Subfield K) : Set K) = p.carrier ∩ p'.carrier

Full source

@[simp]
theorem coe_inf (p p' : Subfield K) : ((p ⊓ p' : Subfield K) : Set K) = p.carrier ∩ p'.carrier :=
  rfl

Intersection of Subfields as Set Intersection

Informal description

For any two subfields $p$ and $p'$ of a division ring $K$, the underlying set of their intersection $p \sqcap p'$ is equal to the intersection of their underlying sets, i.e., $(p \sqcap p') = p \cap p'$.

Subfield.mem_inf theorem

{p p' : Subfield K} {x : K} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

Full source

@[simp]
theorem mem_inf {p p' : Subfield K} {x : K} : x ∈ p ⊓ p'x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p' :=
  Iff.rfl

Membership in Intersection of Subfields

Informal description

For any two subfields $p$ and $p'$ of a division ring $K$ and any element $x \in K$, $x$ belongs to the intersection $p \sqcap p'$ if and only if $x$ belongs to both $p$ and $p'$.

Subfield.instInfSet instance

: InfSet (Subfield K)

Full source

instance : InfSet (Subfield K) :=
  ⟨fun S =>
    { sInf (Subfield.toSubring '' S) with
      inv_mem' := by
        rintro x hx
        apply Subring.mem_sInf.mpr
        rintro _ ⟨p, p_mem, rfl⟩
        exact p.inv_mem (Subring.mem_sInf.mp hx p.toSubring ⟨p, p_mem, rfl⟩) }⟩

Complete Lattice Structure on Subfields of a Division Ring

Informal description

The collection of subfields of a division ring $K$ forms a complete lattice with respect to inclusion, where the infimum of a set of subfields is their intersection.

Subfield.coe_sInf theorem

(S : Set (Subfield K)) : ((sInf S : Subfield K) : Set K) = ⋂ s ∈ S, ↑s

Full source

@[simp, norm_cast]
theorem coe_sInf (S : Set (Subfield K)) : ((sInf S : Subfield K) : Set K) = ⋂ s ∈ S, ↑s :=
  show ((sInf (Subfield.toSubringSubfield.toSubring '' S) : Subring K) : Set K) = ⋂ s ∈ S, ↑s by
    ext x
    rw [Subring.coe_sInf, Set.mem_iInter, Set.mem_iInter]
    exact
      ⟨fun h s s' ⟨s_mem, s'_eq⟩ => h s.toSubring _ ⟨⟨s, s_mem, rfl⟩, s'_eq⟩,
        fun h s s' ⟨⟨s'', s''_mem, s_eq⟩, (s'_eq : ↑s = s')⟩ =>
        h s'' _ ⟨s''_mem, by simp [← s_eq, ← s'_eq]⟩⟩

Infimum of Subfields as Intersection of Underlying Sets

Informal description

For any collection $S$ of subfields of a division ring $K$, the underlying set of the infimum of $S$ is equal to the intersection of all the underlying sets of the subfields in $S$. That is, \[ \big(\inf S : \text{Subfield } K\big) = \bigcap_{s \in S} s. \]

Subfield.mem_sInf theorem

{S : Set (Subfield K)} {x : K} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Full source

theorem mem_sInf {S : Set (Subfield K)} {x : K} : x ∈ sInf Sx ∈ sInf S ↔ ∀ p ∈ S, x ∈ p :=
  Subring.mem_sInf.trans
    ⟨fun h p hp => h p.toSubring ⟨p, hp, rfl⟩, fun h _ ⟨p', hp', p_eq⟩ => p_eq ▸ h p' hp'⟩

Characterization of Membership in Intersection of Subfields

Informal description

For any collection $S$ of subfields of a division ring $K$ and any element $x \in K$, $x$ belongs to the infimum of $S$ (i.e., the intersection of all subfields in $S$) if and only if $x$ is contained in every subfield $p \in S$.

Subfield.coe_iInf theorem

{ι : Sort*} {S : ι → Subfield K} : (↑(⨅ i, S i) : Set K) = ⋂ i, S i

Full source

@[simp, norm_cast]
theorem coe_iInf {ι : Sort*} {S : ι → Subfield K} : (↑(⨅ i, S i) : Set K) = ⋂ i, S i := by
  simp only [iInf, coe_sInf, Set.biInter_range]

Infimum of Subfields as Intersection of Underlying Sets (Indexed Version)

Informal description

For any indexed family of subfields $(S_i)_{i \in \iota}$ of a division ring $K$, the underlying set of the infimum $\bigsqcap_i S_i$ is equal to the intersection $\bigcap_i S_i$ of the underlying sets of the subfields. That is, \[ \left(\bigsqcap_i S_i\right) = \bigcap_i S_i. \]

Subfield.mem_iInf theorem

{ι : Sort*} {S : ι → Subfield K} {x : K} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Full source

theorem mem_iInf {ι : Sort*} {S : ι → Subfield K} {x : K} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by
  simp only [iInf, mem_sInf, Set.forall_mem_range]

Characterization of Membership in Infimum of Subfields

Informal description

For any indexed family of subfields $(S_i)_{i \in \iota}$ of a division ring $K$ and any element $x \in K$, we have $x \in \bigsqcap_i S_i$ if and only if $x \in S_i$ for every $i \in \iota$.

Subfield.sInf_toSubring theorem

(s : Set (Subfield K)) : (sInf s).toSubring = ⨅ t ∈ s, Subfield.toSubring t

Full source

@[simp]
theorem sInf_toSubring (s : Set (Subfield K)) :
    (sInf s).toSubring = ⨅ t ∈ s, Subfield.toSubring t := by
  ext x
  simp [mem_sInf, ← sInf_image, Subring.mem_sInf]

Infimum of Subfields as Infimum of Subrings

Informal description

For any collection $s$ of subfields of a division ring $K$, the underlying subring of the infimum of $s$ is equal to the infimum of the underlying subrings of all subfields in $s$. That is, \[ (\bigsqcap s).\text{toSubring} = \bigsqcap_{t \in s} t.\text{toSubring}. \]

Subfield.isGLB_sInf theorem

(S : Set (Subfield K)) : IsGLB S (sInf S)

Full source

theorem isGLB_sInf (S : Set (Subfield K)) : IsGLB S (sInf S) := by
  have : ∀ {s t : Subfield K}, (s : Set K) ≤ t ↔ s ≤ t := by simp [SetLike.coe_subset_coe]
  refine IsGLB.of_image this ?_
  convert isGLB_biInf (s := S) (f := SetLike.coe)
  exact coe_sInf _

Infimum of Subfields is Greatest Lower Bound

Informal description

For any collection $S$ of subfields of a division ring $K$, the infimum $\bigsqcap S$ is the greatest lower bound of $S$ with respect to the partial order of subfield inclusion. That is, $\bigsqcap S$ is a lower bound for $S$ (i.e., $\bigsqcap S \leq T$ for all $T \in S$) and is greater than or equal to any other lower bound of $S$.

Subfield.instCompleteLattice instance

: CompleteLattice (Subfield K)

Full source

/-- Subfields of a ring form a complete lattice. -/
instance : CompleteLattice (Subfield K) :=
  { completeLatticeOfInf (Subfield K) isGLB_sInf with
    top := ⊤
    le_top := fun _ _ _ => trivial
    inf := (· ⊓ ·)
    inf_le_left := fun _ _ _ => And.left
    inf_le_right := fun _ _ _ => And.right
    le_inf := fun _ _ _ h₁ h₂ _ hx => ⟨h₁ hx, h₂ hx⟩ }

Complete Lattice Structure on Subfields of a Division Ring

Informal description

The collection of subfields of a division ring $K$ forms a complete lattice, where the partial order is given by inclusion, the infimum of a collection of subfields is their intersection, and the supremum is the subfield generated by their union.

Subfield.closure definition

(s : Set K) : Subfield K

Full source

/-- The `Subfield` generated by a set. -/
def closure (s : Set K) : Subfield K := sInf {S | s ⊆ S}

Subfield closure of a subset

Informal description

Given a subset $s$ of a division ring $K$, the subfield closure of $s$ is the smallest subfield of $K$ containing $s$, defined as the infimum of all subfields containing $s$.

Subfield.mem_closure theorem

{x : K} {s : Set K} : x ∈ closure s ↔ ∀ S : Subfield K, s ⊆ S → x ∈ S

Full source

theorem mem_closure {x : K} {s : Set K} : x ∈ closure sx ∈ closure s ↔ ∀ S : Subfield K, s ⊆ S → x ∈ S :=
  mem_sInf

Characterization of Membership in Subfield Closure

Informal description

For any element $x$ in a division ring $K$ and any subset $s \subseteq K$, $x$ belongs to the subfield closure of $s$ if and only if $x$ is contained in every subfield $S$ of $K$ that contains $s$.

Subfield.subset_closure theorem

{s : Set K} : s ⊆ closure s

Full source

/-- The subfield generated by a set includes the set. -/
@[simp, aesop safe 20 apply (rule_sets := [SetLike])]
theorem subset_closure {s : Set K} : s ⊆ closure s := fun _ hx => mem_closure.2 fun _ hS => hS hx

Subset is Contained in its Subfield Closure

Informal description

For any subset $s$ of a division ring $K$, the subfield closure of $s$ contains $s$, i.e., $s \subseteq \text{closure}(s)$.

Subfield.subring_closure_le theorem

(s : Set K) : Subring.closure s ≤ (closure s).toSubring

Full source

theorem subring_closure_le (s : Set K) : Subring.closure s ≤ (closure s).toSubring :=
  Subring.closure_le.mpr subset_closure

Subring Closure is Contained in Subfield Closure's Underlying Subring

Informal description

For any subset $s$ of a division ring $K$, the subring closure of $s$ is contained in the underlying subring of the subfield closure of $s$, i.e., $\text{Subring.closure}(s) \subseteq (\text{closure}(s)).\text{toSubring}$.

Subfield.not_mem_of_not_mem_closure theorem

{s : Set K} {P : K} (hP : P ∉ closure s) : P ∉ s

Full source

theorem not_mem_of_not_mem_closure {s : Set K} {P : K} (hP : P ∉ closure s) : P ∉ s := fun h =>
  hP (subset_closure h)

Non-membership in Subfield Closure Implies Non-membership in Subset

Informal description

For any subset $s$ of a division ring $K$ and any element $P \in K$, if $P$ is not in the subfield closure of $s$, then $P$ is not in $s$.

Subfield.closure_le theorem

{s : Set K} {t : Subfield K} : closure s ≤ t ↔ s ⊆ t

Full source

/-- A subfield `t` includes `closure s` if and only if it includes `s`. -/
@[simp]
theorem closure_le {s : Set K} {t : Subfield K} : closureclosure s ≤ t ↔ s ⊆ t :=
  ⟨Set.Subset.trans subset_closure, fun h _ hx => mem_closure.mp hx t h⟩

Subfield Closure Containment Criterion: $\text{closure}(s) \leq t \leftrightarrow s \subseteq t$

Informal description

For any subset $s$ of a division ring $K$ and any subfield $t$ of $K$, the subfield closure of $s$ is contained in $t$ if and only if $s$ is a subset of $t$.

Subfield.closure_mono theorem

⦃s t : Set K⦄ (h : s ⊆ t) : closure s ≤ closure t

Full source

/-- Subfield closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure s ≤ closure t`. -/
@[gcongr]
theorem closure_mono ⦃s t : Set K⦄ (h : s ⊆ t) : closure s ≤ closure t :=
  closure_le.2 <| Set.Subset.trans h subset_closure

Monotonicity of Subfield Closure: $s \subseteq t \Rightarrow \text{closure}(s) \leq \text{closure}(t)$

Informal description

For any subsets $s$ and $t$ of a division ring $K$, if $s \subseteq t$, then the subfield closure of $s$ is contained in the subfield closure of $t$, i.e., $\text{closure}(s) \leq \text{closure}(t)$.

Subfield.closure_eq_of_le theorem

{s : Set K} {t : Subfield K} (h₁ : s ⊆ t) (h₂ : t ≤ closure s) : closure s = t

Full source

theorem closure_eq_of_le {s : Set K} {t : Subfield K} (h₁ : s ⊆ t) (h₂ : t ≤ closure s) :
    closure s = t :=
  le_antisymm (closure_le.2 h₁) h₂

Subfield Closure Equality Criterion: $\text{closure}(s) = t$ under containment conditions

Informal description

For any subset $s$ of a division ring $K$ and any subfield $t$ of $K$, if $s$ is contained in $t$ and $t$ is contained in the subfield closure of $s$, then the closure of $s$ is equal to $t$.

Subfield.closure_induction theorem

 {s : Set K} {p : ∀ x ∈ closure s, Prop} (mem : ∀ x hx, p x (subset_closure hx)) (one : p 1 (one_mem _))
  (add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem hx hy)) (neg : ∀ x hx, p x hx → p (-x) (neg_mem hx))
  (inv : ∀ x hx, p x hx → p x⁻¹ (inv_mem hx)) (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) {x}
  (h : x ∈ closure s) : p x h

Full source

/-- An induction principle for closure membership. If `p` holds for `1`, and all elements
of `s`, and is preserved under addition, negation, and multiplication, then `p` holds for all
elements of the closure of `s`. -/
@[elab_as_elim]
theorem closure_induction {s : Set K} {p : ∀ x ∈ closure s, Prop}
    (mem : ∀ x hx, p x (subset_closure hx))
    (one : p 1 (one_mem _)) (add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem hx hy))
    (neg : ∀ x hx, p x hx → p (-x) (neg_mem hx)) (inv : ∀ x hx, p x hx → p x⁻¹ (inv_mem hx))
    (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
    {x} (h : x ∈ closure s) : p x h :=
  letI : Subfield K :=
    { carrier := {x | ∃ hx, p x hx}
      mul_mem' := by rintro _ _ ⟨_, hx⟩ ⟨_, hy⟩; exact ⟨_, mul _ _ _ _ hx hy⟩
      one_mem' := ⟨_, one⟩
      add_mem' := by rintro _ _ ⟨_, hx⟩ ⟨_, hy⟩; exact ⟨_, add _ _ _ _ hx hy⟩
      zero_mem' := ⟨zero_mem _, by
        simp_rw [← @add_neg_cancel K _ 1]; exact add _ _ _ _ one (neg _ _ one)⟩
      neg_mem' := by rintro _ ⟨_, hx⟩; exact ⟨_, neg _ _ hx⟩
      inv_mem' := by rintro _ ⟨_, hx⟩; exact ⟨_, inv _ _ hx⟩ }
  ((closure_le (t := this)).2 (fun x hx ↦ ⟨_, mem x hx⟩) h).2

Induction Principle for Subfield Closure Membership

Informal description

Let $K$ be a division ring and $s \subseteq K$ a subset. Consider a predicate $p$ defined on the subfield closure of $s$ (i.e., for all $x \in \text{closure}(s)$, $p(x)$ is a proposition). Suppose the following conditions hold: 1. $p$ holds for all elements of $s$ (i.e., $\forall x \in s, p(x)$), 2. $p(1)$ holds, 3. $p$ is preserved under addition (i.e., $\forall x y \in \text{closure}(s), p(x) \land p(y) \to p(x + y)$), 4. $p$ is preserved under negation (i.e., $\forall x \in \text{closure}(s), p(x) \to p(-x)$), 5. $p$ is preserved under inversion (i.e., $\forall x \in \text{closure}(s), p(x) \to p(x^{-1})$), 6. $p$ is preserved under multiplication (i.e., $\forall x y \in \text{closure}(s), p(x) \land p(y) \to p(x y)$). Then $p(x)$ holds for all $x \in \text{closure}(s)$.

Subfield.gi definition

: GaloisInsertion (@closure K _) (↑)

Full source

/-- `closure` forms a Galois insertion with the coercion to set. -/
protected def gi : GaloisInsertion (@closure K _) (↑) where
  choice s _ := closure s
  gc _ _ := closure_le
  le_l_u _ := subset_closure
  choice_eq _ _ := rfl

Galois insertion between subfield closure and coercion

Informal description

The pair of functions `closure : Set K → Subfield K` (subfield closure) and the coercion `(↑) : Subfield K → Set K` (forgetting the subfield structure) form a Galois insertion. This means: 1. For any subset $s$ of $K$ and any subfield $t$ of $K$, we have $\text{closure}(s) \leq t$ if and only if $s \subseteq t$ (as sets). 2. For any subfield $t$, we have $t \subseteq \text{closure}(t)$ (as sets). 3. The closure operation is idempotent: $\text{closure}(\text{closure}(s)) = \text{closure}(s)$ for any subset $s$.

Subfield.closure_eq theorem

(s : Subfield K) : closure (s : Set K) = s

Full source

/-- Closure of a subfield `S` equals `S`. -/
@[simp]
theorem closure_eq (s : Subfield K) : closure (s : Set K) = s :=
  (Subfield.gi K).l_u_eq s

Subfield Closure of a Subfield is Itself

Informal description

For any subfield $s$ of a division ring $K$, the subfield closure of the underlying set of $s$ is equal to $s$ itself. In other words, $\text{closure}(s) = s$.

Subfield.closure_empty theorem

: closure (∅ : Set K) = ⊥

Full source

@[simp]
theorem closure_empty : closure (∅ : Set K) = ⊥ :=
  (Subfield.gi K).gc.l_bot

Subfield Closure of Empty Set is Trivial Subfield

Informal description

The subfield closure of the empty set in a division ring $K$ is the trivial subfield $\bot$.

Subfield.closure_univ theorem

: closure (Set.univ : Set K) = ⊤

Full source

@[simp]
theorem closure_univ : closure (Set.univ : Set K) = ⊤ :=
  @coe_top K _ ▸ closure_eq ⊤

Subfield Closure of Universal Set is Top Subfield

Informal description

The subfield closure of the universal set in a division ring $K$ is equal to the top subfield, i.e., $\text{closure}(\text{univ}) = \top$.

Subfield.closure_union theorem

(s t : Set K) : closure (s ∪ t) = closure s ⊔ closure t

Full source

theorem closure_union (s t : Set K) : closure (s ∪ t) = closureclosure s ⊔ closure t :=
  (Subfield.gi K).gc.l_sup

Subfield Closure of Union Equals Supremum of Closures

Informal description

For any two subsets $s$ and $t$ of a division ring $K$, the subfield closure of their union $s \cup t$ equals the supremum of their individual closures, i.e., $\text{closure}(s \cup t) = \text{closure}(s) \sqcup \text{closure}(t)$.

Subfield.closure_iUnion theorem

{ι} (s : ι → Set K) : closure (⋃ i, s i) = ⨆ i, closure (s i)

Full source

theorem closure_iUnion {ι} (s : ι → Set K) : closure (⋃ i, s i) = ⨆ i, closure (s i) :=
  (Subfield.gi K).gc.l_iSup

Subfield Closure of Union Equals Supremum of Closures

Informal description

Let $K$ be a division ring and $\{s_i\}_{i \in \iota}$ be a family of subsets of $K$. The subfield closure of the union $\bigcup_{i} s_i$ is equal to the supremum of the subfield closures of each $s_i$, i.e., \[ \text{closure}\left(\bigcup_{i} s_i\right) = \bigsqcup_{i} \text{closure}(s_i). \]

Subfield.closure_sUnion theorem

(s : Set (Set K)) : closure (⋃₀ s) = ⨆ t ∈ s, closure t

Full source

theorem closure_sUnion (s : Set (Set K)) : closure (⋃₀ s) = ⨆ t ∈ s, closure t :=
  (Subfield.gi K).gc.l_sSup

Subfield Closure of Union Equals Supremum of Closures

Informal description

For any collection $s$ of subsets of a division ring $K$, the subfield closure of the union of all sets in $s$ is equal to the supremum of the subfield closures of each individual set in $s$. That is, \[ \text{closure}\left(\bigcup_{t \in s} t\right) = \bigsqcup_{t \in s} \text{closure}(t). \]

Subfield.map_sup theorem

(s t : Subfield K) (f : K →+* L) : (s ⊔ t).map f = s.map f ⊔ t.map f

Full source

theorem map_sup (s t : Subfield K) (f : K →+* L) : (s ⊔ t).map f = s.map f ⊔ t.map f :=
  (gc_map_comap f).l_sup

Image of Subfield Supremum under Ring Homomorphism Equals Supremum of Images

Informal description

Let $K$ and $L$ be division rings, and let $f \colon K \to L$ be a ring homomorphism. For any two subfields $s$ and $t$ of $K$, the image of their supremum under $f$ equals the supremum of their images. That is, \[ f(s \sqcup t) = f(s) \sqcup f(t). \]

Subfield.map_iSup theorem

{ι : Sort*} (f : K →+* L) (s : ι → Subfield K) : (iSup s).map f = ⨆ i, (s i).map f

Full source

theorem map_iSup {ι : Sort*} (f : K →+* L) (s : ι → Subfield K) :
    (iSup s).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f).l_iSup

Image of Supremum of Subfields under Ring Homomorphism Equals Supremum of Images

Informal description

Let $K$ and $L$ be division rings, and let $f : K \to L$ be a ring homomorphism. For any family of subfields $(S_i)_{i \in \iota}$ of $K$, the image of their supremum under $f$ equals the supremum of their images. That is, \[ f\left(\bigsqcup_{i \in \iota} S_i\right) = \bigsqcup_{i \in \iota} f(S_i). \]

Subfield.map_inf theorem

(s t : Subfield K) (f : K →+* L) : (s ⊓ t).map f = s.map f ⊓ t.map f

Full source

theorem map_inf (s t : Subfield K) (f : K →+* L) : (s ⊓ t).map f = s.map f ⊓ t.map f :=
  SetLike.coe_injective (Set.image_inter f.injective)

Image of Subfield Intersection under Ring Homomorphism Equals Intersection of Images

Informal description

Let $K$ and $L$ be division rings, and let $f : K \to L$ be a ring homomorphism. For any two subfields $s$ and $t$ of $K$, the image of their intersection under $f$ equals the intersection of their images. That is, \[ f(s \sqcap t) = f(s) \sqcap f(t). \]

Subfield.map_iInf theorem

{ι : Sort*} [Nonempty ι] (f : K →+* L) (s : ι → Subfield K) : (iInf s).map f = ⨅ i, (s i).map f

Full source

theorem map_iInf {ι : Sort*} [Nonempty ι] (f : K →+* L) (s : ι → Subfield K) :
    (iInf s).map f = ⨅ i, (s i).map f := by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective f.injective).image_iInter_eq (s := SetLike.coeSetLike.coe ∘ s)

Image of Infimum of Subfields under Ring Homomorphism Equals Infimum of Images

Informal description

Let $K$ and $L$ be division rings, and let $f : K \to L$ be a ring homomorphism. Given a nonempty index set $\iota$ and a family of subfields $(S_i)_{i \in \iota}$ of $K$, the image of their infimum under $f$ equals the infimum of their images. That is, \[ f\left(\bigsqcap_{i \in \iota} S_i\right) = \bigsqcap_{i \in \iota} f(S_i). \]

Subfield.comap_inf theorem

(s t : Subfield L) (f : K →+* L) : (s ⊓ t).comap f = s.comap f ⊓ t.comap f

Full source

theorem comap_inf (s t : Subfield L) (f : K →+* L) : (s ⊓ t).comap f = s.comap f ⊓ t.comap f :=
  (gc_map_comap f).u_inf

Preimage of Subfield Intersection Equals Intersection of Preimages

Informal description

Let $K$ and $L$ be division rings, and let $f : K \to L$ be a ring homomorphism. For any two subfields $s$ and $t$ of $L$, the preimage of their intersection under $f$ equals the intersection of their preimages. That is, \[ f^{-1}(s \sqcap t) = f^{-1}(s) \sqcap f^{-1}(t). \]

Subfield.comap_iInf theorem

{ι : Sort*} (f : K →+* L) (s : ι → Subfield L) : (iInf s).comap f = ⨅ i, (s i).comap f

Full source

theorem comap_iInf {ι : Sort*} (f : K →+* L) (s : ι → Subfield L) :
    (iInf s).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f).u_iInf

Preimage of Infimum of Subfields Equals Infimum of Preimages

Informal description

Let $K$ and $L$ be division rings, and let $f : K \to L$ be a ring homomorphism. For any family of subfields $(S_i)_{i \in \iota}$ of $L$, the preimage of their infimum under $f$ equals the infimum of their preimages. That is, \[ f^{-1}\left(\bigsqcap_{i \in \iota} S_i\right) = \bigsqcap_{i \in \iota} f^{-1}(S_i). \]

Subfield.map_bot theorem

(f : K →+* L) : (⊥ : Subfield K).map f = ⊥

Full source

@[simp]
theorem map_bot (f : K →+* L) : (⊥ : Subfield K).map f = ⊥ :=
  (gc_map_comap f).l_bot

Image of Bottom Subfield is Bottom Subfield

Informal description

For any ring homomorphism $f \colon K \to L$ between division rings (or fields), the image of the bottom subfield $\bot$ of $K$ under $f$ is the bottom subfield $\bot$ of $L$.

Subfield.comap_top theorem

(f : K →+* L) : (⊤ : Subfield L).comap f = ⊤

Full source

@[simp]
theorem comap_top (f : K →+* L) : (⊤ : Subfield L).comap f = ⊤ :=
  (gc_map_comap f).u_top

Preimage of Top Subfield is Top Subfield

Informal description

For any ring homomorphism $f \colon K \to L$ between division rings (or fields), the preimage of the top subfield of $L$ (which is $L$ itself) under $f$ is the top subfield of $K$ (which is $K$ itself). In other words, $f^{-1}(L) = K$.

Subfield.mem_iSup_of_directed theorem

 {ι} [hι : Nonempty ι] {S : ι → Subfield K} (hS : Directed (· ≤ ·) S) {x : K} : (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i

Full source

/-- The underlying set of a non-empty directed sSup of subfields is just a union of the subfields.
  Note that this fails without the directedness assumption (the union of two subfields is
  typically not a subfield) -/
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Subfield K} (hS : Directed (· ≤ ·) S)
    {x : K} : (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i := by
  let s : Subfield K :=
    { __ := Subring.copy _ _ (Subring.coe_iSup_of_directed hS).symm
      inv_mem' := fun _ hx ↦ have ⟨i, hi⟩ := Set.mem_iUnion.mp hx
        Set.mem_iUnion.mpr ⟨i, (S i).inv_mem hi⟩ }
  have : iSup S = s := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set K)) i) (Set.iUnion_subset fun _ ↦ le_iSup S _)
  exact this ▸ Set.mem_iUnion

Characterization of Membership in Directed Supremum of Subfields

Informal description

Let $K$ be a division ring, $\iota$ a nonempty index set, and $S : \iota \to \text{Subfield } K$ a directed family of subfields of $K$. For any element $x \in K$, we have $x \in \bigsqcup_{i \in \iota} S_i$ if and only if there exists an index $i \in \iota$ such that $x \in S_i$.

Subfield.coe_iSup_of_directed theorem

 {ι} [hι : Nonempty ι] {S : ι → Subfield K} (hS : Directed (· ≤ ·) S) : ((⨆ i, S i : Subfield K) : Set K) = ⋃ i, ↑(S i)

Full source

theorem coe_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Subfield K} (hS : Directed (· ≤ ·) S) :
    ((⨆ i, S i : Subfield K) : Set K) = ⋃ i, ↑(S i) :=
  Set.ext fun x => by simp [mem_iSup_of_directed hS]

Supremum of Directed Family of Subfields as Union of Underlying Sets

Informal description

Let $K$ be a division ring, $\iota$ a nonempty index set, and $S : \iota \to \text{Subfield } K$ a directed family of subfields of $K$. Then the underlying set of the supremum $\bigsqcup_{i \in \iota} S_i$ is equal to the union $\bigcup_{i \in \iota} S_i$ of the underlying sets of the subfields in the family.

Subfield.mem_sSup_of_directedOn theorem

 {S : Set (Subfield K)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S) {x : K} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Full source

theorem mem_sSup_of_directedOn {S : Set (Subfield K)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S)
    {x : K} : x ∈ sSup Sx ∈ sSup S ↔ ∃ s ∈ S, x ∈ s := by
  haveI : Nonempty S := Sne.to_subtype
  simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]

Characterization of Membership in Directed Supremum of Subfields via Subfield Membership

Informal description

Let $K$ be a division ring and $S$ a nonempty set of subfields of $K$ that is directed with respect to inclusion. For any element $x \in K$, we have $x \in \mathrm{sSup}(S)$ if and only if there exists a subfield $s \in S$ such that $x \in s$.

Subfield.coe_sSup_of_directedOn theorem

{S : Set (Subfield K)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set K) = ⋃ s ∈ S, ↑s

Full source

theorem coe_sSup_of_directedOn {S : Set (Subfield K)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set K) = ⋃ s ∈ S, ↑s :=
  Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]

Supremum of Directed Set of Subfields as Union of Underlying Sets

Informal description

Let $K$ be a division ring and $S$ a nonempty set of subfields of $K$ that is directed with respect to inclusion. Then the underlying set of the supremum $\mathrm{sSup}(S)$ is equal to the union $\bigcup_{s \in S} s$ of the underlying sets of the subfields in $S$.

RingHom.rangeRestrictField definition

(f : K →+* L) : K →+* f.fieldRange

Full source

/-- Restriction of a ring homomorphism to its range interpreted as a subfield. -/
def rangeRestrictField (f : K →+* L) : K →+* f.fieldRange :=
  f.rangeSRestrict

Restriction of a ring homomorphism to its range subfield

Informal description

Given a ring homomorphism $f : K \to L$ between division rings (or fields), the function restricts $f$ to its range, yielding a ring homomorphism from $K$ to the subfield $\text{fieldRange}(f) \subseteq L$ consisting of all elements in the image of $f$.

RingHom.coe_rangeRestrictField theorem

(f : K →+* L) (x : K) : (f.rangeRestrictField x : L) = f x

Full source

@[simp]
theorem coe_rangeRestrictField (f : K →+* L) (x : K) : (f.rangeRestrictField x : L) = f x :=
  rfl

Equality of Restricted and Original Ring Homomorphism Values

Informal description

For any ring homomorphism $f : K \to L$ between division rings (or fields) and any element $x \in K$, the image of $x$ under the restricted homomorphism $f.\text{rangeRestrictField}$ (viewed as an element of $L$) equals $f(x)$. In other words, the following diagram commutes: $$(f.\text{rangeRestrictField}(x) : L) = f(x)$$

RingHom.rangeRestrictField_bijective theorem

(f : K →+* L) : Function.Bijective (rangeRestrictField f)

Full source

theorem rangeRestrictField_bijective (f : K →+* L) : Function.Bijective (rangeRestrictField f) :=
  (Equiv.ofInjective f f.injective).bijective

Bijectivity of the Range-Restricted Ring Homomorphism

Informal description

For any ring homomorphism $f \colon K \to L$ between division rings (or fields), the restricted homomorphism $\mathrm{rangeRestrictField}\, f \colon K \to \mathrm{fieldRange}\, f$ is bijective. That is, it is both injective and surjective onto its range subfield.

RingHom.eqLocusField definition

(f g : K →+* L) : Subfield K

Full source

/-- The subfield of elements `x : R` such that `f x = g x`, i.e.,
the equalizer of f and g as a subfield of R -/
def eqLocusField (f g : K →+* L) : Subfield K where
  __ := (f : K →+* L).eqLocus g
  inv_mem' _ := eq_on_inv₀ f g
  carrier := { x | f x = g x }

Equalizer subfield of ring homomorphisms

Informal description

Given two ring homomorphisms $ f, g : K \to L $ between division rings (or fields), the subfield of $ K $ consisting of all elements $ x $ such that $ f(x) = g(x) $. This is the equalizer of $ f $ and $ g $ viewed as a subfield of $ K $.

RingHom.eqOn_field_closure theorem

{f g : K →+* L} {s : Set K} (h : Set.EqOn f g s) : Set.EqOn f g (closure s)

Full source

/-- If two ring homomorphisms are equal on a set, then they are equal on its subfield closure. -/
theorem eqOn_field_closure {f g : K →+* L} {s : Set K} (h : Set.EqOn f g s) :
    Set.EqOn f g (closure s) :=
  show closure s ≤ f.eqLocusField g from closure_le.2 h

Agreement of Ring Homomorphisms on Subfield Closure

Informal description

Let $K$ and $L$ be division rings (or fields), and let $f, g \colon K \to L$ be ring homomorphisms. If $f$ and $g$ agree on a subset $s \subseteq K$, then they also agree on the subfield closure of $s$ in $K$.

RingHom.field_closure_preimage_le theorem

(f : K →+* L) (s : Set L) : closure (f ⁻¹' s) ≤ (closure s).comap f

Full source

theorem field_closure_preimage_le (f : K →+* L) (s : Set L) :
    closure (f ⁻¹' s) ≤ (closure s).comap f :=
  closure_le.2 fun _ hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx

Subfield Closure of Preimage is Contained in Preimage of Closure

Informal description

Let $K$ and $L$ be division rings, and let $f : K \to L$ be a ring homomorphism. For any subset $s \subseteq L$, the subfield closure of the preimage $f^{-1}(s)$ is contained in the preimage of the subfield closure of $s$ under $f$. In other words, $\text{closure}(f^{-1}(s)) \leq (\text{closure}(s)).\text{comap}(f)$.

RingHom.map_field_closure theorem

(f : K →+* L) (s : Set K) : (closure s).map f = closure (f '' s)

Full source

/-- The image under a ring homomorphism of the subfield generated by a set equals
the subfield generated by the image of the set. -/
theorem map_field_closure (f : K →+* L) (s : Set K) : (closure s).map f = closure (f '' s) :=
  Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Subfield.gi L).gc (Subfield.gi K).gc
    fun _ ↦ rfl

Image of Subfield Closure Equals Closure of Image

Informal description

Let $K$ and $L$ be division rings (or fields), and let $f : K \to L$ be a ring homomorphism. For any subset $s \subseteq K$, the image under $f$ of the subfield closure of $s$ in $K$ is equal to the subfield closure of the image $f(s)$ in $L$. In other words: \[ f(\text{closure}(s)) = \text{closure}(f(s)) \] where $\text{closure}(s)$ denotes the smallest subfield of $K$ containing $s$, and $f(s)$ denotes the image of $s$ under $f$.

Subfield.inclusion definition

{S T : Subfield K} (h : S ≤ T) : S →+* T

Full source

/-- The ring homomorphism associated to an inclusion of subfields. -/
def inclusion {S T : Subfield K} (h : S ≤ T) : S →+* T :=
  S.subtype.codRestrict _ fun x => h x.2

Inclusion homomorphism between subfields

Informal description

Given two subfields $S$ and $T$ of a division ring $K$ with $S \subseteq T$, the inclusion map $S \hookrightarrow T$ is a ring homomorphism that preserves both the additive and multiplicative structures.

Subfield.fieldRange_subtype theorem

(s : Subfield K) : s.subtype.fieldRange = s

Full source

@[simp]
theorem fieldRange_subtype (s : Subfield K) : s.subtype.fieldRange = s :=
  SetLike.ext' <| (coe_rangeS _).trans Subtype.range_coe

Range of Subfield Inclusion Equals Subfield

Informal description

For any subfield $s$ of a division ring $K$, the range of the canonical inclusion ring homomorphism $s \hookrightarrow K$ is equal to $s$ itself. In other words, the image of the subfield under its inclusion map is the subfield itself.

RingEquiv.subfieldCongr definition

(h : s = t) : s ≃+* t

Full source

/-- Makes the identity isomorphism from a proof two subfields of a multiplicative
    monoid are equal. -/
def subfieldCongr (h : s = t) : s ≃+* t :=
  { Equiv.setCongr <| SetLike.ext'_iff.1 h with
    map_mul' := fun _ _ => rfl
    map_add' := fun _ _ => rfl }

Ring isomorphism between equal subfields

Informal description

Given two subfields $s$ and $t$ of a division ring $K$ that are equal ($s = t$), the ring equivalence (isomorphism) between them is defined by the identity map, preserving both multiplication and addition.

Subfield.closure_preimage_le theorem

(f : K →+* L) (s : Set L) : closure (f ⁻¹' s) ≤ (closure s).comap f

Full source

theorem closure_preimage_le (f : K →+* L) (s : Set L) : closure (f ⁻¹' s) ≤ (closure s).comap f :=
  closure_le.2 fun _ hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx

Subfield Closure of Preimage is Contained in Preimage of Closure

Informal description

For any ring homomorphism $f \colon K \to L$ and any subset $s \subseteq L$, the subfield closure of the preimage $f^{-1}(s)$ is contained in the preimage of the subfield closure of $s$ under $f$. In other words, $\text{closure}(f^{-1}(s)) \leq (\text{closure}(s)).\text{comap}\, f$.

Subfield.multiset_prod_mem theorem

(m : Multiset K) : (∀ a ∈ m, a ∈ s) → m.prod ∈ s

Full source

/-- Product of a multiset of elements in a subfield is in the subfield. -/
protected theorem multiset_prod_mem (m : Multiset K) : (∀ a ∈ m, a ∈ s) → m.prod ∈ s :=
  multiset_prod_mem m

Subfield Closure Under Multiset Product

Informal description

Let $K$ be a division ring and $s$ a subfield of $K$. For any multiset $m$ of elements in $K$, if every element $a \in m$ belongs to $s$, then the product of all elements in $m$ (computed in $K$) also belongs to $s$.

Subfield.prod_mem theorem

{ι : Type*} {t : Finset ι} {f : ι → K} (h : ∀ c ∈ t, f c ∈ s) : (∏ i ∈ t, f i) ∈ s

Full source

/-- Product of elements of a subfield indexed by a `Finset` is in the subfield. -/
protected theorem prod_mem {ι : Type*} {t : Finset ι} {f : ι → K} (h : ∀ c ∈ t, f c ∈ s) :
    (∏ i ∈ t, f i) ∈ s :=
  prod_mem h

Product of Subfield Elements over a Finite Set Belongs to Subfield

Informal description

Let $K$ be a division ring and $s$ a subfield of $K$. For any finite index set $t$ and function $f : \iota \to K$, if $f(c) \in s$ for every $c \in t$, then the product $\prod_{i \in t} f(i)$ belongs to $s$.

Subfield.toAlgebra instance

: Algebra s K

Full source

instance toAlgebra : Algebra s K :=
  RingHom.toAlgebra s.subtype

Algebra Structure on Subfields

Informal description

For any subfield $s$ of a division ring $K$, there is a canonical algebra structure on $s$ over $K$.

Subfield.mem_closure_iff theorem

{s : Set K} {x} : x ∈ closure s ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x

Full source

theorem mem_closure_iff {s : Set K} {x} :
    x ∈ closure sx ∈ closure s ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x := by
  rw [← commClosure_eq_closure]; rfl

Characterization of Elements in Subfield Closure via Subring Closure

Informal description

Let $K$ be a division ring and $s \subseteq K$ a subset. An element $x \in K$ belongs to the subfield closure of $s$ if and only if there exist elements $y, z$ in the subring closure of $s$ such that $x = y / z$.

Subfield.map_comap_eq theorem

(f : K →+* L) (s : Subfield L) : (s.comap f).map f = s ⊓ f.fieldRange

Full source

theorem map_comap_eq (f : K →+* L) (s : Subfield L) : (s.comap f).map f = s ⊓ f.fieldRange :=
  SetLike.coe_injective Set.image_preimage_eq_inter_range

Image-Preimage Equality for Subfields: $f(f^{-1}(s)) = s \cap \mathrm{range}(f)$

Informal description

For any ring homomorphism $f : K \to L$ between division rings (or fields) and any subfield $s$ of $L$, the image under $f$ of the preimage of $s$ under $f$ equals the intersection of $s$ with the range of $f$. That is, $f(f^{-1}(s)) = s \cap \mathrm{range}(f)$.

Subfield.map_comap_eq_self theorem

{f : K →+* L} {s : Subfield L} (h : s ≤ f.fieldRange) : (s.comap f).map f = s

Full source

theorem map_comap_eq_self
    {f : K →+* L} {s : Subfield L} (h : s ≤ f.fieldRange) : (s.comap f).map f = s := by
  simpa only [inf_of_le_left h] using map_comap_eq f s

Image-Preimage Equality for Subfields Contained in Range: $f(f^{-1}(s)) = s$

Informal description

Let $K$ and $L$ be division rings (or fields), and let $f : K \to L$ be a ring homomorphism. For any subfield $s$ of $L$ that is contained in the range of $f$, the image under $f$ of the preimage of $s$ under $f$ equals $s$ itself, i.e., $f(f^{-1}(s)) = s$.

Subfield.map_comap_eq_self_of_surjective theorem

{f : K →+* L} (hf : Function.Surjective f) (s : Subfield L) : (s.comap f).map f = s

Full source

theorem map_comap_eq_self_of_surjective
    {f : K →+* L} (hf : Function.Surjective f) (s : Subfield L) : (s.comap f).map f = s :=
  SetLike.coe_injective (Set.image_preimage_eq _ hf)

Image-Preimage Equality for Subfields under Surjective Ring Homomorphisms: $f(f^{-1}(s)) = s$

Informal description

Let $K$ and $L$ be division rings (or fields), and let $f : K \to L$ be a surjective ring homomorphism. For any subfield $s$ of $L$, the image under $f$ of the preimage of $s$ under $f$ equals $s$ itself, i.e., \[ f(f^{-1}(s)) = s. \]

Subfield.comap_map theorem

(f : K →+* L) (s : Subfield K) : (s.map f).comap f = s

Full source

theorem comap_map (f : K →+* L) (s : Subfield K) : (s.map f).comap f = s :=
  SetLike.coe_injective (Set.preimage_image_eq _ f.injective)

Preimage-Image Equality for Subfields under Ring Homomorphisms: $f^{-1}(f(s)) = s$

Informal description

Let $K$ and $L$ be division rings (or fields), and let $f : K \to L$ be a ring homomorphism. For any subfield $s$ of $K$, the preimage of the image of $s$ under $f$ equals $s$ itself, i.e., $f^{-1}(f(s)) = s$.

Subfield.instSMulSubtypeMem instance

[SMul K X] (F : Subfield K) : SMul F X

Full source

/-- The action by a subfield is the action by the underlying field. -/
instance [SMul K X] (F : Subfield K) : SMul F X :=
  inferInstanceAs (SMul F.toSubsemiring X)

Scalar Multiplication Action Inherited from Subfield Inclusion

Informal description

For any type $X$ with a scalar multiplication action by a division ring $K$, and any subfield $F$ of $K$, $X$ inherits a scalar multiplication action by $F$ via the inclusion map $F \hookrightarrow K$.

Subfield.smul_def theorem

[SMul K X] {F : Subfield K} (g : F) (m : X) : g • m = (g : K) • m

Full source

theorem smul_def [SMul K X] {F : Subfield K} (g : F) (m : X) : g • m = (g : K) • m :=
  rfl

Subfield scalar multiplication agrees with parent field

Informal description

For any type $X$ with a scalar multiplication action by a division ring $K$, and any subfield $F$ of $K$, the scalar multiplication of an element $g \in F$ on an element $m \in X$ is equal to the scalar multiplication of $g$ (viewed as an element of $K$) on $m$. In other words, $g \• m = (g : K) \• m$.

Subfield.smulCommClass_left instance

[SMul K Y] [SMul X Y] [SMulCommClass K X Y] (F : Subfield K) : SMulCommClass F X Y

Full source

instance smulCommClass_left [SMul K Y] [SMul X Y] [SMulCommClass K X Y] (F : Subfield K) :
    SMulCommClass F X Y :=
  inferInstanceAs (SMulCommClass F.toSubsemiring X Y)

Commutativity of Scalar Multiplication by Subfield and Another Type

Informal description

For any type $Y$ with scalar multiplication actions by both $K$ and $X$, if the scalar multiplications by $K$ and $X$ on $Y$ commute (i.e., $k \cdot (x \cdot y) = x \cdot (k \cdot y)$ for all $k \in K$, $x \in X$, $y \in Y$), then for any subfield $F$ of $K$, the scalar multiplications by $F$ and $X$ on $Y$ also commute.

Subfield.smulCommClass_right instance

[SMul X Y] [SMul K Y] [SMulCommClass X K Y] (F : Subfield K) : SMulCommClass X F Y

Full source

instance smulCommClass_right [SMul X Y] [SMul K Y] [SMulCommClass X K Y] (F : Subfield K) :
    SMulCommClass X F Y :=
  inferInstanceAs (SMulCommClass X F.toSubsemiring Y)

Commutativity of Scalar Multiplication with Subfield Actions

Informal description

For any type $Y$ with scalar multiplication actions by types $X$ and $K$, if the scalar multiplications by $X$ and $K$ on $Y$ commute (i.e., $x \cdot (k \cdot y) = k \cdot (x \cdot y)$ for all $x \in X$, $k \in K$, $y \in Y$), then for any subfield $F$ of $K$, the scalar multiplications by $X$ and $F$ on $Y$ also commute.

Subfield.instIsScalarTowerSubtypeMem instance

[SMul X Y] [SMul K X] [SMul K Y] [IsScalarTower K X Y] (F : Subfield K) : IsScalarTower F X Y

Full source

/-- Note that this provides `IsScalarTower F K K` which is needed by `smul_mul_assoc`. -/
instance [SMul X Y] [SMul K X] [SMul K Y] [IsScalarTower K X Y] (F : Subfield K) :
    IsScalarTower F X Y :=
  inferInstanceAs (IsScalarTower F.toSubsemiring X Y)

Scalar Tower Property for Subfield Actions

Informal description

For any division ring $K$ with scalar multiplication actions on types $X$ and $Y$ such that $K$ forms a scalar tower over $X$ and $Y$, and any subfield $F$ of $K$, the scalar multiplication actions of $F$ on $X$ and $Y$ also form a scalar tower. That is, for any $x \in F$, $y \in X$, and $z \in Y$, the equality $(x \cdot y) \cdot z = x \cdot (y \cdot z)$ holds, where $\cdot$ denotes the respective scalar multiplication operations.

Subfield.instFaithfulSMulSubtypeMem instance

[SMul K X] [FaithfulSMul K X] (F : Subfield K) : FaithfulSMul F X

Full source

instance [SMul K X] [FaithfulSMul K X] (F : Subfield K) : FaithfulSMul F X :=
  inferInstanceAs (FaithfulSMul F.toSubsemiring X)

Faithfulness of Scalar Multiplication Restricted to Subfields

Informal description

For any division ring $K$ with a faithful scalar multiplication action on a type $X$, and any subfield $F$ of $K$, the scalar multiplication action of $F$ on $X$ is also faithful. This means that if two elements of $F$ act identically on all elements of $X$, then they must be equal.

Subfield.instMulActionSubtypeMem instance

[MulAction K X] (F : Subfield K) : MulAction F X

Full source

/-- The action by a subfield is the action by the underlying field. -/
instance [MulAction K X] (F : Subfield K) : MulAction F X :=
  inferInstanceAs (MulAction F.toSubsemiring X)

Restriction of Multiplicative Action to Subfields

Informal description

For any division ring $K$ with a multiplicative action on a type $X$, and any subfield $F$ of $K$, the multiplicative action of $K$ on $X$ restricts to a multiplicative action of $F$ on $X$.

Subfield.instDistribMulActionSubtypeMem instance

[AddMonoid X] [DistribMulAction K X] (F : Subfield K) : DistribMulAction F X

Full source

/-- The action by a subfield is the action by the underlying field. -/
instance [AddMonoid X] [DistribMulAction K X] (F : Subfield K) : DistribMulAction F X :=
  inferInstanceAs (DistribMulAction F.toSubsemiring X)

Distributive Multiplicative Action Inherited by Subfields

Informal description

For any additive monoid $X$ with a distributive multiplicative action by a division ring $K$, and any subfield $F$ of $K$, the additive monoid $X$ inherits a distributive multiplicative action by $F$. This means that for any $a \in F$ and $x, y \in X$, the action satisfies $a \cdot (x + y) = a \cdot x + a \cdot y$ and $a \cdot 0 = 0$.

Subfield.instMulDistribMulActionSubtypeMem instance

[Monoid X] [MulDistribMulAction K X] (F : Subfield K) : MulDistribMulAction F X

Full source

/-- The action by a subfield is the action by the underlying field. -/
instance [Monoid X] [MulDistribMulAction K X] (F : Subfield K) : MulDistribMulAction F X :=
  inferInstanceAs (MulDistribMulAction F.toSubsemiring X)

Multiplicative Distributive Action Inherited by Subfields

Informal description

For any monoid $X$ with a multiplicative distributive action by a division ring $K$, and any subfield $F$ of $K$, the monoid $X$ inherits a multiplicative distributive action by $F$. This means that for any $a \in F$ and $x, y \in X$, the action satisfies $a \cdot (x * y) = (a \cdot x) * (a \cdot y)$.

Subfield.instSMulWithZeroSubtypeMem instance

[Zero X] [SMulWithZero K X] (F : Subfield K) : SMulWithZero F X

Full source

/-- The action by a subfield is the action by the underlying field. -/
instance [Zero X] [SMulWithZero K X] (F : Subfield K) : SMulWithZero F X :=
  inferInstanceAs (SMulWithZero F.toSubsemiring X)

Restriction of Scalar Multiplication with Zero to Subfields

Informal description

For any subfield $F$ of a division ring $K$ and any type $X$ with a zero element equipped with a scalar multiplication with zero by $K$, $X$ inherits a scalar multiplication with zero by $F$ where the action is defined by restricting the $K$-action to $F$.

Subfield.instMulActionWithZeroSubtypeMem instance

[Zero X] [MulActionWithZero K X] (F : Subfield K) : MulActionWithZero F X

Full source

/-- The action by a subfield is the action by the underlying field. -/
instance [Zero X] [MulActionWithZero K X] (F : Subfield K) : MulActionWithZero F X :=
  inferInstanceAs (MulActionWithZero F.toSubsemiring X)

Restriction of Multiplicative Action with Zero to Subfields

Informal description

For any subfield $F$ of a division ring $K$ and any type $X$ with a zero element equipped with a multiplicative action with zero by $K$, $X$ inherits a multiplicative action with zero by $F$ where the action is defined by restricting the $K$-action to $F$.

Subfield.instModuleSubtypeMem instance

[AddCommMonoid X] [Module K X] (F : Subfield K) : Module F X

Full source

/-- The action by a subfield is the action by the underlying field. -/
instance [AddCommMonoid X] [Module K X] (F : Subfield K) : Module F X :=
  inferInstanceAs (Module F.toSubsemiring X)

Module Structure on Subfields

Informal description

For any subfield $F$ of a division ring $K$ and any additive commutative monoid $X$ equipped with a module structure over $K$, $X$ inherits a module structure over $F$ where the scalar multiplication is defined by restricting the $K$-action to $F$.

Subfield.instMulSemiringActionSubtypeMem instance

[Semiring X] [MulSemiringAction K X] (F : Subfield K) : MulSemiringAction F X

Full source

/-- The action by a subfield is the action by the underlying field. -/
instance [Semiring X] [MulSemiringAction K X] (F : Subfield K) : MulSemiringAction F X :=
  inferInstanceAs (MulSemiringAction F.toSubsemiring X)

Restriction of Multiplicative Semiring Action to Subfields

Informal description

For any subfield $F$ of a division ring $K$ and any semiring $X$ equipped with a multiplicative semiring action by $K$, $X$ inherits a multiplicative semiring action by $F$ where the action is defined by restricting the $K$-action to $F$.

Mathlib.Algebra.Field.Subfield.Basic

Main definitions

Implementation notes

Tags