Equivalences of finite toric fans

An equivalence of finite fans is a compatible pair of equivalences of their integral lattices and ambient real vector spaces which carries the cones of one fan exactly onto the cones of the other. It induces an order isomorphism of the cone index types and a morphism in each direction. Regularity and completeness are invariant under fan equivalence.

This is the combinatorial notion used to compare toric realizations without choosing coordinates. In particular, the cone equivalence identifies the affine charts which are glued in the analytic realization.

Main declarations

• TauCeti.Toric.FanEquiv: an equivalence of finite fans.
• TauCeti.Toric.FanEquiv.coneEquiv: the induced order isomorphism of their cone index types.
• TauCeti.Toric.FanEquiv.toFanHom: the underlying morphism of fans.
• TauCeti.Toric.FanEquiv.isRegular_iff: regularity is invariant under fan equivalence.
• TauCeti.Toric.FanEquiv.isComplete_iff: completeness is invariant under fan equivalence.

References

The definition follows §1.4 of W. Fulton, Introduction to Toric Varieties, and §3.3 of D. Cox, J. Little and H. Schenck, Toric Varieties.

structure TauCeti.Toric.FanEquiv {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (Φ : Fan i) (Ψ : Fan i') : Type (max (max (max u_1 u_2) u_4) u_5)

An equivalence of finite fans consists of compatible equivalences of the integral lattices and ambient real vector spaces which carry precisely the cones of the source fan to cones of the target fan.

• latticeEquiv : N ≃+ N'

  The equivalence of integral lattices.

• realEquiv : V ≃ₗ[ℝ] V'

  The equivalence of ambient real vector spaces.

• map_lattice (n : N) : self.realEquiv (i n) = i' (self.latticeEquiv n)

  The integral and real equivalences commute with the lattice embeddings.

• map_mem (σ : PointedCone ℝ V) : PointedCone.map (↑self.realEquiv) σ ∈ Ψ.cones ↔ σ ∈ Φ.cones

  A cone belongs to the target fan after transport exactly when it belongs to the source fan.

theorem TauCeti.Toric.FanEquiv.realEquiv_toLinearMap_eq {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : ↑e.realEquiv = ⋯.extend i' ↑e.latticeEquiv

The real-linear part of a fan equivalence is determined by its integral part.

theorem TauCeti.Toric.FanEquiv.ext {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} {e e' : FanEquiv Φ Ψ} (h : e.latticeEquiv = e'.latticeEquiv) : e = e'

Fan equivalences are determined by their equivalence of integral lattices.

theorem TauCeti.Toric.FanEquiv.ext_iff {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} {e e' : FanEquiv Φ Ψ} : e = e' ↔ e.latticeEquiv = e'.latticeEquiv

def TauCeti.Toric.FanEquiv.refl {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : FanEquiv Φ Φ

The identity equivalence of a fan.

@[simp]

theorem TauCeti.Toric.FanEquiv.refl_latticeEquiv {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : (FanEquiv.refl Φ).latticeEquiv = AddEquiv.refl N

The integral part of the identity fan equivalence is the identity.

@[simp]

theorem TauCeti.Toric.FanEquiv.refl_realEquiv {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : (FanEquiv.refl Φ).realEquiv = LinearEquiv.refl ℝ V

The real part of the identity fan equivalence is the identity.

def TauCeti.Toric.FanEquiv.symm {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : FanEquiv Ψ Φ

The inverse equivalence of finite fans.

@[simp]

theorem TauCeti.Toric.FanEquiv.symm_latticeEquiv {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : e.symm.latticeEquiv = e.latticeEquiv.symm

The integral part of the inverse fan equivalence is the inverse integral equivalence.

@[simp]

theorem TauCeti.Toric.FanEquiv.symm_realEquiv {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : e.symm.realEquiv = e.realEquiv.symm

The real part of the inverse fan equivalence is the inverse real equivalence.

def TauCeti.Toric.FanEquiv.trans {N : Type u_1} {N' : Type u_2} {N'' : Type u_3} {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [AddCommGroup V] [AddCommGroup V'] [AddCommGroup V''] [Module ℝ V] [Module ℝ V'] [Module ℝ V''] {i : N →+ V} {i' : N' →+ V'} {i'' : N'' →+ V''} {Φ : Fan i} {Ψ : Fan i'} {Ω : Fan i''} (e : FanEquiv Φ Ψ) (e' : FanEquiv Ψ Ω) : FanEquiv Φ Ω

The composite of two equivalences of finite fans.

@[simp]

theorem TauCeti.Toric.FanEquiv.trans_latticeEquiv {N : Type u_1} {N' : Type u_2} {N'' : Type u_3} {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [AddCommGroup V] [AddCommGroup V'] [AddCommGroup V''] [Module ℝ V] [Module ℝ V'] [Module ℝ V''] {i : N →+ V} {i' : N' →+ V'} {i'' : N'' →+ V''} {Φ : Fan i} {Ψ : Fan i'} {Ω : Fan i''} (e : FanEquiv Φ Ψ) (e' : FanEquiv Ψ Ω) : (e.trans e').latticeEquiv = e.latticeEquiv.trans e'.latticeEquiv

The integral part of a composite fan equivalence is the composite integral equivalence.

@[simp]

theorem TauCeti.Toric.FanEquiv.trans_realEquiv {N : Type u_1} {N' : Type u_2} {N'' : Type u_3} {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [AddCommGroup V] [AddCommGroup V'] [AddCommGroup V''] [Module ℝ V] [Module ℝ V'] [Module ℝ V''] {i : N →+ V} {i' : N' →+ V'} {i'' : N'' →+ V''} {Φ : Fan i} {Ψ : Fan i'} {Ω : Fan i''} (e : FanEquiv Φ Ψ) (e' : FanEquiv Ψ Ω) : (e.trans e').realEquiv = e.realEquiv ≪≫ₗ e'.realEquiv

The real part of a composite fan equivalence is the composite real equivalence.

@[simp]

theorem TauCeti.Toric.FanEquiv.refl_trans {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : (FanEquiv.refl Φ).trans e = e

The identity fan equivalence is a left unit for composition.

@[simp]

theorem TauCeti.Toric.FanEquiv.trans_refl {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : e.trans (FanEquiv.refl Ψ) = e

The identity fan equivalence is a right unit for composition.

theorem TauCeti.Toric.FanEquiv.trans_assoc {N : Type u_1} {N' : Type u_2} {N'' : Type u_3} {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [AddCommGroup V] [AddCommGroup V'] [AddCommGroup V''] [Module ℝ V] [Module ℝ V'] [Module ℝ V''] {i : N →+ V} {i' : N' →+ V'} {i'' : N'' →+ V''} {Φ : Fan i} {Ψ : Fan i'} {Ω : Fan i''} (e : FanEquiv Φ Ψ) (e' : FanEquiv Ψ Ω) {N''' : Type u_7} {V''' : Type u_8} [AddCommGroup N'''] [AddCommGroup V'''] [Module ℝ V'''] {i''' : N''' →+ V'''} {Θ : Fan i'''} (e'' : FanEquiv Ω Θ) : (e.trans e').trans e'' = e.trans (e'.trans e'')

Composition of fan equivalences is associative.

@[simp]

theorem TauCeti.Toric.FanEquiv.symm_symm {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : e.symm.symm = e

Inverting a fan equivalence twice gives the original equivalence.

@[simp]

theorem TauCeti.Toric.FanEquiv.refl_symm {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : (FanEquiv.refl Φ).symm = FanEquiv.refl Φ

The inverse of the identity fan equivalence is the identity.

@[simp]

theorem TauCeti.Toric.FanEquiv.self_trans_symm {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : e.trans e.symm = FanEquiv.refl Φ

A fan equivalence followed by its inverse is the identity equivalence.

@[simp]

theorem TauCeti.Toric.FanEquiv.symm_trans_self {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : e.symm.trans e = FanEquiv.refl Ψ

The inverse fan equivalence followed by the original is the identity equivalence.

def TauCeti.Toric.FanEquiv.coneEquiv {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : ↑Φ.cones ≃o ↑Ψ.cones

A fan equivalence induces an order isomorphism between the cones of its source and target. In particular it preserves inclusions and intersections of cones (OrderIso.map_inf).

@[simp]

theorem TauCeti.Toric.FanEquiv.coneEquiv_apply_coe {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) (σ : ↑Φ.cones) : ↑(e.coneEquiv σ) = PointedCone.map ↑e.realEquiv ↑σ

The induced cone equivalence transports a cone by the ambient linear equivalence.

@[simp]

theorem TauCeti.Toric.FanEquiv.finrank_span_coneEquiv {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) (σ : ↑Φ.cones) : Module.finrank ℝ ↥(Submodule.span ℝ ↑↑(e.coneEquiv σ)) = Module.finrank ℝ ↥(Submodule.span ℝ ↑↑σ)

The induced cone equivalence preserves the dimension of each cone's linear span.

@[simp]

theorem TauCeti.Toric.FanEquiv.coneEquiv_symm {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : e.coneEquiv.symm = e.symm.coneEquiv

The inverse induced cone equivalence is the cone equivalence of the inverse fan equivalence.

@[simp]

theorem TauCeti.Toric.FanEquiv.coneEquiv_refl {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : (FanEquiv.refl Φ).coneEquiv = OrderIso.refl ↑Φ.cones

The cone equivalence of the identity fan equivalence is the identity.

@[simp]

theorem TauCeti.Toric.FanEquiv.coneEquiv_trans {N : Type u_1} {N' : Type u_2} {N'' : Type u_3} {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [AddCommGroup V] [AddCommGroup V'] [AddCommGroup V''] [Module ℝ V] [Module ℝ V'] [Module ℝ V''] {i : N →+ V} {i' : N' →+ V'} {i'' : N'' →+ V''} {Φ : Fan i} {Ψ : Fan i'} {Ω : Fan i''} (e : FanEquiv Φ Ψ) (e' : FanEquiv Ψ Ω) : (e.trans e').coneEquiv = e.coneEquiv.trans e'.coneEquiv

The cone equivalence of a composite fan equivalence is the composite cone equivalence.

def TauCeti.Toric.FanEquiv.toFanHom {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : FanHom Φ Ψ

The morphism of fans underlying a fan equivalence.

@[simp]

theorem TauCeti.Toric.FanEquiv.toFanHom_latticeMap {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : e.toFanHom.latticeMap = ↑e.latticeEquiv

The integral map of the underlying fan morphism is the integral equivalence.

@[simp]

theorem TauCeti.Toric.FanEquiv.toFanHom_realMap {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : e.toFanHom.realMap = ↑e.realEquiv

The real map of the underlying fan morphism is the ambient real equivalence.

@[simp]

theorem TauCeti.Toric.FanEquiv.toFanHom_refl {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : (FanEquiv.refl Φ).toFanHom = FanHom.id Φ

The underlying morphism of the identity fan equivalence is the identity morphism.

@[simp]

theorem TauCeti.Toric.FanEquiv.toFanHom_trans {N : Type u_1} {N' : Type u_2} {N'' : Type u_3} {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [AddCommGroup V] [AddCommGroup V'] [AddCommGroup V''] [Module ℝ V] [Module ℝ V'] [Module ℝ V''] {i : N →+ V} {i' : N' →+ V'} {i'' : N'' →+ V''} {Φ : Fan i} {Ψ : Fan i'} {Ω : Fan i''} (e : FanEquiv Φ Ψ) (e' : FanEquiv Ψ Ω) : (e.trans e').toFanHom = e'.toFanHom.comp e.toFanHom

The underlying morphism respects composition of fan equivalences.

@[simp]

theorem TauCeti.Toric.FanEquiv.toFanHom_leastCone {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) (σ : ↑Φ.cones) : e.toFanHom.leastCone ⋯ = ↑(e.coneEquiv σ)

The least target cone of the underlying fan morphism is the image cone itself.

theorem TauCeti.Toric.FanEquiv.isRegular_iff {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : Ψ.IsRegular ↔ Φ.IsRegular

A finite fan is regular exactly when an equivalent fan is regular.

theorem TauCeti.Toric.FanEquiv.image_support {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : ⇑e.realEquiv '' Φ.support = Ψ.support

The ambient linear equivalence carries the support of the source fan onto the support of the target fan.

theorem TauCeti.Toric.FanEquiv.isComplete_iff {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (e : FanEquiv Φ Ψ) : Ψ.IsComplete ↔ Φ.IsComplete

Completeness of finite fans is invariant under fan equivalence.