Products of finite toric fans

The cones σ × τ, for σ and τ ranging through two fans, form a fan in the product lattice. Faces of a product cone split uniquely as products of faces of its factors, which gives the face-closure axiom. Intersections and supports are computed componentwise.

Products preserve completeness and regularity. They also act on fan morphisms by taking the componentwise maps, compatibly with identities and composition. These facts supply the combinatorial product operation used by products of toric realizations.

Main declarations

• TauCeti.Toric.Fan.prod: the product of two finite toric fans.
• TauCeti.Toric.Fan.prodCone: the cone of a product fan indexed by a pair of cones.
• TauCeti.Toric.Fan.support_prod: the support of a product is the product of the supports.
• TauCeti.Toric.Fan.isComplete_prod_iff: a product fan is complete exactly when both factors are complete.
• TauCeti.Toric.Fan.IsRegular.prod: products preserve regularity.
• TauCeti.Toric.Fan.mem_dualSemigroup_prod_of_comp_inl_of_comp_inr: a character of the product lattice is nonnegative on a product fan when both of its restrictions are nonnegative.
• TauCeti.Toric.FanHom.fst, TauCeti.Toric.FanHom.snd, and TauCeti.Toric.FanHom.prod: the projections and common-source pairing for product fans.
• TauCeti.Toric.FanHom.prodMap: the componentwise product of two fan morphisms.

References

The construction is described in §1.4 of W. Fulton, Introduction to Toric Varieties, and §3.1 of D. Cox, J. Little and H. Schenck, Toric Varieties.

The face-splitting argument uses PointedCone.Face.fst_prod_snd from Mathlib.Geometry.Convex.Cone.Face.Lattice.

Product fans

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

The product of two finite fans consists of the products of their cones.

@[simp]

theorem TauCeti.Toric.Fan.mem_prod_cones {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (Φ : Fan i) (Ψ : Fan i') {ξ : PointedCone ℝ (V × V')} : ξ ∈ (Φ.prod Ψ).cones ↔ ∃ σ ∈ Φ.cones, ∃ τ ∈ Ψ.cones, ξ = Submodule.prod σ τ

The cones of a product fan are exactly the products of cones from the two factors.

@[reducible, inline]

