Closures

We define groupClosure, ringClosure, and fieldClosure, which represent the smallest nimber equal or greater to another, which satisfies IsGroup, IsRing, or IsField.

The analogous algClosure is defined in Nimber.SimplestExtension.Algebraic.

For Mathlib

@[simp]

theorem Subring.coe_eq_univ {R : Type u_1} [Ring R] {H : Subring R} : ↑H = Set.univ ↔ H = ⊤

@[simp]

theorem Subfield.coe_eq_univ {R : Type u_1} [Field R] {H : Subfield R} : ↑H = Set.univ ↔ H = ⊤

@[simp]

theorem Subfield.toSubring_eq_top {R : Type u_1} [Field R] {H : Subfield R} : H.toSubring = ⊤ ↔ H = ⊤

@[simp]

theorem Subfield.coe_bot {R : Type u_1} [DivisionRing R] : ↑⊥ = Set.range Rat.cast

instance Subfield.small_closure {R : Type u_1} (s : Set R) [DivisionRing R] [Small.{u, u_1} ↑s] : Small.{u, u_1} ↥(closure s)

instance Subfield.small_closure' {R : Type u_1} (s : Set R) [DivisionRing R] [Small.{u, u_1} ↑s] : Small.{u, u_1} ↑↑(closure s)

instance Nimber.instIsRegularCardinalOrder : IsRegularCardinalOrder Nimber

Groups

theorem Nimber.isGroup_sInf_compl (s : AddSubgroup Nimber) (hs : s ≠ ⊤) : (sInf (↑s)ᶜ).IsGroup

theorem Nimber.isLowerSet_addSubgroupClosure {s : Set Nimber} (hs : IsLowerSet s) : IsLowerSet ↑(AddSubgroup.closure s)

instance Nimber.small_addSubgroupClosure (s : Set Nimber) [Small.{u, u_1 + 1} ↑s] : Small.{u, u_1 + 1} ↥(AddSubgroup.closure s)

theorem Nimber.addSubgroupClosure_Iio_eq_Iio (x : Nimber) : ∃ (y : Nimber), ↑(AddSubgroup.closure (Set.Iio x)) = Set.Iio y

noncomputable def Nimber.groupClosure (x : Nimber) : Nimber

Returns the smallest IsGroup that's at least x.

Equations

• x.groupClosure = Classical.choose ⋯

@[simp]

theorem Nimber.coe_addSubgroupClosure_Iio (x : Nimber) : ↑(AddSubgroup.closure (Set.Iio x)) = Set.Iio x.groupClosure

@[simp]

theorem Nimber.mem_addSubgroupClosure_Iio {x y : Nimber} : y ∈ AddSubgroup.closure (Set.Iio x) ↔ y < x.groupClosure

@[simp]

theorem Nimber.le_groupClosure (x : Nimber) : x ≤ x.groupClosure

@[simp]

theorem Nimber.IsGroup.groupClosure (x : Nimber) : x.groupClosure.IsGroup

theorem Nimber.IsGroup.groupClosure_le_iff {x y : Nimber} (h : x.IsGroup) : y.groupClosure ≤ x ↔ y ≤ x

theorem Nimber.IsGroup.lt_groupClosure_iff {x y : Nimber} (h : x.IsGroup) : x < y.groupClosure ↔ x < y

theorem Nimber.IsGroup.groupClosure_eq {x : Nimber} (h : x.IsGroup) : x.groupClosure = x

theorem Nimber.groupClosure_monotone : Monotone groupClosure

theorem Nimber.leftOrdContinuous_groupClosure : LeftOrdContinuous groupClosure

@[simp]

theorem Nimber.groupClosure_zero : groupClosure 0 = 1

@[simp]

theorem Nimber.groupClosure_one : groupClosure 1 = 1

@[simp]

theorem Nimber.groupClosure_two : (of 2).groupClosure = of 2

@[simp]

theorem Nimber.groupClosure.two_opow (x : Ordinal.{u_1}) : (of (2 ^ x)).groupClosure = of (2 ^ x)

