Sato hyperfunctions and analytic generalized functions

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremSupport truncation#

If the local cohomology sheaves 𝓗_S^q(F) vanish for all q < n, then the cohomology groups H_S^q(W, F) with supports in S vanish for all q < n and every open W.

CategoryTheory.Sheaf.subsingleton_supportedH_of_isZero_supportedHSheaf.{u} {X : TopCat}
  (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat)
  (S : TopologicalSpace.Closeds ↑X) {n : β„•}
  (h : βˆ€ q < n, CategoryTheory.Limits.IsZero (F.supportedHSheaf S q)) {q : β„•} (hq : q < n)
  (W : TopologicalSpace.Opens ↑X) : Subsingleton (F.supportedH S W q)
Lean

Formalized in Tau Ceti as CategoryTheory.Sheaf.subsingleton_supportedH_of_isZero_supportedHSheaf.

Sources
LeanCategoryTheory.Sheaf.subsingleton_supportedH_of_isZero_supportedHSheaf
Uses 2
Statement usesCategoryTheory.Sheaf.supportedH Β· CategoryTheory.Sheaf.supportedHSheaf

TheoremTopCat.Sheaf.map_surjective_of_locally_flasque#

If every restriction map of a sheaf inside some neighbourhood of each point is surjective, then every restriction map is surjective.

TopCat.Sheaf.map_surjective_of_locally_flasque.{u, v_1, u_1, u_2, u_3} {X : TopCat} {C : Type u_1}
  [CategoryTheory.Category.{v_1, u_1} C] {FC : C β†’ C β†’ Type u_2} {CC : C β†’ Type u_3}
  [(X Y : C) β†’ FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{u, u, v_1, u_3, u_1, u_3 + 1}
      (CategoryTheory.forget C)]
  (F : TopCat.Sheaf C X)
  (h :
    βˆ€ (x : ↑X),
      βˆƒ W,
        x ∈ W ∧
          βˆ€ ⦃U V : TopologicalSpace.Opens ↑X⦄ (hUV : U ≀ V),
            V ≀ W β†’
              Function.Surjective
                ⇑(CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE hUV).op)))
  {U V : TopologicalSpace.Opens ↑X} (hUV : U ≀ V) :
  Function.Surjective
    ⇑(CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE hUV).op))
Lean

Formalized in Tau Ceti as TopCat.Sheaf.map_surjective_of_locally_flasque.

Sources
LeanTopCat.Sheaf.map_surjective_of_locally_flasque

DefinitionCategoryTheory.Sheaf.supportedHExcisionEquiv#

Excision for cohomology with supports: if W' ≀ W and S ∩ W βŠ† W' (that is, W ≀ W' βŠ” (X βˆ– S)), restriction is an isomorphism H_Sⁿ(W, F) ≃+ H_Sⁿ(W', F).