abbrev TauCeti.Toric.Fan.prodCone {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (Φ : Fan i) (Ψ : Fan i') (σ : ↑Φ.cones) (τ : ↑Ψ.cones) : ↑(Φ.prod Ψ).cones

A pair of cones determines a cone of the product fan.

@[simp]

theorem TauCeti.Toric.Fan.coe_prodCone {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (Φ : Fan i) (Ψ : Fan i') (σ : ↑Φ.cones) (τ : ↑Ψ.cones) : ↑(Φ.prodCone Ψ σ τ) = Submodule.prod ↑σ ↑τ

@[simp]

theorem TauCeti.Toric.Fan.prodCone_inf_prodCone {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (Φ : Fan i) (Ψ : Fan i') (σ σ' : ↑Φ.cones) (τ τ' : ↑Ψ.cones) : Φ.prodCone Ψ σ τ ⊓ Φ.prodCone Ψ σ' τ' = Φ.prodCone Ψ (σ ⊓ σ') (τ ⊓ τ')

Intersections of product cones are computed componentwise.

theorem TauCeti.Toric.Fan.exists_prodCone_eq {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (Φ : Fan i) (Ψ : Fan i') (ξ : ↑(Φ.prod Ψ).cones) : ∃ (σ : ↑Φ.cones) (τ : ↑Ψ.cones), Φ.prodCone Ψ σ τ = ξ

Every cone of a product fan is the product cone of a pair of factor cones.

@[simp]

theorem TauCeti.Toric.Fan.support_prod {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (Φ : Fan i) (Ψ : Fan i') : (Φ.prod Ψ).support = Φ.support ×ˢ Ψ.support

The support of a product fan is the product of the supports of its factors.

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

A product fan is complete exactly when both factors are complete.

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

The product of complete fans is complete.

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

The product of regular fans is regular.

theorem TauCeti.Toric.Fan.mem_dualSemigroup_prod_of_comp_inl_of_comp_inr {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} (Φ : Fan i) (Ψ : Fan i') {m : N × N' →+ ℤ} (h₁ : ∀ (σ : ↑Φ.cones), m.comp (AddMonoidHom.inl N N') ∈ dualSemigroup ⋯ ↑σ) (h₂ : ∀ (τ : ↑Ψ.cones), m.comp (AddMonoidHom.inr N N') ∈ dualSemigroup ⋯ ↑τ) (ξ : ↑(Φ.prod Ψ).cones) : m ∈ dualSemigroup ⋯ ↑ξ

A character of the product lattice is nonnegative on every cone of a product fan when its restrictions to the two lattice factors are nonnegative on every cone of the corresponding factor fans. The converse needs both fans to be nonempty: a product with an empty fan has no cones.

Products of fan morphisms

def TauCeti.Toric.FanHom.fst {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} (Φ₁ : Fan i₁) (Φ₂ : Fan i₂) : FanHom (Φ₁.prod Φ₂) Φ₁

The first projection from a product fan.

def TauCeti.Toric.FanHom.snd {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} (Φ₁ : Fan i₁) (Φ₂ : Fan i₂) : FanHom (Φ₁.prod Φ₂) Φ₂

The second projection from a product fan.

@[simp]

theorem TauCeti.Toric.FanHom.fst_latticeMap {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} (Φ₁ : Fan i₁) (Φ₂ : Fan i₂) : (fst Φ₁ Φ₂).latticeMap = AddMonoidHom.fst N₁ N₂

The integral map of the first projection is the first projection.

@[simp]

theorem TauCeti.Toric.FanHom.fst_realMap {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} (Φ₁ : Fan i₁) (Φ₂ : Fan i₂) : (fst Φ₁ Φ₂).realMap = LinearMap.fst ℝ V₁ V₂

The real-linear map of the first projection is the first projection.

@[simp]

theorem TauCeti.Toric.FanHom.snd_latticeMap {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} (Φ₁ : Fan i₁) (Φ₂ : Fan i₂) : (snd Φ₁ Φ₂).latticeMap = AddMonoidHom.snd N₁ N₂

The integral map of the second projection is the second projection.

@[simp]

theorem TauCeti.Toric.FanHom.snd_realMap {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} (Φ₁ : Fan i₁) (Φ₂ : Fan i₂) : (snd Φ₁ Φ₂).realMap = LinearMap.snd ℝ V₁ V₂

The real-linear map of the second projection is the second projection.

@[simp]

theorem TauCeti.Toric.FanHom.fst_leastCone_prodCone {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} (σ : ↑Φ₁.cones) (τ : ↑Φ₂.cones) : (fst Φ₁ Φ₂).leastCone ⋯ = ↑σ

The least cone containing the first projection of a product cone is its first factor.

@[simp]

theorem TauCeti.Toric.FanHom.snd_leastCone_prodCone {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} (σ : ↑Φ₁.cones) (τ : ↑Φ₂.cones) : (snd Φ₁ Φ₂).leastCone ⋯ = ↑τ

The least cone containing the second projection of a product cone is its second factor.

def TauCeti.Toric.FanHom.prod {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} {N₀ : Type u_13} {V₀ : Type u_14} [AddCommGroup N₀] [AddCommGroup V₀] [Module ℝ V₀] {i₀ : N₀ →+ V₀} {Ω : Fan i₀} (f : FanHom Ω Φ₁) (g : FanHom Ω Φ₂) : FanHom Ω (Φ₁.prod Φ₂)

Pair two fan morphisms with a common source into a product fan.

@[simp]

theorem TauCeti.Toric.FanHom.prod_latticeMap {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} {N₀ : Type u_13} {V₀ : Type u_14} [AddCommGroup N₀] [AddCommGroup V₀] [Module ℝ V₀] {i₀ : N₀ →+ V₀} {Ω : Fan i₀} (f : FanHom Ω Φ₁) (g : FanHom Ω Φ₂) : (f.prod g).latticeMap = f.latticeMap.prod g.latticeMap

The integral map of a pairing is the pairing of the integral maps.

@[simp]

theorem TauCeti.Toric.FanHom.prod_realMap {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} {N₀ : Type u_13} {V₀ : Type u_14} [AddCommGroup N₀] [AddCommGroup V₀] [Module ℝ V₀] {i₀ : N₀ →+ V₀} {Ω : Fan i₀} (f : FanHom Ω Φ₁) (g : FanHom Ω Φ₂) : (f.prod g).realMap = f.realMap.prod g.realMap

The real-linear map of a pairing is the pairing of the real-linear maps.

@[simp]

theorem TauCeti.Toric.FanHom.fst_comp_prod {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} {N₀ : Type u_13} {V₀ : Type u_14} [AddCommGroup N₀] [AddCommGroup V₀] [Module ℝ V₀] {i₀ : N₀ →+ V₀} {Ω : Fan i₀} (f : FanHom Ω Φ₁) (g : FanHom Ω Φ₂) : (fst Φ₁ Φ₂).comp (f.prod g) = f

Composing a pairing with the first projection recovers its first component.

@[simp]

theorem TauCeti.Toric.FanHom.snd_comp_prod {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} {N₀ : Type u_13} {V₀ : Type u_14} [AddCommGroup N₀] [AddCommGroup V₀] [Module ℝ V₀] {i₀ : N₀ →+ V₀} {Ω : Fan i₀} (f : FanHom Ω Φ₁) (g : FanHom Ω Φ₂) : (snd Φ₁ Φ₂).comp (f.prod g) = g

Composing a pairing with the second projection recovers its second component.

@[simp]

theorem TauCeti.Toric.FanHom.prod_unique {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} {N₀ : Type u_13} {V₀ : Type u_14} [AddCommGroup N₀] [AddCommGroup V₀] [Module ℝ V₀] {i₀ : N₀ →+ V₀} {Ω : Fan i₀} (f : FanHom Ω (Φ₁.prod Φ₂)) : ((fst Φ₁ Φ₂).comp f).prod ((snd Φ₁ Φ₂).comp f) = f

A morphism into a product fan is the pairing of its two projections.

def TauCeti.Toric.FanHom.prodMap {N₁ : Type u_5} {N₂ : Type u_6} {N₁' : Type u_7} {N₂' : Type u_8} {V₁ : Type u_9} {V₂ : Type u_10} {V₁' : Type u_11} {V₂' : Type u_12} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup N₁'] [AddCommGroup N₂'] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₁'] [AddCommGroup V₂'] [Module ℝ V₁] [Module ℝ V₂] [Module ℝ V₁'] [Module ℝ V₂'] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {i₁' : N₁' →+ V₁'} {i₂' : N₂' →+ V₂'} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} {Ψ₁ : Fan i₁'} {Ψ₂ : Fan i₂'} (f : FanHom Φ₁ Ψ₁) (g : FanHom Φ₂ Ψ₂) : FanHom (Φ₁.prod Φ₂) (Ψ₁.prod Ψ₂)

The product of two fan morphisms is given by the componentwise maps.

@[simp]

theorem TauCeti.Toric.FanHom.prodMap_latticeMap {N₁ : Type u_5} {N₂ : Type u_6} {N₁' : Type u_7} {N₂' : Type u_8} {V₁ : Type u_9} {V₂ : Type u_10} {V₁' : Type u_11} {V₂' : Type u_12} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup N₁'] [AddCommGroup N₂'] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₁'] [AddCommGroup V₂'] [Module ℝ V₁] [Module ℝ V₂] [Module ℝ V₁'] [Module ℝ V₂'] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {i₁' : N₁' →+ V₁'} {i₂' : N₂' →+ V₂'} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} {Ψ₁ : Fan i₁'} {Ψ₂ : Fan i₂'} (f : FanHom Φ₁ Ψ₁) (g : FanHom Φ₂ Ψ₂) : (f.prodMap g).latticeMap = f.latticeMap.prodMap g.latticeMap

The integral map of a product morphism is the product of the integral maps.

@[simp]

theorem TauCeti.Toric.FanHom.prodMap_realMap {N₁ : Type u_5} {N₂ : Type u_6} {N₁' : Type u_7} {N₂' : Type u_8} {V₁ : Type u_9} {V₂ : Type u_10} {V₁' : Type u_11} {V₂' : Type u_12} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup N₁'] [AddCommGroup N₂'] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₁'] [AddCommGroup V₂'] [Module ℝ V₁] [Module ℝ V₂] [Module ℝ V₁'] [Module ℝ V₂'] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {i₁' : N₁' →+ V₁'} {i₂' : N₂' →+ V₂'} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} {Ψ₁ : Fan i₁'} {Ψ₂ : Fan i₂'} (f : FanHom Φ₁ Ψ₁) (g : FanHom Φ₂ Ψ₂) : (f.prodMap g).realMap = f.realMap.prodMap g.realMap

The real-linear map of a product morphism is the product of the real-linear maps.

@[simp]

theorem TauCeti.Toric.FanHom.fst_comp_prodMap {N₁ : Type u_5} {N₂ : Type u_6} {N₁' : Type u_7} {N₂' : Type u_8} {V₁ : Type u_9} {V₂ : Type u_10} {V₁' : Type u_11} {V₂' : Type u_12} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup N₁'] [AddCommGroup N₂'] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₁'] [AddCommGroup V₂'] [Module ℝ V₁] [Module ℝ V₂] [Module ℝ V₁'] [Module ℝ V₂'] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {i₁' : N₁' →+ V₁'} {i₂' : N₂' →+ V₂'} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} {Ψ₁ : Fan i₁'} {Ψ₂ : Fan i₂'} (f : FanHom Φ₁ Ψ₁) (g : FanHom Φ₂ Ψ₂) : (fst Ψ₁ Ψ₂).comp (f.prodMap g) = f.comp (fst Φ₁ Φ₂)

