Transport of toric rays along lattice equivalences

A linear equivalence of ambient real vector spaces sends a ray of a pointed cone to a ray of the image cone. When it is compatible with an equivalence of integral lattices, it also sends the primitive lattice generator of the ray to the primitive generator of the image ray.

This is the coordinate-free naturality needed when a toric cone is transported to an isomorphic lattice. In particular, the canonical primitive generator does not depend on presenting the lattice and its ambient real vector space in particular coordinates.

Main declarations

• TauCeti.Toric.ToricRay.map: the image ray under a real-linear equivalence.
• TauCeti.Toric.ToricRay.mapLinearEquiv: the induced equivalence between the ray types.
• TauCeti.Toric.IsPrimitiveGenerator.map_equiv: transport of an arbitrary primitive generator under compatible integral and real equivalences.
• TauCeti.Toric.primitiveGenerator_map_equiv: naturality of the canonical primitive generator.

References

The construction is the invariance of primitive ray generators under a lattice isomorphism; see W. Fulton, Introduction to Toric Varieties, §1.2, and D. Cox, J. Little and H. Schenck, Toric Varieties, §1.2.

def TauCeti.Toric.ToricRay.map {V : Type u_3} {V' : Type u_4} [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {σ : PointedCone ℝ V} (rho : ToricRay σ) (e : V ≃ₗ[ℝ] V') : ToricRay (PointedCone.map (↑e) σ)

The image of a ray under a real-linear equivalence, regarded as a ray of the image cone.

@[simp]

theorem TauCeti.Toric.ToricRay.toPointedCone_map {V : Type u_3} {V' : Type u_4} [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {σ : PointedCone ℝ V} (rho : ToricRay σ) (e : V ≃ₗ[ℝ] V') : (rho.map e).toPointedCone = PointedCone.map (↑e) rho.toPointedCone

The pointed cone underlying the image ray is the image of the original ray's cone.

@[simp]

theorem TauCeti.Toric.ToricRay.mem_map {V : Type u_3} {V' : Type u_4} [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {σ : PointedCone ℝ V} (rho : ToricRay σ) (e : V ≃ₗ[ℝ] V') (x : V') : x ∈ rho.map e ↔ e.symm x ∈ rho

A vector belongs to the image ray exactly when it is the image of a vector in the original ray.

@[simp]

theorem TauCeti.Toric.ToricRay.map_id {V : Type u_3} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} (rho : ToricRay σ) : cast ⋯ (rho.map (LinearEquiv.refl ℝ V)) = rho

Transporting a ray along the identity equivalence is the original ray, after identifying the image cone with the original cone.

@[simp]

theorem TauCeti.Toric.ToricRay.map_comp {V : Type u_3} {V' : Type u_4} [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {σ : PointedCone ℝ V} {V'' : Type u_5} [AddCommGroup V''] [Module ℝ V''] (rho : ToricRay σ) (e : V ≃ₗ[ℝ] V') (e' : V' ≃ₗ[ℝ] V'') : cast ⋯ ((rho.map e).map e') = rho.map (e ≪≫ₗ e')

Successive transports of a ray agree with transport along the composite equivalence, after identifying the iterated image cone with the image under the composite.

noncomputable def TauCeti.Toric.ToricRay.mapLinearEquiv {V : Type u_3} {V' : Type u_4} [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {σ : PointedCone ℝ V} (e : V ≃ₗ[ℝ] V') : ToricRay σ ≃ ToricRay (PointedCone.map (↑e) σ)

A real-linear equivalence induces an equivalence between the rays of a cone and those of its image cone.

@[simp]

theorem TauCeti.Toric.ToricRay.mapLinearEquiv_apply {V : Type u_3} {V' : Type u_4} [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {σ : PointedCone ℝ V} (e : V ≃ₗ[ℝ] V') (rho : ToricRay σ) : (mapLinearEquiv e) rho = rho.map e

@[simp]

theorem TauCeti.Toric.ToricRay.mapLinearEquiv_refl {V : Type u_3} [AddCommGroup V] [Module ℝ V] {σ : PointedCone ℝ V} : (mapLinearEquiv (LinearEquiv.refl ℝ V)).trans (Equiv.cast ⋯) = Equiv.refl (ToricRay σ)

The ray equivalence induced by the identity linear equivalence is the identity, after identifying the image cone with the original cone.

@[simp]

theorem TauCeti.Toric.ToricRay.mapLinearEquiv_trans {V : Type u_3} {V' : Type u_4} [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {σ : PointedCone ℝ V} {V'' : Type u_5} [AddCommGroup V''] [Module ℝ V''] (e : V ≃ₗ[ℝ] V') (e' : V' ≃ₗ[ℝ] V'') : (mapLinearEquiv e).trans ((mapLinearEquiv e').trans (Equiv.cast ⋯)) = mapLinearEquiv (e ≪≫ₗ e')

Ray equivalences induced by successive linear equivalences compose to the ray equivalence induced by their composite, after identifying the two image cones.

@[simp]

theorem TauCeti.Toric.ToricRay.mapLinearEquiv_symm_apply {V : Type u_3} {V' : Type u_4} [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {σ : PointedCone ℝ V} (e : V ≃ₗ[ℝ] V') (tau : ToricRay (PointedCone.map (↑e) σ)) : (mapLinearEquiv e).symm tau = cast ⋯ (tau.map e.symm)

The inverse ray equivalence is transport along the inverse linear equivalence, after identifying the double image cone with the original cone.

theorem TauCeti.Toric.IsPrimitiveGenerator.map_equiv {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} {f : N ≃+ N'} {e : V ≃ₗ[ℝ] V'} (hfe : ∀ (n : N), e (i n) = i' (f n)) {rho : ToricRay σ} {v : N} (hv : IsPrimitiveGenerator i rho v) : IsPrimitiveGenerator i' (rho.map e) (f v)

A compatible pair of integral and real-linear equivalences sends a primitive generator to a primitive generator of the image ray.

theorem TauCeti.Toric.primitiveGenerator_map_equiv {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} {f : N ≃+ N'} {e : V ≃ₗ[ℝ] V'} (hfe : ∀ (n : N), e (i n) = i' (f n)) (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) (rho : ToricRay σ) : f (primitiveGenerator hi hσ rho) = primitiveGenerator ⋯ ⋯ (rho.map e)

The canonical primitive generator commutes with transport along compatible integral and real-linear equivalences.