Profinite.NobelingProof.GoodProducts.span
theorem Profinite.NobelingProof.GoodProducts.span :
∀ {I : Type u} [inst : LinearOrder I] [inst_1 : IsWellOrder I fun x x_1 => x < x_1] (C : Set (I → Bool)),
IsClosed C → ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval C))
This theorem, named `Profinite.NobelingProof.GoodProducts.span`, states that for any set `C` of boolean functions over a type `I` which has a linear order and a well-order defined by less-than relation, if `C` is closed, then the entire space is contained within the submodule of integer coefficients spanned by the range of evaluations of 'good' products. Here, 'good' products are a certain type of mathematical construction defined as part of Nobeling's proof in the theory of profinite spaces.
More concisely: For any set of boolean functions over a linearly and well-ordered type `I` with a closed subset `C`, the entire space is contained in the submodule spanned by the evaluations of 'good' products on `C`.
|
Profinite.NobelingProof.Products.prop_of_isGood
theorem Profinite.NobelingProof.Products.prop_of_isGood :
∀ {I : Type u} [inst : LinearOrder I] (C : Set (I → Bool)) {l : Profinite.NobelingProof.Products I} (J : I → Prop)
[inst_1 : (j : I) → Decidable (J j)],
Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C J) l → ∀ a ∈ ↑l, J a
The theorem `Profinite.NobelingProof.Products.prop_of_isGood` states that for any type `I` equipped with a linear order, a set `C` of Boolean-valued functions on `I`, a product `l` of `I`, and a property `J` of elements of `I`, if `l` is "good" with respect to the image of `C` under the projection `J`, then every element `a` of `l` satisfies the property `J`. Here, a product is said to be "good" if the evaluation of `C` at `l` is not an integer linear combination of the evaluations of `C` at all products less than `l`. The projection of `C` by `J` is the image of `C` under the projection function `J`.
More concisely: If a product of a linearly ordered type with respect to a set of Boolean-valued functions is "good" with respect to the image of the functions under a projection, then every element in the product satisfies the property of the projection.
|
Profinite.NobelingProof.ord_term_aux
theorem Profinite.NobelingProof.ord_term_aux :
∀ {I : Type u} [inst : LinearOrder I] [inst_1 : IsWellOrder I fun x x_1 => x < x_1] {o : Ordinal.{u}}
(ho : o < Ordinal.type fun x x_1 => x < x_1),
Profinite.NobelingProof.ord I (Profinite.NobelingProof.term I ho) = o
The theorem `Profinite.NobelingProof.ord_term_aux` states that for any type `I`, given a linear order and a well-ordering on `I`, and for any ordinal `o` less than the order type of `I`, when one sends `o` to `I` using the `Profinite.NobelingProof.term` function and then sends the result back to the ordinals using `Profinite.NobelingProof.ord`, one obtains the original ordinal `o`. This demonstrates a property of these two operations acting as a form of an inverse pair for the given conditions.
More concisely: Given a linear order and a well-ordering on a type `I`, the functions `Profinite.NobelingProof.term` and `Profinite.NobelingProof.ord` form an inverse pair, preserving ordinals below the order type of `I`.
|
Profinite.NobelingProof.continuous_proj
theorem Profinite.NobelingProof.continuous_proj :
∀ {I : Type u} (J : I → Prop) [inst : (i : I) → Decidable (J i)], Continuous (Profinite.NobelingProof.Proj J) := by
sorry
The theorem `Profinite.NobelingProof.continuous_proj` asserts that for any type `I`, any property `J` over `I`, and given that for each element `i` of type `I` it is decidable whether `J i` holds or not, the projection function `Profinite.NobelingProof.Proj J` that maps everything satisfying `J i` to itself and everything else to `false` is continuous. In mathematical terms, this essentially means that the projection function preserves the topological structure and does not disrupt the continuity of the underlying set.
More concisely: Given a type `I` and a decidable property `J` over `I`, the continuous map `Profinte.NobelingProof.Proj J : I -> Prop` sending `i : I` to `J i` if `J i` holds and `false` otherwise, is a continuous function.
|
Profinite.NobelingProof.πs'.proof_1
theorem Profinite.NobelingProof.πs'.proof_1 :
∀ {I : Type u_1} [inst : LinearOrder I] [inst_1 : IsWellOrder I fun x x_1 => x < x_1] {o₁ o₂ : Ordinal.{u_1}},
o₁ ≤ o₂ → ∀ (x : I), Profinite.NobelingProof.ord I x < o₁ → Profinite.NobelingProof.ord I x < o₂
The theorem `Profinite.NobelingProof.πs'.proof_1` states that for any type `I` equipped with a linear order and a well-order, and for any two ordinals `o₁` and `o₂` in the same type, if `o₁` is less than or equal to `o₂`, then for any element `x` of type `I`, if the ordinal of `x` is less than `o₁`, it will also be less than `o₂`. In other words, this theorem guarantees the preservation of order among ordinals under certain conditions.
More concisely: For any type equipped with a linear order and a well-order, if one ordinal is less than or equal to another, then the ordinal of any element is preserved and is less than or equal to the larger ordinal.
|
Profinite.NobelingProof.GoodProducts.spanFin
theorem Profinite.NobelingProof.GoodProducts.spanFin :
∀ {I : Type u} [inst : LinearOrder I] [inst_1 : IsWellOrder I fun x x_1 => x < x_1] (C : Set (I → Bool))
(s : Finset I),
⊤ ≤
Submodule.span ℤ
(Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun x => x ∈ s)))
The theorem `Profinite.NobelingProof.GoodProducts.spanFin` states that for any type `I` equipped with a linear order, and a well-order for which the order relation is less than (`<`), and a given set `C` of boolean-valued functions on `I`, and a finite subset `s` of `I`, the entirety (`⊤`) is less than or equal to the submodule span over integers (`ℤ`) of the range of the evaluation of good products of the image of `Proj π J` where `J` is the characteristic function of the set `s` (i.e., `fun x => x ∈ s`). Essentially, it asserts that the good products in a given set span the entire space when the set is a finite subset of `I`.
More concisely: For any linear order `I` with well-order `<`, set `C` of boolean-valued functions, and finite subset `s` of `I`, the good products of `J := char_on s` span the entire space over integers `ℤ` when evaluated on `Proj π J`. That is, `⊤ ≤ span C (range (good_products.map (Proj.π J)))`.
|
Profinite.NobelingProof.Products.isGood_mono
theorem Profinite.NobelingProof.Products.isGood_mono :
∀ {I : Type u} [inst : LinearOrder I] [inst_1 : IsWellOrder I fun x x_1 => x < x_1] (C : Set (I → Bool))
{l : Profinite.NobelingProof.Products I} {o₁ o₂ : Ordinal.{u}},
o₁ ≤ o₂ →
Profinite.NobelingProof.Products.isGood
(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₁) l →
Profinite.NobelingProof.Products.isGood
(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₂) l
The theorem `Profinite.NobelingProof.Products.isGood_mono` states that, for any type `I` with a linear order and well-ordering, a set `C` of Boolean-valued functions on `I`, a product `l` in the Nobeling space for `I`, and two ordinals `o₁` and `o₂` where `o₁` is less than or equal to `o₂`, if `l` is 'good' with respect to the mapping `π` applied to `C` and the set of elements of `I` that have an ordinal less than `o₁`, then `l` is also 'good' with respect to the mapping `π` applied to `C` and the set of elements of `I` that have an ordinal less than `o₂`. Here, 'good' means that the evaluation of `l` is not in the integer span of the evaluation of `C` for elements less than `l`.
More concisely: If a function in the Nobeling space is good with respect to a set of Boolean-valued functions and a ordinal `o₁`, then it is also good with respect to that ordinal `o₂` as long as `o₁` is less than or equal to `o₂`.
|
Profinite.Nobeling.embedding
theorem Profinite.Nobeling.embedding : ∀ (S : Profinite), ClosedEmbedding (Profinite.Nobeling.ι S)
The theorem `Profinite.Nobeling.embedding` states that for every Profinite space `S`, the map `Nobeling.ι` is a closed embedding. In other words, when mapping from the Profinite space `S` to the Boolean values of a set of clopen (both closed and open) subsets, the `Nobeling.ι` function preserves the closeness of the original space, making it a closed embedding.
More concisely: The `Nobeling.ι` function is a closed embedding for every Profinite space `S`, preserving closeness when mapping to the Boolean values of its clopen subsets.
|
Profinite.NobelingProof.continuous_projRestrict
theorem Profinite.NobelingProof.continuous_projRestrict :
∀ {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [inst : (i : I) → Decidable (J i)],
Continuous (Profinite.NobelingProof.ProjRestrict C J)
The theorem `Profinite.NobelingProof.continuous_projRestrict` asserts that for any type `I`, any set `C` of Boolean-valued functions on `I`, and any property `J` of the elements of `I`, given that we can decide for each `i` in `I` whether `J i` holds, the restriction of the projection `Proj` to a subset and mapping to its image (represented by the function `Profinite.NobelingProof.ProjRestrict C J`) is continuous.
More concisely: Given a type `I`, a set `C` of Boolean-valued functions on `I`, and a property `J` of elements in `I`, if we can decide for each `i` in `I` whether `J(i)` holds, then the continuous restriction of the projection `Proj` to a subset and mapping to its image (`Profinite.NobelingProof.ProjRestrict C J`) is a continuous function.
|
Profinite.NobelingProof.continuous_projRestricts
theorem Profinite.NobelingProof.continuous_projRestricts :
∀ {I : Type u} (C : Set (I → Bool)) {J K : I → Prop} [inst : (i : I) → Decidable (J i)]
[inst_1 : (i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i),
Continuous (Profinite.NobelingProof.ProjRestricts C h)
This theorem is a part of the Profinite space proof in Nobeling's theorem. It states that for any type `I`, any set `C` of boolean valued functions on `I`, and any two properties `J` and `K` of elements of `I` (where for each `i` in `I`, it is decidable whether `J i` and `K i` hold), if every `i` such that `J i` holds also satisfies `K i`, then the function `Profinite.NobelingProof.ProjRestricts C h`, which restricts a projection based on the set `C` and properties `J` and `K`, is continuous. Here, the function `h` ensures the inclusion of the domain where `J` holds into the domain where `K` holds.
More concisely: If a set `C` of boolean functions on a type `I` satisfies `J i ⟹ K i` for all `i` in `I` where `J i` and `K i` are decidable, then the function restricting a projection based on `C`, `J`, and `K` is continuous.
|
Profinite.NobelingProof.ord_term
theorem Profinite.NobelingProof.ord_term :
∀ {I : Type u} [inst : LinearOrder I] [inst_1 : IsWellOrder I fun x x_1 => x < x_1] {o : Ordinal.{u}}
(ho : o < Ordinal.type fun x x_1 => x < x_1) (i : I),
Profinite.NobelingProof.ord I i = o ↔ Profinite.NobelingProof.term I ho = i
The theorem `Profinite.NobelingProof.ord_term` establishes a bijective correspondence between terms of type `I` and ordinals less than the order type of `I`. Specifically, for any type `I` with a linear order and a well-order, and any ordinal `o` less than the order type of `I`, the ordinal representation `Profinite.NobelingProof.ord I i` of a term `i` of `I` is equal to `o` if and only if the term `Profinite.NobelingProof.term I ho` associated with `o` is equal to `i`. In other words, `Profinite.NobelingProof.ord` and `Profinite.NobelingProof.term` are inverse operations, and the type `I` can be bijectively mapped onto the ordinals less than its order type.
More concisely: The function `Profinite.NobelingProof.ord` and its inverse `Profinite.NobelingProof.term` establish a bijective correspondence between the ordinals less than the order type of a linearly ordered and well-ordered type `I` and its terms.
|
Profinite.NobelingProof.Nobeling_aux
theorem Profinite.NobelingProof.Nobeling_aux :
∀ {I : Type u} [inst : LinearOrder I] [inst : IsWellOrder I fun x x_1 => x < x_1] {S : Profinite}
{ι : ↑S.toCompHaus.toTop → I → Bool}, ClosedEmbedding ι → Module.Free ℤ (LocallyConstant ↑S.toCompHaus.toTop ℤ)
This theorem states that for any profinite set `S` and a closed embedding of `S` into a function from `I` to `Bool` where `I` is a linear order and well-ordered with respect to a less than operator, the set of locally constant functions from the topological space associated with `S` to the integers (`ℤ`) forms a free module over the integers. Here, a profinite set is a projective limit of finite discrete spaces, a closed embedding is a homeomorphism onto its image, and a locally constant function is one which is constant on each connected component of its domain.
More concisely: The set of locally constant functions from a profinite set embedded as a closed subspace of a linear order into Booleans, to integers, forms a free module over the integers.
|
Profinite.NobelingProof.factors_prod_eq_basis
theorem Profinite.NobelingProof.factors_prod_eq_basis :
∀ {I : Type u} [inst : LinearOrder I] (C : Set (I → Bool)) (s : Finset I)
(x : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)),
(Profinite.NobelingProof.factors C s x).prod = Profinite.NobelingProof.spanFinBasis C s x
The theorem `Profinite.NobelingProof.factors_prod_eq_basis` states that for any type `I` with a linear order structure, any set `C` of boolean-valued functions on `I`, any finite subset `s` of `I`, and any element `x` from the image of the projection of `C` onto the set of functions in `I` that are true when their input is in `s`, the product of the elements of the list `factors C s x` is equal to the Kronecker delta function at `x`, which is a locally constant function that is equal to 1 at `x` and 0 elsewhere. This product is computed with respect to the basis spanned by `C` and `s`. This theorem is part of the proof of the Nobeling's theorem in the setting of profinite topological spaces.
More concisely: For any linear ordered type I, any set C of boolean-valued functions on I, any finite subset s of I, and any x in the image of the restriction of C to s, the product of the elements of the basis of C and s at x is equal to the Kronecker delta function at x.
|
Mathlib.Topology.Category.Profinite.Nobeling._auxLemma.36
theorem Mathlib.Topology.Category.Profinite.Nobeling._auxLemma.36 :
∀ {α : Type u} [inst : LinearOrder α] {a b : α}, (¬a < b) = (b ≤ a)
This theorem, named `Mathlib.Topology.Category.Profinite.Nobeling._auxLemma.36`, states that for all types `α` endowed with a linear order and for all elements `a` and `b` of this type, the statement "not (`a` is less than `b`)" is equivalent to "`b` is less than or equal to `a`". In mathematical terms, it encapsulates the principle ¬(a < b) = (b ≤ a) in the context of any linear order.
More concisely: In any linear order, the negation of `a` being less than `b` is equivalent to `b` being less than or equal to `a`.
|
Profinite.NobelingProof.GoodProducts.span_iff_products
theorem Profinite.NobelingProof.GoodProducts.span_iff_products :
∀ {I : Type u} [inst : LinearOrder I] [inst_1 : IsWellOrder I fun x x_1 => x < x_1] (C : Set (I → Bool)),
⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval C)) ↔
⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.Products.eval C))
This theorem, named `Profinite.NobelingProof.GoodProducts.span_iff_products`, states that for any set `C` of functions from a type `I` (which has a linear order and is well-ordered) to Boolean values, the 'good' products span the space of locally constant functions from `C` to integers if and only if all products span this space. Here, 'good' products and products are evaluated using `Profinite.NobelingProof.GoodProducts.eval` and `Profinite.NobelingProof.Products.eval` respectively, and the span of a set of elements refers to the smallest submodule containing that set. The spanning is performed over the integers, `ℤ`.
More concisely: For a well-ordered set I with a linear order, the set of good products of functions from I to Boolean values spans the space of locally constant functions from I to integers if and only if the ordinary products of these functions do.
|
Profinite.NobelingProof.GoodProducts.maxTail_isGood
theorem Profinite.NobelingProof.GoodProducts.maxTail_isGood :
∀ {I : Type u} [inst : LinearOrder I] [inst_1 : IsWellOrder I fun x x_1 => x < x_1] (C : Set (I → Bool))
{o : Ordinal.{u}},
IsClosed C →
Profinite.NobelingProof.contained C (Order.succ o) →
∀ (ho : o < Ordinal.type fun x x_1 => x < x_1) (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)),
⊤ ≤
Submodule.span ℤ
(Set.range
(Profinite.NobelingProof.GoodProducts.eval
(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o))) →
Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.C' C ho) (↑l).Tail
The theorem `Profinite.NobelingProof.GoodProducts.maxTail_isGood` states the following:
For any type `I` with a linear order and well order, a set `C` of Boolean functions over `I`, and an ordinal `o`, if `C` is closed and all elements `f` in `C` of type `I` for which `f i = true` satisfy that `Profinite.NobelingProof.ord I i < Order.succ o`, then for any `o` less than the order type of `I` and any `l` in the "good" products `MaxProducts` of `C` that contain `o`, if the span of the range of the evaluation of the image under projection `π` of the good products of `C` is equal to or greater than the whole space, then the tail of `l` (which is obtained by removing the leading `o` from `l`) is a "good" product with respect to `C'`, the intersection of the subsets `C0` and `π(C1)` of `C`. Here, a product is "good" if its evaluation is not in the span of the evaluations of all smaller products.
More concisely: If `C` is a closed set of Boolean functions over a well-ordered type `I` with order `o`, and for all `f` in `C` with `f i = true` and `Profinite.NobelingProof.ord I i < Order.succ o`, the span of `π(MaxProducts(C))` is greater than or equal to the whole space, then the tail of any good product `l` containing `o` is a good product with respect to the intersection of `C` and the image of `C` under `π`.
|
Profinite.NobelingProof.Products.evalFacProp
theorem Profinite.NobelingProof.Products.evalFacProp :
∀ {I : Type u} [inst : LinearOrder I] (C : Set (I → Bool)) {l : Profinite.NobelingProof.Products I} (J : I → Prop),
(∀ a ∈ ↑l, J a) →
∀ [inst_1 : (j : I) → Decidable (J j)],
⇑(Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C J) l) ∘
Profinite.NobelingProof.ProjRestrict C J =
⇑(Profinite.NobelingProof.Products.eval C l)
This theorem, which is a part of Profinite's NobelingProof, asserts the following: for any type `I` equipped with a linear order, a set `C` of Boolean-valued functions on `I`, a product `l` of elements from `I`, and a predicate `J` on `I`, if every element `a` in the product `l` satisfies the predicate `J`, then for any `j` in `I` that can be decided by `J`, the composition of the evaluation of `l` under the image of `Proj π J` with the restriction of `Proj π J` to `C`, is equal to the evaluation of `l` under `C`.
In simple terms, this theorem shows a relationship between the evaluation of a product under a set of functions and its projection restricted to a subset, assuming that all elements of the product satisfy a certain property. The mathematical operations involved are function composition and evaluation.
More concisely: Given a linear ordered type `I`, a set `C` of Boolean-valued functions on `I`, a product `l` of elements from `I`, and a predicate `J` on `I`, if every `a` in `l` satisfies `J`, then for any `j` in `I` decidable by `J`, the composition of `l`'s evaluation under `Proj π J` and `Proj π J`'s restriction to `C` equals `l`'s evaluation under `C`.
|