Finite fans of toric cones and their morphisms

A fan is the combinatorial datum from which a toric variety is glued: a finite family of toric cones in one real vector space, closed under passing to faces, and such that the intersection of any two members is a face of each of them. This file defines fans and their morphisms, computes the elementary consequences of the axioms, and proves the functoriality of the support.

The two axioms have complementary roles. Closure under faces makes the affine charts of a fan overlap in charts of the same family, and the intersection axiom makes those overlaps open immersions on both sides. Together they force the zero cone into every nonempty fan, which is why every affine chart of a fan contains the dense torus.

Main declarations

• TauCeti.Toric.Fan: a finite fan of toric cones for a lattice map i : N →+ V.
• TauCeti.Toric.Fan.inf_mem and TauCeti.Toric.Fan.bot_mem: the intersection of two cones of a fan is again one, and the zero cone belongs to every nonempty fan.
• TauCeti.Toric.Fan.support and TauCeti.Toric.Fan.IsComplete: the union of the cones of a fan, and the condition that it fills the ambient real vector space.
• TauCeti.Toric.Fan.ofCone: the faces of a single toric cone form a fan, whose support is that cone. This is the fan of an affine toric variety.
• TauCeti.Toric.Fan.ofCones: the faces of finitely many toric cones, any two of which meet in a face of each, form a fan, whose support is the union of those cones.
• TauCeti.Toric.Fan.subfan: a subset of the cones of a fan which is closed under faces is a fan, and TauCeti.Toric.Fan.ofCone_eq_subfan identifies the subfan of the faces of a cone of a fan with the fan of that cone. A subfan of a subfan is a subfan of the ambient fan, TauCeti.Toric.Fan.subfan_subfan. The cones not containing a given cone form a subfan, TauCeti.Toric.Fan.setOf_not_le_closedUnderFaces.
• TauCeti.Toric.FanHom: a morphism of fans, namely a map of the integral vectors, a compatible real-linear map, and the condition that every source cone lands in some target cone.
• TauCeti.Toric.FanHom.realMap_eq: the real-linear part of a fan morphism is determined by its integral part, so TauCeti.Toric.FanHom.ext needs only the latter.
• TauCeti.Toric.FanHom.id, TauCeti.Toric.FanHom.comp and the identity, unit and associativity laws they satisfy.
• TauCeti.Toric.Fan.subfanInclusion: the inclusion of a subfan, with TauCeti.Toric.Fan.subfanInclusion_self and TauCeti.Toric.Fan.subfanInclusion_comp_subfanInclusion making these inclusions functorial for nested subfans.
• TauCeti.Toric.FanHom.mapsTo_support: a fan morphism maps the support of its source into the support of its target.
• TauCeti.Toric.FanHom.exists_isLeast_cone: the target cones containing the image of a given source cone have a least element, so a fan morphism has a well-defined cone-by-cone description. TauCeti.Toric.FanHom.leastCone names that least target cone, and TauCeti.Toric.FanHom.leastCone_mono records its monotonicity, while TauCeti.Toric.FanHom.leastCone_isFaceOf transports face inclusions to the least cones.

Implementation notes

Closure under faces is stated with Mathlib's PointedCone.IsFaceOf rather than with its bundled face lattice PointedCone.Face; the two are interchangeable, and the unbundled form avoids a coercion at every use site.

Only the left half (σ ⊓ τ).IsFaceOf σ of the intersection axiom is a field: its right half is the same statement with the two cones exchanged, and TauCeti.Toric.Fan.inf_isFaceOf_right derives it.

The body of TauCeti.Toric.Fan.subfan is exposed, so that a subfan of a subfan is by definition the subfan of the ambient fan on the same cones (TauCeti.Toric.Fan.subfan_subfan), and the subfan of a fan on all of its cones is the fan itself (TauCeti.Toric.Fan.subfan_self). The functoriality of subfan inclusions and of the maps they induce is stated across these definitional equalities of fans.

A Fan carries the proof that its ambient lattice map is an integral lattice. This makes the real-linear extension of a map of integral vectors exist and be unique, so the real-linear part of a fan morphism is determined by its integral part rather than being an independent choice.

References

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

structure TauCeti.Toric.Fan {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] (i : N →+ V) : Type u_3