The first projection commutes with componentwise products of fan morphisms.

@[simp]

theorem TauCeti.Toric.FanHom.snd_comp_prodMap {N₁ : Type u_5} {N₂ : Type u_6} {N₁' : Type u_7} {N₂' : Type u_8} {V₁ : Type u_9} {V₂ : Type u_10} {V₁' : Type u_11} {V₂' : Type u_12} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup N₁'] [AddCommGroup N₂'] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₁'] [AddCommGroup V₂'] [Module ℝ V₁] [Module ℝ V₂] [Module ℝ V₁'] [Module ℝ V₂'] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {i₁' : N₁' →+ V₁'} {i₂' : N₂' →+ V₂'} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} {Ψ₁ : Fan i₁'} {Ψ₂ : Fan i₂'} (f : FanHom Φ₁ Ψ₁) (g : FanHom Φ₂ Ψ₂) : (snd Ψ₁ Ψ₂).comp (f.prodMap g) = g.comp (snd Φ₁ Φ₂)

The second projection commutes with componentwise products of fan morphisms.

@[simp]

theorem TauCeti.Toric.FanHom.prodMap_id {N₁ : Type u_5} {N₂ : Type u_6} {V₁ : Type u_9} {V₂ : Type u_10} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup V₁] [AddCommGroup V₂] [Module ℝ V₁] [Module ℝ V₂] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} : (FanHom.id Φ₁).prodMap (FanHom.id Φ₂) = FanHom.id (Φ₁.prod Φ₂)

