IMO 2012 A7

Given a lattice $α$, the inf-closure (resp. sup-closure) of a subset $S ⊆ α$ is the smallest set containing $S$ that is closed under infimum (resp. supremum).

Let $R$ be a totally ordered commutative ring and $σ$ be a set. Let $R^{R^σ}$ be the ring of functions from $R^σ$ to $R$. View $R^{R^σ}$ as a lattice via pointwise maximum and minimum. Let $R[σ]$ denote the ring of multivariate polynomials with variable set $σ$. Let $S ⊆ R^{R^σ}$ be the sup-closure of the inf-closure of $R[σ]$. Prove that $S$ is a subring of $R^{R^σ}$.

Solution

We follow and generalize the official solution. The original formulation only asks to prove that $S$ is closed under multiplication. However, the official solution essentially proves that $S$ is a ring.

We define the meta-closure of a subset $S$ of a lattice to be the smallest set containing $S$ that is closed under both infimum and supremum.

Extra lemmas

theorem IMOSL.IMO2012A7.Pi_posPart_mul_inf {I : Type u_2} {R : I → Type u_1} [(i : I) → Ring (R i)] [(i : I) → LinearOrder (R i)] [∀ (i : I), IsOrderedRing (R i)] (f g₁ g₂ : (i : I) → R i) : f⁺ * (g₁ ⊓ g₂) = f⁺ * g₁ ⊓ f⁺ * g₂

For any f, g₁, g₂ ∈ ∏_i R_i, we have f⁺ min{g₁, g₂} = min{f⁺ g₁, f⁺ g₂}.

theorem IMOSL.IMO2012A7.Pi_posPart_mul_sup {I : Type u_2} {R : I → Type u_1} [(i : I) → Ring (R i)] [(i : I) → LinearOrder (R i)] [∀ (i : I), IsOrderedRing (R i)] (f g₁ g₂ : (i : I) → R i) : f⁺ * (g₁ ⊔ g₂) = f⁺ * g₁ ⊔ f⁺ * g₂

For any f, g₁, g₂ ∈ ∏_i R_i, we have f⁺ max{g₁, g₂} = max{f⁺ g₁, f⁺ g₂}.

theorem IMOSL.IMO2012A7.Pi_inf_mul_posPart {I : Type u_2} {R : I → Type u_1} [(i : I) → Ring (R i)] [(i : I) → LinearOrder (R i)] [∀ (i : I), IsOrderedRing (R i)] (f g₁ g₂ : (i : I) → R i) : (g₁ ⊓ g₂) * f⁺ = g₁ * f⁺ ⊓ g₂ * f⁺

For any f, g₁, g₂ ∈ ∏_i R_i, we have min{g₁, g₂} f⁺ = min{g₁ f⁺, g₂ f⁺}.

theorem IMOSL.IMO2012A7.Pi_sup_mul_posPart {I : Type u_2} {R : I → Type u_1} [(i : I) → Ring (R i)] [(i : I) → LinearOrder (R i)] [∀ (i : I), IsOrderedRing (R i)] (f g₁ g₂ : (i : I) → R i) : (g₁ ⊔ g₂) * f⁺ = g₁ * f⁺ ⊔ g₂ * f⁺

For any f, g₁, g₂ ∈ ∏_i R_i, we have max{g₁, g₂} f⁺ = max{g₁ f⁺, g₂ f⁺}.

Start of the problem

inductive IMOSL.IMO2012A7.MetaClosure {α : Type u_1} [Lattice α] (P : α → Prop) : α → Prop

Closure under simultaneous infimum and supremum.

• ofMem {α : Type u_1} [Lattice α] {P : α → Prop} (a : α) : P a → MetaClosure P a
• ofMin {α : Type u_1} [Lattice α] {P : α → Prop} (a b : α) : MetaClosure P a → MetaClosure P b → MetaClosure P (a ⊓ b)
• ofMax {α : Type u_1} [Lattice α] {P : α → Prop} (a b : α) : MetaClosure P a → MetaClosure P b → MetaClosure P (a ⊔ b)

inductive IMOSL.IMO2012A7.BinOpClosure {α : Sort u_1} (op : α → α → α) (P : α → Prop) : α → Prop

Closure under one binary operation.