A finite fan for the lattice map i : N →+ V is a finite family of toric cones in V, closed under passing to faces, whose pairwise intersections are faces of both members.

• lattice : IsIntegralLattice i

  The ambient map of integral vectors is an integral lattice.

• cones : Set (PointedCone ℝ V)

  The cones of the fan.

• finite_cones : self.cones.Finite

  A fan has finitely many cones.

• isToricCone ⦃σ : PointedCone ℝ V⦄ : σ ∈ self.cones → IsToricCone i σ

  Every cone of a fan is a toric cone.

• mem_of_isFaceOf ⦃σ τ : PointedCone ℝ V⦄ : σ ∈ self.cones → τ.IsFaceOf σ → τ ∈ self.cones

  The cones of a fan are closed under passing to faces.

• inf_isFaceOf_left ⦃σ τ : PointedCone ℝ V⦄ : σ ∈ self.cones → τ ∈ self.cones → (σ ⊓ τ).IsFaceOf σ

  The intersection of two cones of a fan is a face of the first one. Exchanging the two cones gives the same statement for the second one, so only this half is a field.

theorem TauCeti.Toric.Fan.ext {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ : Fan i} (h : Φ.cones = Ψ.cones) : Φ = Ψ

A fan is determined by its set of cones.

theorem TauCeti.Toric.Fan.ext_iff {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ : Fan i} : Φ = Ψ ↔ Φ.cones = Ψ.cones