Products of identity fan morphisms are identity fan morphisms.

theorem TauCeti.Toric.FanHom.prodMap_comp {N₁ : Type u_5} {N₂ : Type u_6} {N₁' : Type u_7} {N₂' : Type u_8} {V₁ : Type u_9} {V₂ : Type u_10} {V₁' : Type u_11} {V₂' : Type u_12} [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup N₁'] [AddCommGroup N₂'] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₁'] [AddCommGroup V₂'] [Module ℝ V₁] [Module ℝ V₂] [Module ℝ V₁'] [Module ℝ V₂'] {i₁ : N₁ →+ V₁} {i₂ : N₂ →+ V₂} {i₁' : N₁' →+ V₁'} {i₂' : N₂' →+ V₂'} {Φ₁ : Fan i₁} {Φ₂ : Fan i₂} {Ψ₁ : Fan i₁'} {Ψ₂ : Fan i₂'} {N₁'' : Type u_13} {N₂'' : Type u_14} {V₁'' : Type u_15} {V₂'' : Type u_16} [AddCommGroup N₁''] [AddCommGroup N₂''] [AddCommGroup V₁''] [AddCommGroup V₂''] [Module ℝ V₁''] [Module ℝ V₂''] {i₁'' : N₁'' →+ V₁''} {i₂'' : N₂'' →+ V₂''} {Ω₁ : Fan i₁''} {Ω₂ : Fan i₂''} (f₁ : FanHom Φ₁ Ψ₁) (f₂ : FanHom Ψ₁ Ω₁) (g₁ : FanHom Φ₂ Ψ₂) (g₂ : FanHom Ψ₂ Ω₂) : (f₂.comp f₁).prodMap (g₂.comp g₁) = (f₂.prodMap g₂).comp (f₁.prodMap g₁)

Products commute with composition of fan morphisms.