• ofMem {α : Sort u_1} {op : α → α → α} {P : α → Prop} (a : α) : P a → BinOpClosure op P a
• ofOp {α : Sort u_1} {op : α → α → α} {P : α → Prop} (a b : α) : BinOpClosure op P a → BinOpClosure op P b → BinOpClosure op P (op a b)

theorem IMOSL.IMO2012A7.InfClosure_imp_MetaClosure {α : Type u_1} [Lattice α] (P : α → Prop) {a : α} (ha : BinOpClosure min P a) : MetaClosure P a

The inf-closure is contained in the meta-closure.

theorem IMOSL.IMO2012A7.SupInfClosure_imp_MetaClosure {α : Type u_1} [Lattice α] (P : α → Prop) {a : α} (ha : BinOpClosure max (BinOpClosure min P) a) : MetaClosure P a

The sup-closure of inf-closure is contained in the meta-closure.

theorem IMOSL.IMO2012A7.MetaClosure_imp_SupInfClosure {α : Type u_1} [DistribLattice α] (P : α → Prop) {a : α} (ha : MetaClosure P a) : BinOpClosure max (BinOpClosure min P) a

The meta-closure is contained in the sup-closure of inf-closure.

theorem IMOSL.IMO2012A7.SupInfClosure_eq_MetaClosure {α : Type u_1} [DistribLattice α] (P : α → Prop) : BinOpClosure max (BinOpClosure min P) = MetaClosure P

The sup-closure of inf-closure is equal to the meta-closure.

Subgroup structure of meta-closure

theorem IMOSL.IMO2012A7.MetaClosure.zero_mem {G : Type u_1} [Lattice G] [AddGroup G] (S : AddSubgroup G) : MetaClosure (fun (x : G) => x ∈ S) 0

The meta-closure of a subgroup contains 0.

theorem IMOSL.IMO2012A7.MetaClosure.posPart_mem {G : Type u_1} [Lattice G] [AddGroup G] (S : AddSubgroup G) {a : G} (ha : MetaClosure (fun (x : G) => x ∈ S) a) : MetaClosure (fun (x : G) => x ∈ S) a⁺

The meta-closure of a subgroup is closed under taking maximum with zero.

theorem IMOSL.IMO2012A7.MetaClosure.add_mem {G : Type u_1} [Lattice G] [AddGroup G] (S : AddSubgroup G) [AddLeftMono G] [AddRightMono G] {a b : G} (ha : MetaClosure (fun (x : G) => x ∈ S) a) (hb : MetaClosure (fun (x : G) => x ∈ S) b) : MetaClosure (fun (x : G) => x ∈ S) (a + b)

The meta-closure of a subgroup is closed under addition.

theorem IMOSL.IMO2012A7.MetaClosure.neg_mem {G : Type u_1} [Lattice G] [AddGroup G] (S : AddSubgroup G) [AddLeftMono G] [AddRightMono G] {a : G} (ha : MetaClosure (fun (x : G) => x ∈ S) a) : MetaClosure (fun (x : G) => x ∈ S) (-a)

The meta-closure of a subgroup is closed under taking positive part.

theorem IMOSL.IMO2012A7.MetaClosure.sub_mem {G : Type u_1} [Lattice G] [AddGroup G] (S : AddSubgroup G) [AddLeftMono G] [AddRightMono G] {a b : G} (ha : MetaClosure (fun (x : G) => x ∈ S) a) (hb : MetaClosure (fun (x : G) => x ∈ S) b) : MetaClosure (fun (x : G) => x ∈ S) (a - b)

The meta-closure of a subgroup is closed under subtraction.

def IMOSL.IMO2012A7.MetaClosure.AddGroup_mk {G : Type u_1} [Lattice G] [AddGroup G] (S : AddSubgroup G) [AddLeftMono G] [AddRightMono G] : AddSubgroup G

The meta-closure of a subgroup as a subgroup.

Equations