CategoryTheory.Sheaf.supportedHExcisionEquiv.{u} {X : TopCat}
  (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat)
  (S : TopologicalSpace.Closeds ↑X) {W' W : TopologicalSpace.Opens ↑X} (h : W' ≀ W)
  (hW : W ≀ W' βŠ” S.compl) (n : β„•) : F.supportedH S W n ≃+ F.supportedH S W' n
Lean

Formalized in Tau Ceti as CategoryTheory.Sheaf.supportedHExcisionEquiv.

Sources
LeanCategoryTheory.Sheaf.supportedHExcisionEquiv
Uses 1
Statement usesCategoryTheory.Sheaf.supportedH

TheoremIsCompact.isPolynomiallyConvex_of_forall_im_eq_zero#

Every compact subset of the real locus ℝⁿ βŠ† ℂⁿ is polynomially convex.

IsCompact.isPolynomiallyConvex_of_forall_im_eq_zero.{u_1} {ΞΉ : Type u_1} {K : Set (ΞΉ β†’ β„‚)}
  [Finite ΞΉ] (hK : IsCompact K) (hreal : βˆ€ w ∈ K, βˆ€ (i : ΞΉ), (w i).im = 0) :
  TauCeti.IsPolynomiallyConvex K
Lean

Formalized in Tau Ceti as IsCompact.isPolynomiallyConvex_of_forall_im_eq_zero.

Sources
LeanIsCompact.isPolynomiallyConvex_of_forall_im_eq_zero

TheoremTauCeti.IsPolynomiallyConvex.exists_subset_interior_polynomialPolyhedron#

A compact polynomially convex set K βŠ† ℂⁿ lies in the interior of a polynomial polyhedron contained in any given open neighbourhood U of K.

TauCeti.IsPolynomiallyConvex.exists_subset_interior_polynomialPolyhedron.{u_1} {ΞΉ : Type u_1}
  {K : Set (ΞΉ β†’ β„‚)} [Fintype ΞΉ] (hKc : TauCeti.IsPolynomiallyConvex K) (hK : IsCompact K)
  {U : Set (ΞΉ β†’ β„‚)} (hU : IsOpen U) (hKU : K βŠ† U) :
  βˆƒ R s,
    0 < R ∧ K βŠ† interior (TauCeti.polynomialPolyhedron R s) ∧ TauCeti.polynomialPolyhedron R s βŠ† U
Lean

Formalized in Tau Ceti as TauCeti.IsPolynomiallyConvex.exists_subset_interior_polynomialPolyhedron.

Sources
LeanTauCeti.IsPolynomiallyConvex.exists_subset_interior_polynomialPolyhedron

TheoremThe presheaf of one-dimensional hyperfunctions is separated#

a section that vanishes on the members of an open cover vanishes.

TauCeti.Hyperfunction.oneDimBoundaryPresheaf_isSeparated :
  CategoryTheory.Presheaf.IsSeparated (Opens.grothendieckTopology ↑↧ℝ)
    TauCeti.Hyperfunction.oneDimBoundaryPresheaf
Lean

Formalized in Tau Ceti as TauCeti.Hyperfunction.oneDimBoundaryPresheaf_isSeparated.

Sources
LeanTauCeti.Hyperfunction.oneDimBoundaryPresheaf_isSeparated
Uses 1
Statement usesTauCeti.Hyperfunction.OneDimBoundaryQuotient

AbbreviationCategoryTheory.Sheaf.supportedH#

The cohomology H_Sⁿ(W, F) of F on W with supports in the closed subset S: the relative cohomology of the inclusion W βˆ– S ⟢ W.

CategoryTheory.Sheaf.supportedH.{u} {X : TopCat}
  (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat)
  (S : TopologicalSpace.Closeds ↑X) (W : TopologicalSpace.Opens ↑X) (n : β„•) : Type u
Lean

Formalized in Tau Ceti as CategoryTheory.Sheaf.supportedH.

Sources
LeanCategoryTheory.Sheaf.supportedH
Used by 3
Used byCategoryTheory.Sheaf.supportedHExcisionEquiv Β· CategoryTheory.Sheaf.supportedHSheaf Β· Support truncation

AbbreviationCategoryTheory.Sheaf.supportedHSheaf#

The local cohomology sheaf 𝓗_Sⁿ(F) of F with supports in the closed subset S: the sheafification of the presheaf W ↦ H_Sⁿ(W, F) of cohomology with supports in S.

CategoryTheory.Sheaf.supportedHSheaf.{u} {X : TopCat}
  (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat)
  (S : TopologicalSpace.Closeds ↑X) (n : β„•) :
  CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat
Lean

Formalized in Tau Ceti as CategoryTheory.Sheaf.supportedHSheaf.

Sources
LeanCategoryTheory.Sheaf.supportedHSheaf
Uses 1 Β· Used by 1
Statement usesCategoryTheory.Sheaf.supportedH
Used bySupport truncation

AbbreviationTauCeti.Hyperfunction.OneDimBoundaryQuotient#

The space O(β„‚ βˆ– ℝ) / O(W(U)) of one-dimensional hyperfunctions on an open set U βŠ† ℝ, represented by holomorphic functions on β„‚ βˆ– ℝ modulo those extending holomorphically across U.

TauCeti.Hyperfunction.OneDimBoundaryQuotient (U : TopologicalSpace.Opens ℝ) : Type
Lean

Formalized in Tau Ceti as TauCeti.Hyperfunction.OneDimBoundaryQuotient.

Sources
LeanTauCeti.Hyperfunction.OneDimBoundaryQuotient
Used by 1
Used byThe presheaf of one-dimensional hyperfunctions is separated

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.