theorem Nimber.groupClosure_of_not_isGroup {x : Nimber} (h : ¬x.IsGroup) (hx₀ : x ≠ 0) : x.groupClosure = of (2 ^ (Ordinal.log 2 (val x) + 1))

theorem Nimber.isClub_ofPred_isGroup : IsClub (Set.ofPred IsGroup)

theorem Nimber.exists_isGroup_between {x : Nimber} (hx : x ≠ 0) : ∃ (l : Nimber), l.IsGroup ∧ ∃ (u : Nimber), u.IsGroup ∧ l ≤ x ∧ x < u ∧ ∀ (z : Nimber), z.IsGroup → l < z → u ≤ z

noncomputable def Nimber.enumGroup : Ordinal.{u_1} ↪o Nimber

The normal enumerator function for groups. (This is equal to ∗(2 ^ x).)

Equations

• Nimber.enumGroup = OrderEmbedding.ofStrictMono (fun (x : Ordinal.{?u.1}) => ↑((Order.enum (Set.ofPred Nimber.IsGroup) Nimber.enumGroup._proof_1✝) (Nimber.of x))) Nimber.enumGroup._proof_2✝

theorem Nimber.enumGroup_def (x : Ordinal.{u_1}) : enumGroup x = ↑((Order.enum (Set.ofPred IsGroup) ⋯) (of x))

theorem Nimber.enumGroup_def' (x : Ordinal.{u_1}) : enumGroup x = of ↑((Order.enum {x : Ordinal.{u_1} | (of x).IsGroup} enumGroup_def'._proof_1) x)

@[simp]

theorem Nimber.range_enumGroup : Set.range ⇑enumGroup = Set.ofPred IsGroup

theorem Nimber.mem_range_enumGroup_iff {x : Nimber} : x ∈ Set.range ⇑enumGroup ↔ x.IsGroup

theorem Nimber.IsGroup.enumGroup (x : Ordinal.{u_1}) : (Nimber.enumGroup x).IsGroup

theorem Nimber.isNormal_enumGroup : Order.IsNormal ⇑enumGroup

theorem Nimber.enumGroup_add_one (x : Ordinal.{u_1}) : enumGroup (x + 1) = (Order.succ (enumGroup x)).groupClosure

theorem Nimber.enumGroup_eq_two_opow (x : Ordinal.{u_1}) : enumGroup x = of (2 ^ x)

@[simp]

theorem Nimber.enumGroup_zero : enumGroup 0 = 1

@[simp]

theorem Nimber.enumGroup_one : enumGroup 1 = of 2

theorem Nimber.enumGroup_natCast (n : ℕ) : enumGroup ↑n = of (2 ^ n)

Rings

theorem Nimber.isRing_sInf_compl (s : Subring Nimber) (hs : s ≠ ⊤) : (sInf (↑s)ᶜ).IsRing

theorem Nimber.isLowerSet_subringClosure {s : Set Nimber} (hs : IsLowerSet s) : IsLowerSet ↑(Subring.closure s)

instance Nimber.small_subringClosure (s : Set Nimber) [Small.{u, u_1 + 1} ↑s] : Small.{u, u_1 + 1} ↥(Subring.closure s)

theorem Nimber.subringClosure_Iio_eq_Iio (x : Nimber) : ∃ (y : Nimber), ↑(Subring.closure (Set.Iio x)) = Set.Iio y

noncomputable def Nimber.ringClosure (x : Nimber) : Nimber

Returns the smallest IsRing that's at least x.

Equations

• x.ringClosure = Classical.choose ⋯

@[simp]

theorem Nimber.coe_subringClosure_Iio (x : Nimber) : ↑(Subring.closure (Set.Iio x)) = Set.Iio x.ringClosure

@[simp]

theorem Nimber.mem_subringClosure_Iio {x y : Nimber} : y ∈ Subring.closure (Set.Iio x) ↔ y < x.ringClosure

@[simp]