• IMOSL.IMO2012A7.MetaClosure.AddGroup_mk S = { carrier := setOf (IMOSL.IMO2012A7.MetaClosure fun (x : G) => x ∈ S), add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

Subring structure of meta-closure

theorem IMOSL.IMO2012A7.MetaClosure.posPart_mul_posPart_main_formula {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] (a b : R) : a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺

theorem IMOSL.IMO2012A7.MetaClosure.Pi_one_mem {I : Type u_2} {R : I → Type u_1} [(i : I) → Ring (R i)] [(i : I) → LinearOrder (R i)] (S : Subring ((i : I) → R i)) : MetaClosure (fun (x : (i : I) → R i) => x ∈ S) 1

The meta-closure of a subring of ∏_i R_i contains 1.

theorem IMOSL.IMO2012A7.MetaClosure.Pi_posPart_mul_posPart_main_formula {I : Type u_2} {R : I → Type u_1} [(i : I) → Ring (R i)] [(i : I) → LinearOrder (R i)] [∀ (i : I), IsOrderedRing (R i)] (f g : (i : I) → R i) : f⁺ * g⁺ = (f * g ⊓ ((f ⊔ f * g ^ 2) ⊓ (g ⊔ f ^ 2 * g)))⁺

theorem IMOSL.IMO2012A7.MetaClosure.Pi_posPart_mul_posPart_mem {I : Type u_2} {R : I → Type u_1} [(i : I) → Ring (R i)] [(i : I) → LinearOrder (R i)] [∀ (i : I), IsOrderedRing (R i)] (S : Subring ((i : I) → R i)) {f g : (i : I) → R i} (hf : f ∈ S) (hg : g ∈ S) : MetaClosure (fun (x : (i : I) → R i) => x ∈ S) (f⁺ * g⁺)

If f, g belongs to a subring of ∏_i R_i, then fg belongs to the meta-closure.

theorem IMOSL.IMO2012A7.MetaClosure.Pi_closure_posPart_mul_closure_posPart_mem {I : Type u_2} {R : I → Type u_1} [(i : I) → Ring (R i)] [(i : I) → LinearOrder (R i)] [∀ (i : I), IsOrderedRing (R i)] (S : Subring ((i : I) → R i)) {f g : (i : I) → R i} (hf : MetaClosure (fun (x : (i : I) → R i) => x ∈ S) f) (hg : MetaClosure (fun (x : (i : I) → R i) => x ∈ S) g) : MetaClosure (fun (x : (i : I) → R i) => x ∈ S) (f⁺ * g⁺)

If f, g belongs to the meta-clousre of a subring of ∏_i R_i, then so is f⁺g⁺.

theorem IMOSL.IMO2012A7.MetaClosure.Pi_mul_mem {I : Type u_2} {R : I → Type u_1} [(i : I) → Ring (R i)] [(i : I) → LinearOrder (R i)] [∀ (i : I), IsOrderedRing (R i)] (S : Subring ((i : I) → R i)) {f g : (i : I) → R i} (hf : MetaClosure (fun (x : (i : I) → R i) => x ∈ S) f) (hg : MetaClosure (fun (x : (i : I) → R i) => x ∈ S) g) : MetaClosure (fun (x : (i : I) → R i) => x ∈ S) (f * g)

If f, g belongs to the meta-clousre of a subring of ∏_i R_i, then so is fg.

def IMOSL.IMO2012A7.MetaClosure.PiSubring_mk {I : Type u_2} {R : I → Type u_1} [(i : I) → Ring (R i)] [(i : I) → LinearOrder (R i)] [∀ (i : I), IsOrderedRing (R i)] (S : Subring ((i : I) → R i)) : Subring ((i : I) → R i)

The meta-closure of a subring of ∏_i R_i as a subring.

Equations

• One or more equations did not get rendered due to their size.

Summary for polynomials

@[reducible, inline]

abbrev IMOSL.IMO2012A7.MvPolynomial_image (σ : Type u_1) (R : Type u_2) [CommRing R] : Subring ((σ → R) → R)

The image of MvPolynomial σ R in (σ → R) → R as a ring.

Equations

• IMOSL.IMO2012A7.MvPolynomial_image σ R = (Pi.ringHom MvPolynomial.eval).range

theorem IMOSL.IMO2012A7.final_solution (σ : Type u_1) (R : Type u_2) [CommRing R] [LinearOrder R] [IsOrderedRing R] : ∃ (T : Subring ((σ → R) → R)), T.carrier = setOf (BinOpClosure max (BinOpClosure min fun (x : (σ → R) → R) => x ∈ MvPolynomial_image σ R))

Final solution