The toric scheme of a finite fan

The affine toric schemes of the cones of a fan form a diagram indexed by the cones ordered by inclusion: an inclusion τ ≤ σ of cones of a fan is a face inclusion, and it acts by the face morphism from the affine toric scheme of τ to that of σ. Every face morphism is an open immersion. Moreover, the images of the charts of two faces τ and υ of a cone σ meet exactly in the image of the chart of τ ⊓ υ, which is again a cone of the fan, so the diagram is locally directed in the sense of CategoryTheory.Functor.IsLocallyDirected.

Integral supporting characters identify every face morphism with localization at a single monomial, including for singular cones. Thus the algebraic construction requires no regularity hypothesis. The empty fan is allowed as well.

Mathlib glues such a diagram of open immersions along the overlaps of its members (AlgebraicGeometry.Scheme.IsLocallyDirected), and identifies the result with the colimit of the diagram. This colimit is the toric scheme of the fan. Each affine toric chart is an open subscheme of it, the charts cover it, and two points of the charts of σ and τ are identified exactly when they come from a common point of the chart of σ ⊓ τ.

A morphism of fans sends the chart of each cone into the chart of its least target cone. These affine chart maps agree with the face localizations, so they descend through the colimit to a morphism of the associated toric schemes.

Main declarations

• TauCeti.Toric.Fan.affineToricDiagram: the diagram of affine toric charts of a fan.
• TauCeti.Toric.Fan.isLocallyDirected_affineToricDiagram: the chart diagram of every fan is locally directed.
• TauCeti.Toric.Fan.algebraicRealization: the toric scheme of a finite fan, the colimit of its diagram of affine toric charts.
• TauCeti.Toric.Fan.affineToricChartι: the open immersion of an affine toric chart into the toric scheme.
• TauCeti.Toric.Fan.exists_affineToricChartι_apply_eq: the affine toric charts cover the toric scheme.
• TauCeti.Toric.Fan.isIso_affineToricChartι_of_forall_le: when every cone of the fan is a face of one cone, the chart of that cone is the whole toric scheme; in particular for the fan of the faces of a single cone, TauCeti.Toric.Fan.isIso_affineToricChartι_ofCone.
• TauCeti.Toric.Fan.affineToricOpenCover: the cone-indexed affine open cover of the toric scheme.
• TauCeti.Toric.Fan.affineToricChartι_eq_affineToricChartι_iff: points of two charts are identified exactly along the chart of the intersection of the two cones.
• TauCeti.Toric.FanHom.affineToricChartMap: the affine chart map attached to a fan morphism.
• TauCeti.Toric.FanHom.algebraicMap: the morphism of toric schemes induced by a morphism of finite fans, obtained by descending the compatible chart maps.

References

• W. Fulton, Introduction to Toric Varieties, §§1.4 and 2.4.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §§3.1 and 3.3.

The diagram of affine toric charts