theorem Nimber.le_ringClosure (x : Nimber) : x ≤ x.ringClosure

@[simp]

theorem Nimber.IsRing.ringClosure (x : Nimber) : x.ringClosure.IsRing

theorem Nimber.IsRing.ringClosure_le_iff {x y : Nimber} (h : x.IsRing) : y.ringClosure ≤ x ↔ y ≤ x

theorem Nimber.IsRing.lt_ringClosure_iff {x y : Nimber} (h : x.IsRing) : x < y.ringClosure ↔ x < y

theorem Nimber.IsRing.ringClosure_eq {x : Nimber} (h : x.IsRing) : x.ringClosure = x

theorem Nimber.ringClosure_monotone : Monotone ringClosure

theorem Nimber.leftOrdContinuous_ringClosure : LeftOrdContinuous ringClosure

@[simp]

theorem Nimber.ringClosure_zero : ringClosure 0 = of 2

@[simp]

theorem Nimber.ringClosure_one : ringClosure 1 = of 2

@[simp]

theorem Nimber.ringClosure_two : (of 2).ringClosure = of 2

theorem Nimber.groupClosure_le_ringClosure (x : Nimber) : x.groupClosure ≤ x.ringClosure

@[simp]

theorem Nimber.ringClosure_groupClosure (x : Nimber) : x.groupClosure.ringClosure = x.ringClosure

theorem Nimber.isClub_ofPred_isRing : IsClub (Set.ofPred IsRing)

theorem Nimber.exists_isRing_between {x : Nimber} (hx : 1 < x) : ∃ (l : Nimber), l.IsRing ∧ ∃ (u : Nimber), u.IsRing ∧ l ≤ x ∧ x < u ∧ ∀ (z : Nimber), z.IsRing → l < z → u ≤ z

noncomputable def Nimber.enumRing : Ordinal.{u_1} ↪o Nimber

The normal enumerator function for rings.

Equations

• Nimber.enumRing = OrderEmbedding.ofStrictMono (fun (x : Ordinal.{?u.1}) => ↑((Order.enum (Set.ofPred Nimber.IsRing) Nimber.enumRing._proof_1✝) (Nimber.of x))) Nimber.enumRing._proof_2✝

theorem Nimber.enumRing_def (x : Ordinal.{u_1}) : enumRing x = ↑((Order.enum (Set.ofPred IsRing) ⋯) (of x))

theorem Nimber.enumRing_def' (x : Ordinal.{u_1}) : enumRing x = of ↑((Order.enum {x : Ordinal.{u_1} | (of x).IsRing} enumRing_def'._proof_1) x)

@[simp]

theorem Nimber.range_enumRing : Set.range ⇑enumRing = Set.ofPred IsRing

theorem Nimber.mem_range_enumRing_iff {x : Nimber} : x ∈ Set.range ⇑enumRing ↔ x.IsRing

theorem Nimber.IsRing.enumRing (x : Ordinal.{u_1}) : (Nimber.enumRing x).IsRing

theorem Nimber.isNormal_enumRing : Order.IsNormal ⇑enumRing

theorem Nimber.enumRing_add_one (x : Ordinal.{u_1}) : enumRing (x + 1) = (Order.succ (enumRing x)).ringClosure

@[simp]

theorem Nimber.enumRing_zero : enumRing 0 = of 2

Fields

theorem Nimber.isField_sInf_compl (s : Subfield Nimber) (hs : s ≠ ⊤) : (sInf (↑s)ᶜ).IsField

theorem Nimber.isLowerSet_subfieldClosure {s : Set Nimber} (hs : IsLowerSet s) : IsLowerSet ↑(Subfield.closure s)

theorem Nimber.subfieldClosure_Iio_eq_Iio (x : Nimber) : ∃ (y : Nimber), ↑(Subfield.closure (Set.Iio x)) = Set.Iio y

noncomputable def Nimber.fieldClosure (x : Nimber) : Nimber

Returns the smallest IsField that's at least x.

Equations

