Documentation

VecLat.VectorOrderIdeal.Maximal

class Maximal.IsMaximal {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) :

out : IsCoatom I

Instances

theorem Maximal.le_iff {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) [IsMaximal I] {J : VectorOrderIdeal X} :

I ≤ J ↔ J = ⊤ ∨ J = I

theorem Maximal.trivial_ideals {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) [IsMaximal I] (J : VectorOrderIdeal (X ⧸ I)) :

J = ⊥ ∨ J = ⊤

instance Maximal.instArchimedean {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) [IsMaximal I] :

Archimedean (X ⧸ I)

theorem Maximal.le_total {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) [IsMaximal I] (x y : X ⧸ I) :

x ≤ y ∨ y ≤ x

theorem Maximal.one_dim_pos {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) [IsMaximal I] (x y : X) (xnonneg : 0 ≤ (Quotient.mkQ I) x) (ypos : 0 < (Quotient.mkQ I) y) :

∃ (t : ℝ), (Quotient.mkQ I) x = t • (Quotient.mkQ I) y

theorem Maximal.one_dim {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) [IsMaximal I] (x y : X) (ypos : 0 < (Quotient.mkQ I) y) :

∃ (t : ℝ), (Quotient.mkQ I) x = t • (Quotient.mkQ I) y

def Maximal.real_map {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) {e : X} (epos : 0 < (Quotient.mkQ I) e) :

VecLatHom ℝ (X ⧸ I)

Equations

Maximal.real_map I epos = { toFun := fun (t : ℝ) => t • (Quotient.mkQ I) e, map_add' := ⋯, map_smul' := ⋯, map_sup' := ⋯, map_inf' := ⋯ }

Instances For

theorem Maximal.real_map_injective {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) {e : X} (epos : 0 < (Quotient.mkQ I) e) :

Function.Injective ⇑(real_map I epos)

theorem Maximal.real_map_surjective {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) [IsMaximal I] {e : X} (epos : 0 < (Quotient.mkQ I) e) :

Function.Surjective ⇑(real_map I epos)

theorem Maximal.real_map_bijective {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) [IsMaximal I] {e : X} (epos : 0 < (Quotient.mkQ I) e) :

Function.Bijective ⇑(real_map I epos)

noncomputable def Maximal.character {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) [IsMaximal I] {e : X} (epos : 0 < (Quotient.mkQ I) e) :

VecLatHom X ℝ

Equations

Maximal.character I epos = ((Maximal.real_map I epos).symm ⋯).comp (Quotient.mkQ I)

Instances For

theorem Maximal.character_basis {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) [IsMaximal I] {e : X} (epos : 0 < (Quotient.mkQ I) e) :

(character I epos) e = 1

theorem Maximal.character_eval {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) [IsMaximal I] {e : X} (epos : 0 < (Quotient.mkQ I) e) (x : X) (xmem : x ∈ I) :

(character I epos) x = 0