Documentation

TauCeti.Geometry.Toric.Analytic.Fan.Subfan.Basic

The analytic realization of an open subfan #

A face-closed set of cones of a regular fan is itself a regular fan, TauCeti.Toric.Fan.subfan. The affine chart of one of its cones and the affine chart of the same cone in the ambient fan have the same underlying complex points, and their monomial-embedding topologies agree because that topology does not depend on the chosen finite generating family. These identity-on-points chart comparisons commute with the face maps of the two chart diagrams, so they glue to a continuous map from the realization of the subfan to the ambient realization.

Composed with the inclusion of the chart of a cone of the subfan, this map is the chart comparison followed by the inclusion of the chart of the same cone in the ambient realization. It is an open embedding whose image is the union of the ambient charts of the cones of the subfan. No nonemptiness assumption is made on the set of cones of the subfan.

Main declarations #

References #

Chart comparisons #

source
theorem TauCeti.Toric.Fan.subfan_analyticAffineChartDiagram_obj_str {N V : Type u} [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) :
((Φ.subfan S hS hface).analyticAffineChartDiagram.obj σ).str = (Φ.analyticAffineChartDiagram.obj ⟨↑σ, ⋯⟩).str

The chart of a cone of a subfan and the chart of the same cone in the ambient fan carry the same topology.

source
noncomputable def TauCeti.Toric.Fan.subfanAnalyticChartMap {N V : Type u} [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) :
↑((Φ.subfan S hS hface).analyticAffineChartDiagram.obj σ) ≃ₜ ↑(Φ.analyticAffineChartDiagram.obj ⟨↑σ, ⋯⟩)

The identity-on-points homeomorphism from the chart of a cone of a subfan to the chart of the same cone in the ambient fan.

Instances For
    source
    @[simp]
    theorem TauCeti.Toric.Fan.subfanAnalyticChartMap_apply {N V : Type u} [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) (x : ↑((Φ.subfan S hS hface).analyticAffineChartDiagram.obj σ)) :
    (Φ.subfanAnalyticChartMap S hS hface σ) x = x

    The chart comparison of a subfan is the identity on complex points.

    source
    @[simp]
    theorem TauCeti.Toric.Fan.subfanAnalyticChartMap_symm_apply {N V : Type u} [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) (x : ↑(Φ.analyticAffineChartDiagram.obj ⟨↑σ, ⋯⟩)) :
    (Φ.subfanAnalyticChartMap S hS hface σ).symm x = x

    The inverse chart comparison of a subfan is the identity on complex points.

    source
    theorem TauCeti.Toric.Fan.subfanAnalyticChartMap_map {N V : Type u} [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} (f : τ ⟶ σ) (x : ↑((Φ.subfan S hS hface).analyticAffineChartDiagram.obj τ)) :
    (Φ.subfanAnalyticChartMap S hS hface σ) ((CategoryTheory.ConcreteCategory.hom ((Φ.subfan S hS hface).analyticAffineChartDiagram.map f)) x) = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartDiagram.map (CategoryTheory.homOfLE ⋯))) ((Φ.subfanAnalyticChartMap S hS hface τ) x)

    The chart comparisons of a subfan commute with the face maps of the two chart diagrams.

    The glued map #

    source
    noncomputable def TauCeti.Toric.Fan.subfanAnalyticMap {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) :
    (Φ.subfan S hS hface).analyticRealization ⋯ ⟶ Φ.analyticRealization hΦ

    The map from the analytic realization of a subfan to the analytic realization of the ambient fan, glued from the chart comparisons followed by the ambient chart inclusions.

    Instances For
      source
      theorem TauCeti.Toric.Fan.analyticAffineChartι_comp_subfanAnalyticMap {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) (σ : ↑(Φ.subfan S hS hface).cones) :
      CategoryTheory.CategoryStruct.comp ((Φ.subfan S hS hface).analyticAffineChartι ⋯ σ) (Φ.subfanAnalyticMap hΦ S hS hface) = CategoryTheory.CategoryStruct.comp (TopCat.isoOfHomeo (Φ.subfanAnalyticChartMap S hS hface σ)).hom (Φ.analyticAffineChartι hΦ ⟨↑σ, ⋯⟩)

      On the chart of a cone of a subfan, the subfan map is the chart comparison followed by the inclusion of the chart of the same cone in the ambient realization.

      source
      theorem TauCeti.Toric.Fan.analyticAffineChartι_comp_subfanAnalyticMap_assoc {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) (σ : ↑(Φ.subfan S hS hface).cones) {Z : TopCat} (h : Φ.analyticRealization hΦ ⟶ Z) :
      CategoryTheory.CategoryStruct.comp ((Φ.subfan S hS hface).analyticAffineChartι ⋯ σ) (CategoryTheory.CategoryStruct.comp (Φ.subfanAnalyticMap hΦ S hS hface) h) = CategoryTheory.CategoryStruct.comp (TopCat.isoOfHomeo (Φ.subfanAnalyticChartMap S hS hface σ)).hom (CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartι hΦ ⟨↑σ, ⋯⟩) h)

      On the chart of a cone of a subfan, the subfan map is the chart comparison followed by the inclusion of the chart of the same cone in the ambient realization.

      source
      @[simp]
      theorem TauCeti.Toric.Fan.subfanAnalyticMap_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) (σ : ↑(Φ.subfan S hS hface).cones) (x : ↑((Φ.subfan S hS hface).analyticAffineChartDiagram.obj σ)) :
      (CategoryTheory.ConcreteCategory.hom (Φ.subfanAnalyticMap hΦ S hS hface)) ((CategoryTheory.ConcreteCategory.hom ((Φ.subfan S hS hface).analyticAffineChartι ⋯ σ)) x) = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ ⟨↑σ, ⋯⟩)) ((Φ.subfanAnalyticChartMap S hS hface σ) x)

      On a point of the chart of a cone of a subfan, the subfan map is the inclusion of the same complex point in the chart of that cone in the ambient realization.

      source
      theorem TauCeti.Toric.Fan.subfanAnalyticMap_injective {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) :
      Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.subfanAnalyticMap hΦ S hS hface))

      The subfan map is injective.

      source
      theorem TauCeti.Toric.Fan.range_subfanAnalyticMap {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) :
      Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Φ.subfanAnalyticMap hΦ S hS hface)) = ⋃ (σ : ↑(Φ.subfan S hS hface).cones), Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ ⟨↑σ, ⋯⟩))

      The image of the subfan map is the union of the ambient charts of the cones of the subfan.

      source
      theorem TauCeti.Toric.Fan.isOpenMap_subfanAnalyticMap {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) :
      IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom (Φ.subfanAnalyticMap hΦ S hS hface))

      The subfan map is an open map.

      source
      theorem TauCeti.Toric.Fan.isOpenEmbedding_subfanAnalyticMap {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) :
      Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (Φ.subfanAnalyticMap hΦ S hS hface))

      The map from the analytic realization of a subfan to the ambient analytic realization is an open embedding.