• x.fieldClosure = Classical.choose ⋯

@[simp]

theorem Nimber.coe_subfieldClosure_Iio (x : Nimber) : ↑(Subfield.closure (Set.Iio x)) = Set.Iio x.fieldClosure

@[simp]

theorem Nimber.mem_subfieldClosure_Iio {x y : Nimber} : y ∈ Subfield.closure (Set.Iio x) ↔ y < x.fieldClosure

@[simp]

theorem Nimber.le_fieldClosure (x : Nimber) : x ≤ x.fieldClosure

@[simp]

theorem Nimber.IsField.fieldClosure (x : Nimber) : x.fieldClosure.IsField

theorem Nimber.IsField.fieldClosure_le_iff {x y : Nimber} (h : x.IsField) : y.fieldClosure ≤ x ↔ y ≤ x

theorem Nimber.IsField.lt_fieldClosure_iff {x y : Nimber} (h : x.IsField) : x < y.fieldClosure ↔ x < y

theorem Nimber.IsField.fieldClosure_eq {x : Nimber} (h : x.IsField) : x.fieldClosure = x

theorem Nimber.fieldClosure_monotone : Monotone fieldClosure

theorem Nimber.leftOrdContinuous_fieldClosure : LeftOrdContinuous fieldClosure

@[simp]

theorem Nimber.fieldClosure_zero : fieldClosure 0 = of 2

@[simp]

theorem Nimber.fieldClosure_one : fieldClosure 1 = of 2

@[simp]

theorem Nimber.fieldClosure_two : (of 2).fieldClosure = of 2

theorem Nimber.ringClosure_le_fieldClosure (x : Nimber) : x.ringClosure ≤ x.fieldClosure

theorem Nimber.groupClosure_le_fieldClosure (x : Nimber) : x.groupClosure ≤ x.fieldClosure

@[simp]

theorem Nimber.fieldClosure_ringClosure (x : Nimber) : x.ringClosure.fieldClosure = x.fieldClosure

@[simp]

theorem Nimber.fieldClosure_groupClosure (x : Nimber) : x.groupClosure.fieldClosure = x.fieldClosure

theorem Nimber.isClub_ofPred_isField : IsClub (Set.ofPred IsField)

theorem Nimber.exists_isField_between {x : Nimber} (hx : 1 < x) : ∃ (l : Nimber), l.IsField ∧ ∃ (u : Nimber), u.IsField ∧ l ≤ x ∧ x < u ∧ ∀ (z : Nimber), z.IsField → l < z → u ≤ z

noncomputable def Nimber.enumField : Ordinal.{u_1} ↪o Nimber

The normal enumerator function for fields.

Equations

• Nimber.enumField = OrderEmbedding.ofStrictMono (fun (x : Ordinal.{?u.1}) => ↑((Order.enum (Set.ofPred Nimber.IsField) Nimber.enumField._proof_1✝) (Nimber.of x))) Nimber.enumField._proof_2✝

theorem Nimber.enumField_def (x : Ordinal.{u_1}) : enumField x = ↑((Order.enum (Set.ofPred IsField) ⋯) (of x))

theorem Nimber.enumField_def' (x : Ordinal.{u_1}) : enumField x = of ↑((Order.enum {x : Ordinal.{u_1} | (of x).IsField} enumField_def'._proof_1) x)

@[simp]

theorem Nimber.range_enumField : Set.range ⇑enumField = Set.ofPred IsField

theorem Nimber.mem_range_enumField_iff {x : Nimber} : x ∈ Set.range ⇑enumField ↔ x.IsField

theorem Nimber.IsField.enumField (x : Ordinal.{u_1}) : (Nimber.enumField x).IsField

theorem Nimber.isNormal_enumField : Order.IsNormal ⇑enumField

theorem Nimber.enumField_add_one (x : Ordinal.{u_1}) : enumField (x + 1) = (Order.succ (enumField x)).fieldClosure

@[simp]

theorem Nimber.enumField_zero : enumField 0 = of 2