theorem TauCeti.Toric.Fan.inf_isFaceOf_right {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (Φ : Fan i) (hσ : σ ∈ Φ.cones) (hτ : τ ∈ Φ.cones) : (σ ⊓ τ).IsFaceOf τ

The intersection of two cones of a fan is a face of the second one.

theorem TauCeti.Toric.Fan.inf_mem {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (Φ : Fan i) (hσ : σ ∈ Φ.cones) (hτ : τ ∈ Φ.cones) : σ ⊓ τ ∈ Φ.cones

The intersection of two cones of a fan is again a cone of the fan: it is a face of each of them, and the cones of a fan are closed under faces.

@[instance_reducible]

instance TauCeti.Toric.Fan.instSemilatticeInfElemPointedConeRealCones {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : SemilatticeInf ↑Φ.cones

The cones of a fan form a meet-semilattice under inclusion, with intersection as meet.

@[simp]

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

Coercing the intersection of two fan cones gives their intersection as pointed cones.

instance TauCeti.Toric.Fan.instFiniteElemPointedConeRealCones {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : Finite ↑Φ.cones

A fan has finitely many cones.

theorem TauCeti.Toric.Fan.isFaceOf_of_le {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (Φ : Fan i) (hσ : σ ∈ Φ.cones) (hτ : τ ∈ Φ.cones) (h : τ ≤ σ) : τ.IsFaceOf σ

An inclusion of cones of a fan is a face inclusion: if τ ≤ σ, then τ = τ ⊓ σ is a face of σ.

theorem TauCeti.Toric.Fan.bot_mem {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (Φ : Fan i) (hσ : σ ∈ Φ.cones) : ⊥ ∈ Φ.cones

A nonempty fan contains the zero cone. Its affine chart is the dense torus, which is therefore an open subset of every chart of the fan.

Support and completeness

def TauCeti.Toric.Fan.support {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : Set V

The support of a fan is the union of its cones.

@[simp]

theorem TauCeti.Toric.Fan.mem_support {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {x : V} : x ∈ Φ.support ↔ ∃ σ ∈ Φ.cones, x ∈ σ

A point lies in the support of a fan exactly when some cone of the fan contains it.

theorem TauCeti.Toric.Fan.subset_support {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (Φ : Fan i) (hσ : σ ∈ Φ.cones) : ↑σ ⊆ Φ.support

theorem TauCeti.Toric.Fan.zero_mem_support {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (Φ : Fan i) (hσ : σ ∈ Φ.cones) : 0 ∈ Φ.support

The origin lies in the support of every nonempty fan.

def TauCeti.Toric.Fan.IsComplete {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : Prop

A fan is complete when its cones cover the ambient real vector space.

@[simp]

theorem TauCeti.Toric.Fan.isComplete_iff {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : Φ.IsComplete ↔ ∀ (x : V), ∃ σ ∈ Φ.cones, x ∈ σ

Completeness, spelled pointwise.

theorem TauCeti.Toric.Fan.IsComplete.nonempty_cones {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (h : Φ.IsComplete) : Nonempty ↑Φ.cones

A complete fan is nonempty: some cone contains the origin. In particular, the empty fan is not complete.

The fan of a single cone

def TauCeti.Toric.Fan.ofCone {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) : Fan i

The faces of a toric cone form a fan, the fan of the affine toric variety of that cone.

@[simp]

theorem TauCeti.Toric.Fan.mem_ofCone_cones {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) : τ ∈ (ofCone hi hσ).cones ↔ τ.IsFaceOf σ

The cones of the fan of a cone are exactly the faces of that cone.

@[simp]

theorem TauCeti.Toric.Fan.support_ofCone {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) : (ofCone hi hσ).support = ↑σ

The support of the fan of a cone is that cone.

The fan generated by finitely many cones

def TauCeti.Toric.Fan.ofCones {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (S : Set (PointedCone ℝ V)) (hS : S.Finite) (hSt : ∀ ⦃σ : PointedCone ℝ V⦄, σ ∈ S → IsToricCone i σ) (hSinf : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ ∈ S → (σ ⊓ τ).IsFaceOf σ) : Fan i

The faces of finitely many toric cones form a fan, provided that any two of these cones meet in a face of each.

@[simp]

theorem TauCeti.Toric.Fan.mem_ofCones_cones {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (S : Set (PointedCone ℝ V)) (hS : S.Finite) (hSt : ∀ ⦃σ : PointedCone ℝ V⦄, σ ∈ S → IsToricCone i σ) (hSinf : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ ∈ S → (σ ⊓ τ).IsFaceOf σ) : τ ∈ (ofCones hi S hS hSt hSinf).cones ↔ ∃ σ ∈ S, τ.IsFaceOf σ

The cones of the fan generated by finitely many cones are the faces of those cones.

theorem TauCeti.Toric.Fan.subset_ofCones_cones {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (S : Set (PointedCone ℝ V)) (hS : S.Finite) (hSt : ∀ ⦃σ : PointedCone ℝ V⦄, σ ∈ S → IsToricCone i σ) (hSinf : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ ∈ S → (σ ⊓ τ).IsFaceOf σ) : S ⊆ (ofCones hi S hS hSt hSinf).cones

The generating cones belong to the fan they generate.

@[simp]

theorem TauCeti.Toric.Fan.support_ofCones {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (S : Set (PointedCone ℝ V)) (hS : S.Finite) (hSt : ∀ ⦃σ : PointedCone ℝ V⦄, σ ∈ S → IsToricCone i σ) (hSinf : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ ∈ S → (σ ⊓ τ).IsFaceOf σ) : (ofCones hi S hS hSt hSinf).support = ⋃ σ ∈ S, ↑σ

The support of the fan generated by finitely many cones is their union.

Subfans

def TauCeti.Toric.Fan.subfan {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) : Fan i

A subset of the cones of a fan which is itself closed under passing to faces is a fan.

@[simp]

theorem TauCeti.Toric.Fan.subfan_cones {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) : (Φ.subfan S hS hface).cones = S

The cones of a subfan are the chosen subset.

instance TauCeti.Toric.Fan.instIsEmptyElemPointedConeRealConesSubfanEmptyCollectionSet {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hS : ∅ ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ ∅ → τ.IsFaceOf σ → τ ∈ ∅) : IsEmpty ↑(Φ.subfan ∅ hS hface).cones

The empty subfan of a fan has no cones.

@[simp]

theorem TauCeti.Toric.Fan.subfan_lattice {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) : ⋯ = ⋯

A subfan uses the ambient fan's integral lattice.

theorem TauCeti.Toric.Fan.support_subfan_subset {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) : (Φ.subfan S hS hface).support ⊆ Φ.support

The support of a subfan is contained in the support of the ambient fan.

@[simp]

theorem TauCeti.Toric.Fan.subfan_self {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : Φ.subfan Φ.cones ⋯ ⋯ = Φ

The subfan of a fan on all of its cones is the fan itself.

@[simp]

theorem TauCeti.Toric.Fan.subfan_subfan {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) (T : Set (PointedCone ℝ V)) (hT : T ⊆ (Φ.subfan S hS hface).cones) (hfaceT : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ T → τ.IsFaceOf σ → τ ∈ T) : (Φ.subfan S hS hface).subfan T hT hfaceT = Φ.subfan T ⋯ hfaceT

A subfan of a subfan is the subfan of the ambient fan on the same cones.

theorem TauCeti.Toric.Fan.isFaceOf_subset_cones {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (Φ : Fan i) (hσ : σ ∈ Φ.cones) : {τ : PointedCone ℝ V | τ.IsFaceOf σ} ⊆ Φ.cones

The faces of a cone of a fan are again cones of the fan, so they form a subfan of it.

theorem TauCeti.Toric.Fan.setOf_not_le_subset_cones {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : PointedCone ℝ V) : {τ : PointedCone ℝ V | τ ∈ Φ.cones ∧ ¬σ ≤ τ} ⊆ Φ.cones

The cones of a fan not containing a given cone are cones of the fan.

theorem TauCeti.Toric.Fan.setOf_not_le_closedUnderFaces {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : PointedCone ℝ V) ⦃τ υ : PointedCone ℝ V⦄ : τ ∈ {τ : PointedCone ℝ V | τ ∈ Φ.cones ∧ ¬σ ≤ τ} → υ.IsFaceOf τ → υ ∈ {τ : PointedCone ℝ V | τ ∈ Φ.cones ∧ ¬σ ≤ τ}

The cones of a fan not containing a given cone are closed under faces, so they form a subfan of it.

theorem TauCeti.Toric.Fan.ofCone_eq_subfan {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (Φ : Fan i) (hσ : σ ∈ Φ.cones) : ofCone ⋯ ⋯ = Φ.subfan {τ : PointedCone ℝ V | τ.IsFaceOf σ} ⋯ ⋯

The subfan of the faces of a cone of a fan is the fan of that cone.

Morphisms of fans

structure TauCeti.Toric.FanHom {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') : Type (max (max (max u_1 u_2) u_3) u_4)

A morphism of fans is a map of the integral vectors together with the compatible real-linear map, subject to the condition that every cone of the source lands inside some cone of the target.

• latticeMap : N →+ N'

  The underlying map of integral vectors.

• realMap : V →ₗ[ℝ] V'

  The real-linear map extending latticeMap.

• map_lattice (n : N) : self.realMap (i n) = i' (self.latticeMap n)

  The two maps agree on integral vectors.

• map_cone ⦃σ : PointedCone ℝ V⦄ : σ ∈ Φ.cones → ∃ τ ∈ Ψ.cones, PointedCone.map self.realMap σ ≤ τ

  Every cone of the source fan is carried into a cone of the target fan.

theorem TauCeti.Toric.FanHom.realMap_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'} (f : FanHom Φ Ψ) : f.realMap = ⋯.extend i' f.latticeMap

The real-linear part of a fan morphism is the scalar extension of its integral part. It is therefore determined by the integral part rather than being an independent choice.

theorem TauCeti.Toric.FanHom.ext {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'} {f g : FanHom Φ Ψ} (h : f.latticeMap = g.latticeMap) : f = g

A fan morphism is determined by its map of integral vectors.

theorem TauCeti.Toric.FanHom.ext_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'} {f g : FanHom Φ Ψ} : f = g ↔ f.latticeMap = g.latticeMap

noncomputable def TauCeti.Toric.FanHom.ofLatticeMap {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') (f : N →+ N') (hf : ∀ ⦃σ : PointedCone ℝ V⦄, σ ∈ Φ.cones → ∃ τ ∈ Ψ.cones, PointedCone.map (⋯.extend i' f) σ ≤ τ) : FanHom Φ Ψ

Build a fan morphism from a map of integral vectors alone, using that its real-linear part is forced to be the scalar extension.

@[simp]

theorem TauCeti.Toric.FanHom.ofLatticeMap_latticeMap {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') (f : N →+ N') (hf : ∀ ⦃σ : PointedCone ℝ V⦄, σ ∈ Φ.cones → ∃ τ ∈ Ψ.cones, PointedCone.map (⋯.extend i' f) σ ≤ τ) : (ofLatticeMap Φ Ψ f hf).latticeMap = f

The integral part of a fan morphism built from a map of integral vectors is that map.

@[simp]

theorem TauCeti.Toric.FanHom.ofLatticeMap_realMap {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') (f : N →+ N') (hf : ∀ ⦃σ : PointedCone ℝ V⦄, σ ∈ Φ.cones → ∃ τ ∈ Ψ.cones, PointedCone.map (⋯.extend i' f) σ ≤ τ) : (ofLatticeMap Φ Ψ f hf).realMap = ⋯.extend i' f

The real-linear part of a fan morphism built from a map of integral vectors is the scalar extension of that map.

def TauCeti.Toric.FanHom.id {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : FanHom Φ Φ

The identity morphism of a fan.

@[simp]

theorem TauCeti.Toric.FanHom.id_latticeMap {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : (FanHom.id Φ).latticeMap = AddMonoidHom.id N

The integral part of the identity morphism is the identity.

@[simp]

theorem TauCeti.Toric.FanHom.id_realMap {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : (FanHom.id Φ).realMap = LinearMap.id

The real-linear part of the identity morphism is the identity.

def TauCeti.Toric.FanHom.comp {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'} {N'' : Type u_5} {V'' : Type u_6} [AddCommGroup N''] [AddCommGroup V''] [Module ℝ V''] {i'' : N'' →+ V''} {Ω : Fan i''} (g : FanHom Ψ Ω) (f : FanHom Φ Ψ) : FanHom Φ Ω

The composite of two fan morphisms.

@[simp]

theorem TauCeti.Toric.FanHom.comp_latticeMap {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'} {N'' : Type u_5} {V'' : Type u_6} [AddCommGroup N''] [AddCommGroup V''] [Module ℝ V''] {i'' : N'' →+ V''} {Ω : Fan i''} (g : FanHom Ψ Ω) (f : FanHom Φ Ψ) : (g.comp f).latticeMap = g.latticeMap.comp f.latticeMap

The integral part of a composite is the composite of the integral parts.

@[simp]

theorem TauCeti.Toric.FanHom.comp_realMap {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'} {N'' : Type u_5} {V'' : Type u_6} [AddCommGroup N''] [AddCommGroup V''] [Module ℝ V''] {i'' : N'' →+ V''} {Ω : Fan i''} (g : FanHom Ψ Ω) (f : FanHom Φ Ψ) : (g.comp f).realMap = g.realMap ∘ₗ f.realMap

The real-linear part of a composite is the composite of the real-linear parts.

@[simp]

theorem TauCeti.Toric.FanHom.comp_id {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'} (f : FanHom Φ Ψ) : f.comp (FanHom.id Φ) = f

The identity morphism is a right unit for composition.

@[simp]

theorem TauCeti.Toric.FanHom.id_comp {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'} (f : FanHom Φ Ψ) : (FanHom.id Ψ).comp f = f

The identity morphism is a left unit for composition.

theorem TauCeti.Toric.FanHom.comp_assoc {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'} {N'' : Type u_5} {V'' : Type u_6} [AddCommGroup N''] [AddCommGroup V''] [Module ℝ V''] {i'' : N'' →+ V''} {Ω : Fan i''} {N''' : Type u_7} {V''' : Type u_8} [AddCommGroup N'''] [AddCommGroup V'''] [Module ℝ V'''] {i''' : N''' →+ V'''} {Θ : Fan i'''} (h : FanHom Ω Θ) (g : FanHom Ψ Ω) (f : FanHom Φ Ψ) : (h.comp g).comp f = h.comp (g.comp f)

Composition of fan morphisms is associative.

Functoriality of the support

theorem TauCeti.Toric.FanHom.mapsTo_support {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'} (f : FanHom Φ Ψ) : Set.MapsTo (⇑f.realMap) Φ.support Ψ.support

A fan morphism carries the support of its source fan into the support of its target fan.

The least target cone of a source cone

theorem TauCeti.Toric.FanHom.exists_isLeast_cone {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'} {σ : PointedCone ℝ V} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hσ : σ ∈ Φ.cones) : ∃ (τ : PointedCone ℝ V'), IsLeast {υ : PointedCone ℝ V' | υ ∈ Ψ.cones ∧ PointedCone.map f.realMap σ ≤ υ} τ

The cones of the target fan which contain the image of a fixed source cone have a least element. A fan morphism therefore has a well-defined cone-by-cone description: each affine chart of the source maps to a unique smallest affine chart of the target.

noncomputable def TauCeti.Toric.FanHom.leastCone {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'} {σ : PointedCone ℝ V} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hσ : σ ∈ Φ.cones) : PointedCone ℝ V'

The least cone of the target fan containing the image of a source cone.

theorem TauCeti.Toric.FanHom.isLeast_leastCone {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'} {σ : PointedCone ℝ V} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hσ : σ ∈ Φ.cones) : IsLeast {υ : PointedCone ℝ V' | υ ∈ Ψ.cones ∧ PointedCone.map f.realMap σ ≤ υ} (f.leastCone hσ)

FanHom.leastCone is the least target cone containing the image of the source cone.

theorem TauCeti.Toric.FanHom.leastCone_mem {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'} {σ : PointedCone ℝ V} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hσ : σ ∈ Φ.cones) : f.leastCone hσ ∈ Ψ.cones

The least target cone of a source cone is a cone of the target fan.

theorem TauCeti.Toric.FanHom.map_le_leastCone {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'} {σ : PointedCone ℝ V} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hσ : σ ∈ Φ.cones) : PointedCone.map f.realMap σ ≤ f.leastCone hσ

The least target cone of a source cone contains the image of that cone.

theorem TauCeti.Toric.FanHom.mapsTo_leastCone {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'} {σ : PointedCone ℝ V} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hσ : σ ∈ Φ.cones) : Set.MapsTo ⇑f.realMap ↑σ ↑(f.leastCone hσ)

The real map of a fan morphism carries a source cone into its least target cone.

theorem TauCeti.Toric.FanHom.leastCone_le {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'} {σ : PointedCone ℝ V} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hσ : σ ∈ Φ.cones) {υ : PointedCone ℝ V'} (hυ : υ ∈ Ψ.cones) (h : PointedCone.map f.realMap σ ≤ υ) : f.leastCone hσ ≤ υ

The least target cone of a source cone lies in every target cone containing its image.

theorem TauCeti.Toric.FanHom.leastCone_mono {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'} (f : FanHom Φ Ψ) {τ σ : PointedCone ℝ V} (hτ : τ ∈ Φ.cones) (hσ : σ ∈ Φ.cones) (h : τ ≤ σ) : f.leastCone hτ ≤ f.leastCone hσ

The least target cone is monotone in the source cone.

theorem TauCeti.Toric.FanHom.leastCone_isFaceOf {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'} (f : FanHom Φ Ψ) {τ σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) (h : τ.IsFaceOf σ) : (f.leastCone ⋯).IsFaceOf (f.leastCone hσ)

The least target cones preserve face inclusions.

noncomputable def TauCeti.Toric.Fan.subfanInclusion {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) : FanHom (Φ.subfan S hS hface) Φ

The inclusion of a subfan in its ambient fan, as a fan morphism with identity lattice and real maps.

@[simp]

theorem TauCeti.Toric.Fan.subfanInclusion_latticeMap {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) : (Φ.subfanInclusion S hS hface).latticeMap = AddMonoidHom.id N

@[simp]

theorem TauCeti.Toric.Fan.subfanInclusion_realMap {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) : (Φ.subfanInclusion S hS hface).realMap = LinearMap.id

@[simp]

theorem TauCeti.Toric.Fan.subfanInclusion_leastCone {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) (σ : ↑(Φ.subfan S hS hface).cones) : (Φ.subfanInclusion S hS hface).leastCone ⋯ = ↑σ

The least ambient cone containing a cone of a subfan is that cone itself.

@[simp]

theorem TauCeti.Toric.Fan.subfanInclusion_self {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : Φ.subfanInclusion Φ.cones ⋯ ⋯ = FanHom.id Φ

The inclusion of a fan in itself, as the subfan on all of its cones, is the identity.

@[simp]

theorem TauCeti.Toric.Fan.subfanInclusion_comp_subfanInclusion {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) (T : Set (PointedCone ℝ V)) (hT : T ⊆ (Φ.subfan S hS hface).cones) (hfaceT : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ T → τ.IsFaceOf σ → τ ∈ T) : (Φ.subfanInclusion S hS hface).comp ((Φ.subfan S hS hface).subfanInclusion T hT hfaceT) = Φ.subfanInclusion T ⋯ hfaceT

The inclusions of open subfans compose: including a subfan of a subfan in the subfan and then the subfan in the ambient fan is including it directly in the ambient fan.