The liquid tensor product of disc algebras (Theorem 4.1)

Disproved

CondC.disc_tensor

by Lucas · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

disc-algebrasliquid-tensor-productuniversal-properties

Theorem 4.1 of the paper: for each 0 < p at most 1, the space O(D) is p-liquid and flat for the p-liquid tensor product, and the k-fold p-liquid tensor product of O(D) identifies with O(D^k), the polydisc algebra. The milestone isolates the universal-property content: given a bilinear combination of two polydisc-algebra spaces into a target T whose coefficients factor as the products of the coefficients of its two arguments - the coefficient-side expression of O(D) tensor O(D) = O(D^2) - the target T is p-liquid, and every liquid bilinear map factors uniquely through the combination. The liquid bilinear maps are those carrying designated null sequences to designated null sequences in each variable.

Formalization Note The liquid tensor product is an infinity-categorical construction in the paper and is replaced here by this universal property over the liquid interface; the flatness half of Theorem 4.1 is not part of the statement and is carried in prose.

Preamble

import Mathlib
import Definitions.Def_CondC_liq
import Definitions.Def_CondC_geo

Formal statement

namespace CondC

/-!  Milestone 2: the liquid tensor product of disc algebras. If the
coefficients of a bilinear combination conv factor as the products of the
coefficients of its two arguments, then the target carries a p-liquid
structure, and every liquid bilinear map factors uniquely through conv.
This is the universal-property content of Theorem 4.1: the k-fold liquid
tensor product of the disc algebra is the polydisc algebra.  -/
theorem disc_tensor : ∀ (p r : ℝ), 0 < p → p ≤ 1 → 0 < r →
    ∀ (V W T U : Type) [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
      [AddCommGroup T] [Module ℂ T] [AddCommGroup U] [Module ℂ U],
      ∀ (dV : DiscAlgebraData2 r V) (dW : DiscAlgebraData2 r W)
        (dT : DiscAlgebraData2 r T),
      ∀ (lV : PLiquidStructure p V) (lW : PLiquidStructure p W)
        (lU : PLiquidStructure p U),
      ∀ (conv : V →ₗ[ℂ] W →ₗ[ℂ] T),
      (∀ (v : V) (w : W) (i j : ℕ),
        dT.coeffs (conv v w) (i, j) = dV.coeffs v i * dW.coeffs w j) →
      IsPLiquid p T ∧
      ∀ b : V →ₗ[ℂ] W →ₗ[ℂ] U, LiquidBilinear p V W U lV lW lU b →
        ∃! L : T →ₗ[ℂ] U, ∀ (v : V) (w : W), L (conv v w) = b v w := by sorry

end CondC

Source

D. Clausen, P. Scholze, Condensed Mathematics and Complex Geometry, lecture notes (May 2026 version), Lecture IV (Theorem 4.1).

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: for 0 < p at most 1 and 0 < r, if the coefficients of a bilinear combination of two polydisc-algebra spaces into a target T factor as the products of the coefficients of its two arguments, then T is p-liquid, and every bilinear map from the two spaces that carries designated null sequences to designated null sequences in each argument factors uniquely through the combination. No other hypotheses appear.

View graph