Documentation

TauCeti.Geometry.Toric.Algebraic.Fan.Subdivision

Subdivisions of finite toric fans #

A fan Φ subdivides a fan Ψ when they have the same support and every cone of Φ is contained in a cone of Ψ. Every cone of Ψ is then covered by the cones of Φ which it contains. This derived conewise form is needed to control affine cone charts and to apply support criteria for toric maps.

A subdivision has the same support as the original fan and induces a fan morphism whose lattice and real-linear maps are identities. Subdivisions are reflexive and transitive, and products of subdivisions are subdivisions.

Main declarations #

References #

The definition is the standard one in §1.4 of W. Fulton, Introduction to Toric Varieties, and §3.3 of D. Cox, J. Little and H. Schenck, Toric Varieties.

source
structure TauCeti.Toric.Fan.IsSubdivision {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ Ψ : Fan i) :
Prop

A fan Φ is a subdivision of a fan Ψ if both fans have the same support and every cone of Φ lies in a cone of Ψ.

  • exists_cone_le ⦃σ : PointedCone ℝ V⦄ : σ ∈ Φ.cones → ∃ τ ∈ Ψ.cones, σ ≤ τ

    Every cone of the subdividing fan lies in a cone of the original fan.

  • support_eq : Φ.support = Ψ.support

    The subdividing fan has the same support as the original fan.

Instances For
    source
    theorem TauCeti.Toric.Fan.IsSubdivision.exists_mem_cone {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ : Fan i} {τ : PointedCone ℝ V} (h : Φ.IsSubdivision Ψ) (hτ : τ ∈ Ψ.cones) {x : V} (hx : x ∈ τ) :
    ∃ σ ∈ Φ.cones, σ ≤ τ ∧ x ∈ σ

    Every point of an original cone lies in a subdividing cone contained in it.

    source
    theorem TauCeti.Toric.Fan.IsSubdivision.mem_iff_exists {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ : Fan i} {τ : PointedCone ℝ V} (h : Φ.IsSubdivision Ψ) (hτ : τ ∈ Ψ.cones) {x : V} :
    x ∈ τ ↔ ∃ σ ∈ Φ.cones, σ ≤ τ ∧ x ∈ σ

    Membership in a cone of the original fan is equivalent to membership in some subdividing cone contained in it.

    source
    theorem TauCeti.Toric.Fan.IsSubdivision.isComplete_iff {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ : Fan i} (h : Φ.IsSubdivision Ψ) :
    Φ.IsComplete ↔ Ψ.IsComplete

    A subdivision is complete exactly when the original fan is complete.

    source
    noncomputable def TauCeti.Toric.Fan.IsSubdivision.toFanHom {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ : Fan i} (h : Φ.IsSubdivision Ψ) :
    FanHom Φ Ψ

    A subdivision induces the fan morphism which is the identity on the ambient lattice.

    Instances For
      source
      @[simp]
      theorem TauCeti.Toric.Fan.IsSubdivision.toFanHom_latticeMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ : Fan i} (h : Φ.IsSubdivision Ψ) :
      h.toFanHom.latticeMap = AddMonoidHom.id N

      The integral map induced by a subdivision is the identity.

      source
      @[simp]
      theorem TauCeti.Toric.Fan.IsSubdivision.toFanHom_realMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ : Fan i} (h : Φ.IsSubdivision Ψ) :
      h.toFanHom.realMap = LinearMap.id

      The real-linear map induced by a subdivision is the identity.

      source
      theorem TauCeti.Toric.Fan.IsSubdivision.le_leastCone {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ : Fan i} {σ : PointedCone ℝ V} (h : Φ.IsSubdivision Ψ) (hσ : σ ∈ Φ.cones) :
      σ ≤ h.toFanHom.leastCone hσ

      A cone of a subdivision lies in its least cone of the original fan.

      source
      theorem TauCeti.Toric.Fan.IsSubdivision.leastCone_eq_self {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ : Fan i} {σ : PointedCone ℝ V} (h : Φ.IsSubdivision Ψ) (hσ : σ ∈ Φ.cones) (hσΨ : σ ∈ Ψ.cones) :
      h.toFanHom.leastCone hσ = σ

      A cone of a subdivision which is also a cone of the original fan is its own least cone.

      source
      theorem TauCeti.Toric.Fan.IsSubdivision.refl {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) :
      Φ.IsSubdivision Φ

      Every fan is a subdivision of itself.

      source
      theorem TauCeti.Toric.Fan.IsSubdivision.trans {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ Ω : Fan i} (hΦΨ : Φ.IsSubdivision Ψ) (hΨΩ : Ψ.IsSubdivision Ω) :
      Φ.IsSubdivision Ω

      Subdivision is transitive.

      source
      @[simp]
      theorem TauCeti.Toric.Fan.IsSubdivision.toFanHom_refl {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) :
      ⋯.toFanHom = FanHom.id Φ

      The identity morphism is the morphism induced by the reflexive subdivision.

      source
      theorem TauCeti.Toric.Fan.IsSubdivision.toFanHom_trans {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ Ω : Fan i} (hΦΨ : Φ.IsSubdivision Ψ) (hΨΩ : Ψ.IsSubdivision Ω) :
      ⋯.toFanHom = hΨΩ.toFanHom.comp hΦΨ.toFanHom

      The fan morphism of a composite subdivision is the composite of the induced morphisms.

      This is not a simp lemma: the intermediate fan Ψ occurs only in the hypotheses, so the left-hand side never determines it. Use toFanHom_latticeMap to simplify the underlying maps.

      source
      theorem TauCeti.Toric.Fan.IsSubdivision.prod {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ : Fan i} {N' : Type u_3} {V' : Type u_4} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} {Φ' Ψ' : Fan i'} (h : Φ.IsSubdivision Ψ) (h' : Φ'.IsSubdivision Ψ') :
      (Φ.prod Φ').IsSubdivision (Ψ.prod Ψ')

      The product of two subdivisions is a subdivision of the product fan.

      source
      @[simp]
      theorem TauCeti.Toric.Fan.IsSubdivision.toFanHom_prod {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ : Fan i} {N' : Type u_3} {V' : Type u_4} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} {Φ' Ψ' : Fan i'} (h : Φ.IsSubdivision Ψ) (h' : Φ'.IsSubdivision Ψ') :
      ⋯.toFanHom = h.toFanHom.prodMap h'.toFanHom

      The fan morphism of a product subdivision is the product of the induced morphisms.