Documentation

RealClosedField.Geometry.Convex.Cone.Order

source
theorem PointedCone.eq_zero_of_mem_of_neg_mem {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {C : PointedCone R M} (hC : C.IsPointed) {x : M} (hx₁ : x ∈ C) (hx₂ : -x ∈ C) :
x = 0
source
theorem PointedCone.eq_zero_of_mem_of_neg_mem₂ {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {C : PointedCone R M} (hC : C.IsPointed) {x : M} (hx₁ : x ∈ C) (hx₂ : -x ∈ C) :
x = 0

Alias of PointedCone.eq_zero_of_mem_of_neg_mem.

source
theorem PointedCone.mem_or_neg_mem {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {C : PointedCone R M} (hC : C.IsSpanning) (a : M) :
a ∈ C ∨ -a ∈ C
source
@[simp]
theorem PointedCone.lineal_eq_bot {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_3} [AddCommGroup M] [Module R M] (C : PointedCone R M) (hC : C.IsPointed) :
C.lineal = ⊥
source
theorem PointedCone.comap_isSpanning {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_3} {M' : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (C' : PointedCone R M') (hC' : C'.IsSpanning) :
(comap f C').IsSpanning
source
theorem PointedCone.map_isSpanning {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_3} {M' : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] {f : M →ₗ[R] M'} (C : PointedCone R M) (hC : C.IsSpanning) (hf : Function.Surjective ⇑f) :
(map f C).IsSpanning
source
theorem AddSubmonoid.IsPointed.of_lineal_eq_bot {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_3} [AddCommGroup M] [Module R M] (C : PointedCone R M) (h : C.lineal = ⊥) :
C.IsPointed
source
theorem PointedCone.lineal_mono {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {C D : PointedCone R M} (h : C ≤ D) :
C.lineal ≤ D.lineal
source
@[simp]
theorem PointedCone.lineal_inf {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_3} [AddCommGroup M] [Module R M] (C D : PointedCone R M) :
(C ⊓ D).lineal = C.lineal ⊓ D.lineal
source
@[simp]
theorem PointedCone.lineal_sInf {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {s : Set (PointedCone R M)} :
(sInf s).lineal = sInf (lineal '' s)
source
@[simp]
theorem PointedCone.lineal_comap {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_3} {M' : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (C' : PointedCone R M') :
(comap f C').lineal = Submodule.comap f C'.lineal
source
@[simp]
theorem PointedCone.lineal_map {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_3} {M' : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] {f : M →ₗ[R] M'} {C : PointedCone R M} (hsupp : f.ker ≤ C.lineal) :
(map f C).lineal = Submodule.map f C.lineal
source
theorem PointedCone.IsSpanning.positive {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [LinearOrder M] [IsOrderedAddMonoid M] [IsOrderedModule R M] :
(PointedCone.positive R M).IsSpanning
source
theorem PointedCone.IsPointed.positive {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [PartialOrder M] [IsOrderedAddMonoid M] [IsOrderedModule R M] :
(PointedCone.positive R M).IsPointed
source
theorem IsOrderedModule.ofAddSubmonoid {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {C : PointedCone R M} (hC : C.IsPointed) :
IsOrderedModule R M
source
noncomputable def Module.isPointedPartialOrderEquiv (R : Type u_1) [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] :
{ C : PointedCone R M // C.IsPointed } ≃ { _o : PartialOrder M // IsOrderedAddMonoid M ∧ IsOrderedModule R M }

Equivalence between cones with zero lineality space in an R-module M and partially ordered R-module structures on M.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Module.isPointedPartialOrderEquiv_apply {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (C : PointedCone R M) (h : C.IsPointed) :
    ↑((isPointedPartialOrderEquiv R) ⟨C, h⟩) = PartialOrder.ofAddSubmonoid h
    source
    @[simp]
    theorem Module.isPointedPartialOrderEquiv_symm_apply {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (o : PartialOrder M) (h : IsOrderedAddMonoid M ∧ IsOrderedModule R M) :
    have this := ⋯; have this_1 := ⋯; ↑↑((isPointedPartialOrderEquiv R).symm ⟨o, h⟩) = ConvexCone.positive R M
    source
    noncomputable def Module.isPointedLinearOrderEquiv (R : Type u_1) [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] :
    { C : PointedCone R M // C.IsPointed ∧ C.IsSpanning } ≃ { _o : LinearOrder M // IsOrderedAddMonoid M ∧ IsOrderedModule R M }

    Equivalence between maximal cones with zero lineality space in an R-module M and linearly ordered R-module structures on M.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Module.isPointedLinearOrderEquiv_apply {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (C : PointedCone R M) (h : C.IsPointed ∧ C.IsSpanning) :
      ↑((isPointedLinearOrderEquiv R) ⟨C, h⟩) = LinearOrder.ofAddSubmonoid ⋯ ⋯
      source
      @[simp]
      theorem Module.isPointedLinearOrderEquiv_symm_apply {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (o : LinearOrder M) (h : IsOrderedAddMonoid M ∧ IsOrderedModule R M) :
      have this := ⋯; have this_1 := ⋯; ↑((isPointedLinearOrderEquiv R).symm ⟨o, h⟩) = PointedCone.positive R M