noncomputable def TauCeti.Toric.Fan.affineToricDiagram {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : CategoryTheory.Functor (↑Φ.cones) AlgebraicGeometry.Scheme

The diagram of affine toric charts of a fan, indexed by its cones ordered by inclusion. An inclusion τ ≤ σ acts by the face morphism from the chart of τ to the chart of σ.

@[simp]

theorem TauCeti.Toric.Fan.affineToricDiagram_obj {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : Φ.affineToricDiagram.obj σ = Φ.affineToricChart σ

The diagram of affine toric charts sends a cone to its affine toric chart.

@[simp]

theorem TauCeti.Toric.Fan.affineToricDiagram_map {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {τ σ : ↑Φ.cones} (f : τ ⟶ σ) : Φ.affineToricDiagram.map f = faceAffineToricSchemeMap ⋯ ⋯

The diagram of affine toric charts sends an inclusion of cones to the face morphism.

theorem TauCeti.Toric.Fan.isOpenImmersion_affineToricDiagram_map {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} {τ σ : ↑Φ.cones} (f : τ ⟶ σ) : AlgebraicGeometry.IsOpenImmersion (Φ.affineToricDiagram.map f)

Every morphism of the diagram of affine toric charts is an open immersion.

theorem TauCeti.Toric.Fan.isLocallyDirected_affineToricDiagram {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} : (Φ.affineToricDiagram.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected

The diagram of affine toric charts of a fan is locally directed: if points of the charts of two faces τ and υ of a cone σ have the same image in the chart of σ, they come from a common point of the chart of τ ⊓ υ.

The toric scheme of a finite fan

noncomputable def TauCeti.Toric.Fan.algebraicRealization {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : AlgebraicGeometry.Scheme

The toric scheme of a finite fan: the colimit of its diagram of affine toric charts, which glues the charts along the open immersions of their faces. No regularity is required.

noncomputable def TauCeti.Toric.Fan.affineToricChartι {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : Φ.affineToricChart σ ⟶ Φ.algebraicRealization

The inclusion of the affine toric chart of a cone into the toric scheme of a finite fan.

noncomputable def TauCeti.Toric.Fan.affineToricCocone {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : CategoryTheory.Limits.Cocone Φ.affineToricDiagram

The colimit cocone from the affine toric charts to the toric scheme of a finite fan.

@[simp]

theorem TauCeti.Toric.Fan.affineToricCocone_pt {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : Φ.affineToricCocone.pt = Φ.algebraicRealization

The point of the affine toric cocone is the toric scheme.

@[simp]

theorem TauCeti.Toric.Fan.affineToricCocone_ι_app {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : Φ.affineToricCocone.ι.app σ = Φ.affineToricChartι σ

The legs of the affine toric cocone are the affine chart inclusions.

noncomputable def TauCeti.Toric.Fan.isColimitAffineToricCocone {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : CategoryTheory.Limits.IsColimit Φ.affineToricCocone

The affine toric cocone is a colimit cocone.

theorem TauCeti.Toric.Fan.algebraicRealization_hom_ext {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {X : AlgebraicGeometry.Scheme} {g h : Φ.algebraicRealization ⟶ X} (H : ∀ (σ : ↑Φ.cones), CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι σ) g = CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι σ) h) : g = h

Morphisms from a fan's algebraic realization are determined by their affine chart maps.

theorem TauCeti.Toric.Fan.algebraicRealization_hom_ext_iff {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} {X : AlgebraicGeometry.Scheme} {g h : Φ.algebraicRealization ⟶ X} : g = h ↔ ∀ (σ : ↑Φ.cones), CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι σ) g = CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι σ) h

instance TauCeti.Toric.Fan.isOpenImmersion_affineToricChartι {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) : AlgebraicGeometry.IsOpenImmersion (Φ.affineToricChartι σ)

Each affine toric chart is an open subscheme of the toric scheme of a finite fan.

@[simp]

theorem TauCeti.Toric.Fan.faceAffineToricSchemeMap_comp_affineToricChartι {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} {τ σ : ↑Φ.cones} (h : (↑τ).IsFaceOf ↑σ) : CategoryTheory.CategoryStruct.comp (faceAffineToricSchemeMap ⋯ h) (Φ.affineToricChartι σ) = Φ.affineToricChartι τ

The inclusion of the chart of a face factors through the face morphism into the chart of the ambient cone.

@[simp]

theorem TauCeti.Toric.Fan.faceAffineToricSchemeMap_comp_affineToricChartι_assoc {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} {τ σ : ↑Φ.cones} (h : (↑τ).IsFaceOf ↑σ) {Z : AlgebraicGeometry.Scheme} (h✝ : Φ.algebraicRealization ⟶ Z) : CategoryTheory.CategoryStruct.comp (faceAffineToricSchemeMap ⋯ h) (CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι σ) h✝) = CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι τ) h✝

The inclusion of the chart of a face factors through the face morphism into the chart of the ambient cone.

theorem TauCeti.Toric.Fan.affineToricOverlapLeft_comp_affineToricChartι {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : CategoryTheory.CategoryStruct.comp (Φ.affineToricOverlapLeft σ τ) (Φ.affineToricChartι σ) = Φ.affineToricChartι (σ ⊓ τ)

The left overlap map followed by its chart inclusion is the inclusion of the overlap chart.

theorem TauCeti.Toric.Fan.affineToricOverlapLeft_comp_affineToricChartι_assoc {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) {Z : AlgebraicGeometry.Scheme} (h : Φ.algebraicRealization ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.affineToricOverlapLeft σ τ) (CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι σ) h) = CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι (σ ⊓ τ)) h

The left overlap map followed by its chart inclusion is the inclusion of the overlap chart.

theorem TauCeti.Toric.Fan.affineToricOverlapRight_comp_affineToricChartι {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : CategoryTheory.CategoryStruct.comp (Φ.affineToricOverlapRight σ τ) (Φ.affineToricChartι τ) = Φ.affineToricChartι (σ ⊓ τ)

The right overlap map followed by its chart inclusion is the inclusion of the overlap chart.

theorem TauCeti.Toric.Fan.affineToricOverlapRight_comp_affineToricChartι_assoc {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) {Z : AlgebraicGeometry.Scheme} (h : Φ.algebraicRealization ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.affineToricOverlapRight σ τ) (CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι τ) h) = CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι (σ ⊓ τ)) h

The right overlap map followed by its chart inclusion is the inclusion of the overlap chart.

theorem TauCeti.Toric.Fan.affineToricOverlap_comp_affineToricChartι {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : CategoryTheory.CategoryStruct.comp (Φ.affineToricOverlapLeft σ τ) (Φ.affineToricChartι σ) = CategoryTheory.CategoryStruct.comp (Φ.affineToricOverlapRight σ τ) (Φ.affineToricChartι τ)

The two inclusions of a pairwise overlap into the toric scheme agree.

theorem TauCeti.Toric.Fan.exists_affineToricChartι_apply_eq {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (x : ↥Φ.algebraicRealization) : ∃ (σ : ↑Φ.cones) (y : ↥(Φ.affineToricChart σ)), (Φ.affineToricChartι σ) y = x

Every point of the toric scheme of a finite fan lies in one of its affine toric charts.

theorem TauCeti.Toric.Fan.affineToricChartι_eq_affineToricChartι_iff {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {σ τ : ↑Φ.cones} (x : ↥(Φ.affineToricChart σ)) (y : ↥(Φ.affineToricChart τ)) : (Φ.affineToricChartι σ) x = (Φ.affineToricChartι τ) y ↔ ∃ (z : ↥(Φ.affineToricOverlap σ τ)), (Φ.affineToricOverlapLeft σ τ) z = x ∧ (Φ.affineToricOverlapRight σ τ) z = y

Points of the affine toric charts of two cones σ and τ of a finite fan have the same image in the toric scheme exactly when they come from a common point of the chart of σ ⊓ τ.

@[simp]

theorem TauCeti.Toric.Fan.range_affineToricChartι_inter_range_affineToricChartι {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : Set.range ⇑(Φ.affineToricChartι σ) ∩ Set.range ⇑(Φ.affineToricChartι τ) = Set.range ⇑(Φ.affineToricChartι (σ ⊓ τ))

The intersection of two affine cone opens is the affine open of the intersection cone.

theorem TauCeti.Toric.Fan.affineToricChartι_surjective_of_forall_le {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {σ : ↑Φ.cones} (h : ∀ (τ : ↑Φ.cones), τ ≤ σ) : Function.Surjective ⇑(Φ.affineToricChartι σ)

If every cone of a fan is a face of σ, the chart of σ covers the whole toric scheme.

theorem TauCeti.Toric.Fan.isIso_affineToricChartι_of_forall_le {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {σ : ↑Φ.cones} (h : ∀ (τ : ↑Φ.cones), τ ≤ σ) : CategoryTheory.IsIso (Φ.affineToricChartι σ)

If every cone of a fan is a face of σ, the toric scheme of the fan is the affine toric scheme of σ: the chart inclusion of σ is an isomorphism.

instance TauCeti.Toric.Fan.isIso_affineToricChartι_ofCone {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) : CategoryTheory.IsIso ((ofCone hi hσ).affineToricChartι ⟨σ, ⋯⟩)

The toric scheme of the fan of the faces of a toric cone σ is the affine toric scheme of σ: the chart inclusion of σ is an isomorphism.

noncomputable def TauCeti.Toric.Fan.affineToricOpenCover {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : Φ.algebraicRealization.OpenCover

The canonical affine open cover of the scheme of a finite fan, indexed by its cones.

@[simp]

theorem TauCeti.Toric.Fan.affineToricOpenCover_X {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : Φ.affineToricOpenCover.X σ = Φ.affineToricChart σ

@[simp]

theorem TauCeti.Toric.Fan.affineToricOpenCover_f {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : Φ.affineToricOpenCover.f σ = Φ.affineToricChartι σ

@[instance_reducible]

instance TauCeti.Toric.Fan.instCategoryI₀SchemeAffineToricOpenCover {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : CategoryTheory.Category.{u_2, u_2} Φ.affineToricOpenCover.I₀

The cones of a fan index its affine toric open cover, ordered by inclusion.

@[instance_reducible]

noncomputable instance TauCeti.Toric.Fan.instLocallyDirectedIsOpenImmersionAffineToricOpenCover {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : AlgebraicGeometry.Scheme.Cover.LocallyDirected Φ.affineToricOpenCover

The affine toric open cover is locally directed: its transition maps are the face morphisms, and the overlap of the charts of σ and τ is covered by the chart of σ ⊓ τ.

@[simp]

theorem TauCeti.Toric.Fan.affineToricOpenCover_trans {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {τ σ : ↑Φ.cones} (f : τ ⟶ σ) : AlgebraicGeometry.Scheme.Cover.trans Φ.affineToricOpenCover f = faceAffineToricSchemeMap ⋯ ⋯

The transition maps of the affine toric open cover are the face morphisms.

Morphisms of toric schemes

noncomputable def TauCeti.Toric.FanHom.affineToricChartMap {N N' : Type u} {V : Type u_1} {V' : Type u_2} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (σ : ↑Φ.cones) : Φ.affineToricChart σ ⟶ Ψ.affineToricChart ⟨f.leastCone ⋯, ⋯⟩

The affine morphism from a source chart to the chart of the least target cone containing its image.

theorem TauCeti.Toric.FanHom.affineToricChartMap_def {N N' : Type u} {V : Type u_1} {V' : Type u_2} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (σ : ↑Φ.cones) : f.affineToricChartMap σ = affineToricSchemeMap ⋯ ⋯ f.latticeMap f.realMap ⋯ ⋯

The affine chart map is induced by the fan morphism's lattice and real maps.

@[simp]

theorem TauCeti.Toric.FanHom.faceAffineToricSchemeMap_comp_affineToricChartMap {N N' : Type u} {V : Type u_1} {V' : Type u_2} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) {τ σ : ↑Φ.cones} (h : (↑τ).IsFaceOf ↑σ) : CategoryTheory.CategoryStruct.comp (faceAffineToricSchemeMap ⋯ h) (f.affineToricChartMap σ) = CategoryTheory.CategoryStruct.comp (f.affineToricChartMap τ) (faceAffineToricSchemeMap ⋯ ⋯)

The affine chart maps induced by a fan morphism commute with face inclusions.

@[simp]

theorem TauCeti.Toric.FanHom.faceAffineToricSchemeMap_comp_affineToricChartMap_assoc {N N' : Type u} {V : Type u_1} {V' : Type u_2} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) {τ σ : ↑Φ.cones} (h : (↑τ).IsFaceOf ↑σ) {Z : AlgebraicGeometry.Scheme} (h✝ : Ψ.affineToricChart ⟨f.leastCone ⋯, ⋯⟩ ⟶ Z) : CategoryTheory.CategoryStruct.comp (faceAffineToricSchemeMap ⋯ h) (CategoryTheory.CategoryStruct.comp (f.affineToricChartMap σ) h✝) = CategoryTheory.CategoryStruct.comp (f.affineToricChartMap τ) (CategoryTheory.CategoryStruct.comp (faceAffineToricSchemeMap ⋯ ⋯) h✝)

The affine chart maps induced by a fan morphism commute with face inclusions.

noncomputable def TauCeti.Toric.FanHom.algebraicMap {N N' : Type u} {V : Type u_1} {V' : Type u_2} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) : Φ.algebraicRealization ⟶ Ψ.algebraicRealization

A fan morphism induces a morphism of the algebraic realizations of its finite fans.

@[simp]

theorem TauCeti.Toric.FanHom.affineToricChartι_comp_algebraicMap {N N' : Type u} {V : Type u_1} {V' : Type u_2} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (σ : ↑Φ.cones) : CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι σ) f.algebraicMap = CategoryTheory.CategoryStruct.comp (f.affineToricChartMap σ) (Ψ.affineToricChartι ⟨f.leastCone ⋯, ⋯⟩)

On every affine chart, the global algebraic map is the affine toric map into the least target chart, followed by that chart's inclusion.

@[simp]

theorem TauCeti.Toric.FanHom.affineToricChartι_comp_algebraicMap_assoc {N N' : Type u} {V : Type u_1} {V' : Type u_2} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (σ : ↑Φ.cones) {Z : AlgebraicGeometry.Scheme} (h : Ψ.algebraicRealization ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι σ) (CategoryTheory.CategoryStruct.comp f.algebraicMap h) = CategoryTheory.CategoryStruct.comp (f.affineToricChartMap σ) (CategoryTheory.CategoryStruct.comp (Ψ.affineToricChartι ⟨f.leastCone ⋯, ⋯⟩) h)

On every affine chart, the global algebraic map is the affine toric map into the least target chart, followed by that chart's inclusion.

theorem TauCeti.Toric.FanHom.affineToricChartι_comp_algebraicMap_of_leastCone_eq {N N' : Type u} {V : Type u_1} {V' : Type u_2} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (σ : ↑Φ.cones) (τ : ↑Ψ.cones) (h : f.leastCone ⋯ = ↑τ) (hmaps : Set.MapsTo ⇑f.realMap ↑↑σ ↑↑τ) : CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι σ) f.algebraicMap = CategoryTheory.CategoryStruct.comp (affineToricSchemeMap ⋯ ⋯ f.latticeMap f.realMap ⋯ hmaps) (Ψ.affineToricChartι τ)

If the least target cone containing the image of σ is τ, then on the chart of σ the global algebraic map is the affine toric map into the chart of τ, followed by that chart's inclusion.

@[simp]

theorem TauCeti.Toric.FanHom.algebraicMap_id {N : Type u} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : (FanHom.id Φ).algebraicMap = CategoryTheory.CategoryStruct.id Φ.algebraicRealization

The algebraic map induced by the identity fan morphism is the identity.

@[simp]

theorem TauCeti.Toric.FanHom.algebraicMap_comp {N N' : Type u} {V : Type u_1} {V' : Type u_2} [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} {V'' : Type u_3} [AddCommGroup N''] [AddCommGroup V''] [Module ℝ V''] {i'' : N'' →+ V''} {Ω : Fan i''} (g : FanHom Ψ Ω) (f : FanHom Φ Ψ) : (g.comp f).algebraicMap = CategoryTheory.CategoryStruct.comp f.algebraicMap g.algebraicMap

The algebraic map induced by a composite fan morphism is the composite of the induced maps.