From a45ffeca9676a90c67d7e4758a38d736df32b7a6 Mon Sep 17 00:00:00 2001
From: Pieter Belmans <pieterbelmans@gmail.com>
Date: Tue, 1 Sep 2026 13:27:25 +0200
Subject: [PATCH 01/10] =?UTF-8?q?feat:=20recognize=20K=C3=BCnneth=20bundle?=
 =?UTF-8?q?=20products?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 docs/src/api/zero_loci.md |  16 ++
 src/ZeroLoci.jl           |   4 +-
 src/ZeroLocusBundles.jl   | 379 ++++++++++++++++++++++++++++++++++++++
 test/runtests.jl          |  27 +++
 4 files changed, 425 insertions(+), 1 deletion(-)

diff --git a/docs/src/api/zero_loci.md b/docs/src/api/zero_loci.md
index 2de51f3..1b2cab6 100644
--- a/docs/src/api/zero_loci.md
+++ b/docs/src/api/zero_loci.md
@@ -120,6 +120,22 @@ Exterior and symmetric powers use the derived graded-power formula, so they
 also work for arbitrary composite presentations rather than only for the
 tangent and cotangent sequences.
 
+Before invoking the generic long-exact-sequence solver, `cohomology` checks
+whether the formal locus splits and whether the current presentation is a
+direct sum of external tensor products. If so, and the factor cohomology is
+determined, it applies the Künneth formula. This is structural recognition:
+the optimization also applies when the locus and bundle merely have the
+factorable form, regardless of whether `product` or an `external_*` constructor
+created them. Ambiguous or nonfactorable presentations safely use the generic
+solver.
+
+Equality of zero-locus bundles is structural: it compares the formal locus and
+the multiset of ambient summands in every presentation degree. It does not try
+to prove that two presentations describe isomorphic bundles. `iszero(F)` is
+instead semantic at the vector-bundle level and tests the resulting rank.
+Thus a nonempty rank-zero presentation can satisfy `iszero(F)` without being
+equal to `zero_bundle(variety(F))`.
+
 !!! note "Generic bundle cohomology versus the Hodge engine"
     `cohomology(exterior_power(cotangent_bundle(Z), p))` evaluates that one
     bundle from its presentation. `hodge_numbers(Z)` uses the same conormal
diff --git a/src/ZeroLoci.jl b/src/ZeroLoci.jl
index 74d1aee..d444c20 100644
--- a/src/ZeroLoci.jl
+++ b/src/ZeroLoci.jl
@@ -189,7 +189,9 @@ latter disconnects `Z` into `m` copies); a single reduced point is a Künneth
 identity and is dropped. `n_factors` counts the kept factors.
 
 `hodge_numbers`, `hochschild_cohomology`, and cohomology of the tangent bundle
-recombine the factors by the Künneth formula, which determines
+recombine the factors by the Künneth formula. Cohomology of any bundle whose
+ambient presentation is structurally recognized as a direct sum of external
+tensor products does the same. This determines
 diamonds/parallelograms the monolithic long-exact-sequence solver leaves
 symbolic. (The remaining invariants — `euler_characteristic`,
 `hilbert_polynomial`, the anticanonical degree — are already exact for a
diff --git a/src/ZeroLocusBundles.jl b/src/ZeroLocusBundles.jl
index c933d41..f9e0980 100644
--- a/src/ZeroLocusBundles.jl
+++ b/src/ZeroLocusBundles.jl
@@ -595,6 +595,375 @@ function _presentation_term_cohomology(
   )
 end
 
+# ═══════════════════════════════════════════════════════════════════════════
+#  Structural Künneth recognition
+# ═══════════════════════════════════════════════════════════════════════════
+
+function _split_product_irrep(
+  representation::IrrepLevi,
+  left_ambient::PartialFlagVariety,
+  right_ambient::PartialFlagVariety,
+)
+  coefficients_product = collect(Int, coefficients(p_dominant_weight(representation)))
+  left_rank = rank(dynkin_type(left_ambient))
+  right_rank = rank(dynkin_type(right_ambient))
+  length(coefficients_product) == left_rank + right_rank || return nothing
+
+  left_weight = WeightLatticeElem(
+    dynkin_type(left_ambient), coefficients_product[1:left_rank]
+  )
+  right_weight = WeightLatticeElem(
+    dynkin_type(right_ambient), coefficients_product[(left_rank + 1):end]
+  )
+  (
+    IrrepLevi(marked_dynkin_type(left_ambient), left_weight),
+    IrrepLevi(marked_dynkin_type(right_ambient), right_weight),
+  )
+end
+
+function _add_bipartite_edge!(edges, left, right, degree::Int, multiplicity::Int=1)
+  degrees = get!(edges, (left, right), Dict{Int,Int}())
+  degrees[degree] = get(degrees, degree, 0) + multiplicity
+  edges
+end
+
+function _bipartite_components(edges)
+  remaining = Set(keys(edges))
+  components = Vector{typeof(edges)}()
+  while !isempty(remaining)
+    seed = first(remaining)
+    edge_type = keytype(edges)
+    left_vertices = Set{fieldtype(edge_type, 1)}([seed[1]])
+    right_vertices = Set{fieldtype(edge_type, 2)}([seed[2]])
+    component_keys = Set{edge_type}()
+
+    changed = true
+    while changed
+      changed = false
+      for edge in remaining
+        if edge[1] in left_vertices || edge[2] in right_vertices
+          push!(component_keys, edge)
+          push!(left_vertices, edge[1])
+          push!(right_vertices, edge[2])
+          changed = true
+        end
+      end
+      setdiff!(remaining, component_keys)
+    end
+
+    push!(components, typeof(edges)(edge => edges[edge] for edge in component_keys))
+  end
+  components
+end
+
+"""
+Factor one connected bipartite multiset whose edge labels are additive degrees.
+
+For an external tensor product, an edge `(left, right)` has degree
+`left_degree + right_degree` and multiplicity
+`left_multiplicity * right_multiplicity`. The complete bipartite and rank-one
+checks make this a recognition routine: failure returns `nothing` rather than
+guessing a decomposition.
+"""
+function _rank_one_bipartite_factor(edges)
+  isempty(edges) && return nothing
+  all(length(degrees) == 1 for degrees in values(edges)) || return nothing
+
+  left_vertices = unique(first(edge) for edge in keys(edges))
+  right_vertices = unique(last(edge) for edge in keys(edges))
+  length(edges) == length(left_vertices) * length(right_vertices) || return nothing
+
+  edge_degree(left, right) = only(keys(edges[(left, right)]))
+  edge_multiplicity(left, right) = only(values(edges[(left, right)]))
+
+  left_anchor = first(left_vertices)
+  right_anchor = first(right_vertices)
+  left_degrees = Dict(left_anchor => 0)
+  right_degrees = Dict(
+    right => edge_degree(left_anchor, right) for right in right_vertices
+  )
+  for left in left_vertices
+    left_degrees[left] =
+      edge_degree(left, right_anchor) - right_degrees[right_anchor]
+  end
+
+  left_anchor_multiplicity = gcd(
+    (edge_multiplicity(left_anchor, right) for right in right_vertices)...
+  )
+  right_multiplicities = Dict(
+    right => edge_multiplicity(left_anchor, right) ÷ left_anchor_multiplicity for
+    right in right_vertices
+  )
+  left_multiplicities = Dict{eltype(left_vertices),Int}()
+  for left in left_vertices
+    right_multiplicity = right_multiplicities[right_anchor]
+    edge_multiplicity(left, right_anchor) % right_multiplicity == 0 || return nothing
+    left_multiplicities[left] =
+      edge_multiplicity(left, right_anchor) ÷ right_multiplicity
+  end
+
+  for left in left_vertices, right in right_vertices
+    haskey(edges, (left, right)) || return nothing
+    edge_degree(left, right) == left_degrees[left] + right_degrees[right] ||
+      return nothing
+    expected_multiplicity = left_multiplicities[left] * right_multiplicities[right]
+    edge_multiplicity(left, right) == expected_multiplicity || return nothing
+  end
+
+  (
+    Dict(
+      left => (left_degrees[left], left_multiplicities[left]) for
+      left in left_vertices
+    ),
+    Dict(
+      right => (right_degrees[right], right_multiplicities[right]) for
+      right in right_vertices
+    ),
+  )
+end
+
+function _filtered_bundle_from_factor_data(ambient::PartialFlagVariety, data)
+  pieces = Dict{Int,Vector{IrrepLevi}}()
+  for (representation, (degree, multiplicity)) in data
+    append!(get!(pieces, degree, IrrepLevi[]), fill(representation, multiplicity))
+  end
+  ordered_pieces = CompletelyReducibleBundle[
+    CompletelyReducibleBundle(ambient, pieces[degree]) for
+    degree in sort!(collect(keys(pieces)))
+  ]
+  FilteredBundle(ambient, ordered_pieces)
+end
+
+function _factor_filtered_bundle_on_product(
+  bundle::FilteredBundle,
+  left_ambient::PartialFlagVariety,
+  right_ambient::PartialFlagVariety,
+)
+  edges = Dict{Tuple{IrrepLevi,IrrepLevi},Dict{Int,Int}}()
+  for (degree, piece) in enumerate(graded_pieces(bundle))
+    for representation in components(piece)
+      split = _split_product_irrep(representation, left_ambient, right_ambient)
+      split === nothing && return nothing
+      _add_bipartite_edge!(edges, split[1], split[2], degree)
+    end
+  end
+  factorization = _rank_one_bipartite_factor(edges)
+  factorization === nothing && return nothing
+  left_data, right_data = factorization
+
+  left_filtered = _filtered_bundle_from_factor_data(left_ambient, left_data)
+  right_filtered = _filtered_bundle_from_factor_data(right_ambient, right_data)
+  left_options = if n_filtration_steps(left_filtered) == 1
+    _AmbientBundle[total_bundle(left_filtered), left_filtered]
+  else
+    _AmbientBundle[left_filtered]
+  end
+  right_options = if n_filtration_steps(right_filtered) == 1
+    _AmbientBundle[total_bundle(right_filtered), right_filtered]
+  else
+    _AmbientBundle[right_filtered]
+  end
+
+  for left in left_options, right in right_options
+    external_tensor_product(left, right) == bundle && return (left, right)
+  end
+  nothing
+end
+
+function _factor_ambient_bundle_on_product(
+  bundle::CompletelyReducibleBundle,
+  left_ambient::PartialFlagVariety,
+  right_ambient::PartialFlagVariety,
+)
+  result = Tuple{_AmbientBundle,_AmbientBundle}[]
+  for representation in components(bundle)
+    split = _split_product_irrep(representation, left_ambient, right_ambient)
+    split === nothing && return nothing
+    push!(
+      result,
+      (
+        CompletelyReducibleBundle(left_ambient, IrrepLevi[split[1]]),
+        CompletelyReducibleBundle(right_ambient, IrrepLevi[split[2]]),
+      ),
+    )
+  end
+  result
+end
+
+function _factor_ambient_bundle_on_product(
+  bundle::FilteredBundle,
+  left_ambient::PartialFlagVariety,
+  right_ambient::PartialFlagVariety,
+)
+  n_filtration_steps(bundle) == 1 && return _factor_ambient_bundle_on_product(
+    total_bundle(bundle), left_ambient, right_ambient
+  )
+  factorization = _factor_filtered_bundle_on_product(bundle, left_ambient, right_ambient)
+  factorization === nothing ? nothing : [factorization]
+end
+
+function _product_of_zero_loci(product_factors)
+  length(product_factors) == 1 && return only(product_factors)
+  product(product_factors[1], product_factors[2], product_factors[3:end]...)
+end
+
+function _product_bipartitions(Z::ZeroLocus)
+  product_factors = factors(Z)
+  result = Tuple{ZeroLocus,ZeroLocus}[]
+  for split_index in 1:(length(product_factors) - 1)
+    left = _product_of_zero_loci(product_factors[1:split_index])
+    right = _product_of_zero_loci(product_factors[(split_index + 1):end])
+    product(left, right) == Z && push!(result, (left, right))
+  end
+  result
+end
+
+function _presentation_from_factor_data(
+  locus::ZeroLocus, data, degree_shift::Int
+)
+  terms = Dict{Int,Vector{_AmbientBundle}}()
+  for (bundle, (degree, multiplicity)) in data
+    append!(
+      get!(terms, degree + degree_shift, _AmbientBundle[]),
+      fill(bundle, multiplicity),
+    )
+  end
+  ZeroLocusBundle(locus, _AmbientBundlePresentation(terms))
+end
+
+function _factor_data_rank(data, degree_shift::Int)
+  sum(
+    (isodd(degree + degree_shift) ? -1 : 1) * multiplicity * rank(bundle) for
+    (bundle, (degree, multiplicity)) in data;
+    init=0,
+  )
+end
+
+function _factor_presentation_component(
+  edges, left_locus::ZeroLocus, right_locus::ZeroLocus
+)
+  factorization = _rank_one_bipartite_factor(edges)
+  factorization === nothing && return nothing
+  left_data, right_data = factorization
+
+  shifts = intersect(
+    Set(-degree for (_, (degree, _)) in left_data),
+    Set(degree for (_, (degree, _)) in right_data),
+  )
+  candidates = Tuple{ZeroLocusBundle,ZeroLocusBundle}[]
+  component_rank = sum(
+    (isodd(degree) ? -1 : 1) * multiplicity * rank(left) * rank(right) for
+    ((left, right), degrees) in edges for
+    (degree, multiplicity) in degrees;
+    init=0,
+  )
+
+  for shift in shifts
+    left_rank = _factor_data_rank(left_data, shift)
+    right_rank = _factor_data_rank(right_data, -shift)
+    left_rank > 0 && right_rank > 0 || continue
+    left_rank * right_rank == component_rank || continue
+
+    left = _presentation_from_factor_data(left_locus, left_data, shift)
+    right = _presentation_from_factor_data(right_locus, right_data, -shift)
+    push!(candidates, (left, right))
+  end
+  length(candidates) == 1 ? only(candidates) : nothing
+end
+
+function _degree_zero_kunneth_decomposition(
+  F::ZeroLocusBundle, left_locus::ZeroLocus, right_locus::ZeroLocus
+)
+  terms = F.presentation.terms
+  length(terms) == 1 && haskey(terms, 0) || return nothing
+
+  left_ambient = ambient_variety(left_locus)
+  right_ambient = ambient_variety(right_locus)
+  decomposition = Tuple{ZeroLocusBundle,ZeroLocusBundle}[]
+  for summand in terms[0]
+    factorizations = _factor_ambient_bundle_on_product(
+      summand, left_ambient, right_ambient
+    )
+    factorizations === nothing && return nothing
+    for (left, right) in factorizations
+      push!(decomposition, (restrict(left_locus, left), restrict(right_locus, right)))
+    end
+  end
+  decomposition
+end
+
+"""
+Recognize a presentation as a direct sum of external tensor products.
+
+The recognition depends only on the current locus and presentation. It first
+finds a product decomposition of the formal zero locus, then checks complete
+bipartite rank-one conditions on the ambient presentation. Ambiguous or
+nonfactorable presentations return `nothing` and use the generic LES backend.
+"""
+function _kunneth_decomposition(
+  F::ZeroLocusBundle, left_locus::ZeroLocus, right_locus::ZeroLocus
+)
+  degree_zero_decomposition = _degree_zero_kunneth_decomposition(F, left_locus, right_locus)
+  degree_zero_decomposition === nothing || return degree_zero_decomposition
+
+  left_ambient = ambient_variety(left_locus)
+  right_ambient = ambient_variety(right_locus)
+
+  edges = Dict{Tuple{_AmbientBundle,_AmbientBundle},Dict{Int,Int}}()
+  for (degree, summands) in F.presentation.terms
+    for summand in summands
+      factorizations = _factor_ambient_bundle_on_product(
+        summand, left_ambient, right_ambient
+      )
+      factorizations === nothing && return nothing
+      for (left, right) in factorizations
+        _add_bipartite_edge!(edges, left, right, degree)
+      end
+    end
+  end
+  isempty(edges) && return nothing
+
+  decomposition = Tuple{ZeroLocusBundle,ZeroLocusBundle}[]
+  for component in _bipartite_components(edges)
+    factorization = _factor_presentation_component(
+      component, left_locus, right_locus
+    )
+    factorization === nothing && return nothing
+    push!(decomposition, factorization)
+  end
+  sum(pair -> rank(pair[1]) * rank(pair[2]), decomposition; init=0) == rank(F) ||
+    return nothing
+  decomposition
+end
+
+function _kunneth_decomposition(F::ZeroLocusBundle)
+  for (left_locus, right_locus) in _product_bipartitions(variety(F))
+    decomposition = _kunneth_decomposition(F, left_locus, right_locus)
+    decomposition === nothing || return decomposition
+  end
+  nothing
+end
+
+function _kunneth_cohomology(F::ZeroLocusBundle)
+  decomposition = _kunneth_decomposition(F)
+  decomposition === nothing && return nothing
+
+  d = dimension(variety(F))
+  entries = zeros(BigInt, d + 1)
+  for (left, right) in decomposition
+    left_cohomology = cohomology(left)
+    right_cohomology = cohomology(right)
+    is_determined(left_cohomology) && is_determined(right_cohomology) || return nothing
+    for left_degree in 0:left_cohomology.max_degree
+      for right_degree in 0:right_cohomology.max_degree
+        entries[left_degree + right_degree + 1] +=
+          left_cohomology[left_degree].constant * right_cohomology[right_degree].constant
+      end
+    end
+  end
+  Cohomology{AffineExpr}(AffineExpr.(entries), d)
+end
+
 """
 Compute cohomology from a complex which is exact away from degree zero.
 
@@ -642,6 +1011,13 @@ Compute dimension-valued sheaf cohomology from the ambient presentation.
 Entries are exact integers where exactness and the available geometric
 constraints determine them, and symbolic affine expressions otherwise.
 
+When the formal zero locus splits as a product and the presentation is
+structurally a direct sum of external tensor products, this method first tries
+the Künneth formula. Recognition uses the current locus and presentation, not
+the constructors that produced them. If no unambiguous factorization is found,
+or factor cohomology remains symbolic, computation falls back to the generic
+long-exact-sequence backend.
+
 Character-valued cohomology is not defined: a section cutting out a zero locus
 is generally not invariant under the ambient group.
 """
@@ -650,6 +1026,9 @@ function cohomology(F::ZeroLocusBundle)
   d = dimension(Z)
   is_tangent = F == tangent_bundle(Z)
 
+  kunneth_cohomology = _kunneth_cohomology(F)
+  kunneth_cohomology === nothing || return kunneth_cohomology
+
   if is_tangent && n_factors(Z) >= 2
     tangent_row = AffineExpr[hochschild_cohomology(Z)[1, q] for q in 0:d]
     all(is_determined, tangent_row) && return Cohomology{AffineExpr}(tangent_row, d)
diff --git a/test/runtests.jl b/test/runtests.jl
index 26316ca..7076e07 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -2298,6 +2298,33 @@ mdt(::Type{DT}, marked) where {DT<:DynkinType} = MarkedDynkinType(DT, marked)
     @test euler_characteristic(tangent_sum) ==
       euler_characteristic(TZ) * euler_characteristic(structure_sheaf(W)) +
           euler_characteristic(structure_sheaf(Z)) * euler_characteristic(TW)
+
+    quartic_ambient = projective_space(3)
+    quartic = zero_locus(line_bundle(quartic_ambient, 4))
+    tangent_quartic = tangent_bundle(quartic)
+    tangent_box_square = external_tensor_product(tangent_quartic, tangent_quartic)
+    tangent_box_sum = external_direct_sum(tangent_quartic, tangent_quartic)
+    @test cohomology(tangent_box_square).entries == AffineExpr.([0, 0, 400, 0, 0])
+    @test cohomology(tangent_box_sum).entries == AffineExpr.([0, 40, 0, 40, 0])
+
+    product_ambient = product(quartic_ambient, quartic_ambient)
+    manual_locus = zero_locus(
+      direct_sum(
+        line_bundle(product_ambient, [4, 0]),
+        line_bundle(product_ambient, [0, 4]),
+      ),
+    )
+    manual_ambient_bundle = direct_sum(
+      direct_sum(
+        structure_sheaf(product_ambient),
+        line_bundle(product_ambient, [1, 0]),
+      ),
+      line_bundle(product_ambient, [0, 1]),
+    )
+    manual_bundle = restrict(manual_locus, manual_ambient_bundle)
+    @test manual_locus == product(quartic, quartic)
+    @test length(PartialFlagVarieties._kunneth_decomposition(manual_bundle)) == 3
+    @test cohomology(manual_bundle).entries == AffineExpr.([9, 0, 10, 0, 1])
   end
 
   # The zero locus of a section of O(1) on the Cayley plane OP² = E6/P1

From c1e6f5564a1d0e4604a237b746210b36042cc2dd Mon Sep 17 00:00:00 2001
From: Pieter Belmans <pieterbelmans@gmail.com>
Date: Tue, 1 Sep 2026 14:35:32 +0200
Subject: [PATCH 02/10] =?UTF-8?q?fix:=20preserve=20K=C3=BCnneth=20tangent?=
 =?UTF-8?q?=20recognition?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/ZeroLocusBundles.jl | 28 +++++++++++++++++-----------
 1 file changed, 17 insertions(+), 11 deletions(-)

diff --git a/src/ZeroLocusBundles.jl b/src/ZeroLocusBundles.jl
index f9e0980..c12524c 100644
--- a/src/ZeroLocusBundles.jl
+++ b/src/ZeroLocusBundles.jl
@@ -471,8 +471,15 @@ presentation is the normal sequence
 ``0 \\to \\mathrm{T}_Z \\to \\mathrm{T}_X|_Z \\to \\mathcal{E}|_Z \\to 0``.
 """
 function tangent_bundle(Z::ZeroLocus)
+  ambient_tangent = filtered_tangent_bundle(ambient_variety(Z))
+  tangent_term =
+    if n_filtration_steps(ambient_tangent) == 1
+      total_bundle(ambient_tangent)
+    else
+      ambient_tangent
+    end
   terms = Dict{Int,Vector{_AmbientBundle}}(
-    0 => _AmbientBundle[filtered_tangent_bundle(ambient_variety(Z))],
+    0 => _AmbientBundle[tangent_term],
     1 => _AmbientBundle[defining_bundle(Z)],
   )
   ZeroLocusBundle(Z, _AmbientBundlePresentation(terms))
@@ -1024,16 +1031,6 @@ is generally not invariant under the ambient group.
 function cohomology(F::ZeroLocusBundle)
   Z = variety(F)
   d = dimension(Z)
-  is_tangent = F == tangent_bundle(Z)
-
-  kunneth_cohomology = _kunneth_cohomology(F)
-  kunneth_cohomology === nothing || return kunneth_cohomology
-
-  if is_tangent && n_factors(Z) >= 2
-    tangent_row = AffineExpr[hochschild_cohomology(Z)[1, q] for q in 0:d]
-    all(is_determined, tangent_row) && return Cohomology{AffineExpr}(tangent_row, d)
-  end
-
   var_counter = Ref(0)
 
   # A degree-zero presentation is just a direct sum of restricted ambient
@@ -1044,6 +1041,15 @@ function cohomology(F::ZeroLocusBundle)
     return Cohomology{AffineExpr}(entries, d)
   end
 
+  is_tangent = F == tangent_bundle(Z)
+  if is_tangent && n_factors(Z) >= 2
+    tangent_row = AffineExpr[hochschild_cohomology(Z)[1, q] for q in 0:d]
+    all(is_determined, tangent_row) && return Cohomology{AffineExpr}(tangent_row, d)
+  end
+
+  kunneth_cohomology = _kunneth_cohomology(F)
+  kunneth_cohomology === nothing || return kunneth_cohomology
+
   entries, inequalities = _cohomology_from_presentation(F, var_counter)
   entry_count = length(entries)
   system = vcat(entries, inequalities)

From 030955f14017bad1856cde08bf3755616d3a5bb7 Mon Sep 17 00:00:00 2001
From: Pieter Belmans <pieterbelmans@gmail.com>
Date: Tue, 1 Sep 2026 14:35:42 +0200
Subject: [PATCH 03/10] =?UTF-8?q?docs:=20clarify=20K=C3=BCnneth=20recognit?=
 =?UTF-8?q?ion?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 docs/src/api/zero_loci.md | 9 +--------
 src/ZeroLocusBundles.jl   | 4 ++--
 2 files changed, 3 insertions(+), 10 deletions(-)

diff --git a/docs/src/api/zero_loci.md b/docs/src/api/zero_loci.md
index 1b2cab6..f97cbdf 100644
--- a/docs/src/api/zero_loci.md
+++ b/docs/src/api/zero_loci.md
@@ -121,7 +121,7 @@ also work for arbitrary composite presentations rather than only for the
 tangent and cotangent sequences.
 
 Before invoking the generic long-exact-sequence solver, `cohomology` checks
-whether the formal locus splits and whether the current presentation is a
+whether the zero locus splits and whether the current presentation is a
 direct sum of external tensor products. If so, and the factor cohomology is
 determined, it applies the Künneth formula. This is structural recognition:
 the optimization also applies when the locus and bundle merely have the
@@ -129,13 +129,6 @@ factorable form, regardless of whether `product` or an `external_*` constructor
 created them. Ambiguous or nonfactorable presentations safely use the generic
 solver.
 
-Equality of zero-locus bundles is structural: it compares the formal locus and
-the multiset of ambient summands in every presentation degree. It does not try
-to prove that two presentations describe isomorphic bundles. `iszero(F)` is
-instead semantic at the vector-bundle level and tests the resulting rank.
-Thus a nonempty rank-zero presentation can satisfy `iszero(F)` without being
-equal to `zero_bundle(variety(F))`.
-
 !!! note "Generic bundle cohomology versus the Hodge engine"
     `cohomology(exterior_power(cotangent_bundle(Z), p))` evaluates that one
     bundle from its presentation. `hodge_numbers(Z)` uses the same conormal
diff --git a/src/ZeroLocusBundles.jl b/src/ZeroLocusBundles.jl
index c12524c..8041ac0 100644
--- a/src/ZeroLocusBundles.jl
+++ b/src/ZeroLocusBundles.jl
@@ -903,7 +903,7 @@ end
 Recognize a presentation as a direct sum of external tensor products.
 
 The recognition depends only on the current locus and presentation. It first
-finds a product decomposition of the formal zero locus, then checks complete
+finds a product decomposition of the zero locus, then checks complete
 bipartite rank-one conditions on the ambient presentation. Ambiguous or
 nonfactorable presentations return `nothing` and use the generic LES backend.
 """
@@ -1018,7 +1018,7 @@ Compute dimension-valued sheaf cohomology from the ambient presentation.
 Entries are exact integers where exactness and the available geometric
 constraints determine them, and symbolic affine expressions otherwise.
 
-When the formal zero locus splits as a product and the presentation is
+When the zero locus splits as a product and the presentation is
 structurally a direct sum of external tensor products, this method first tries
 the Künneth formula. Recognition uses the current locus and presentation, not
 the constructors that produced them. If no unambiguous factorization is found,

From 59577d4f1daac4ee16542ad80210821a150e9a60 Mon Sep 17 00:00:00 2001
From: Pieter Belmans <pieterbelmans@gmail.com>
Date: Tue, 1 Sep 2026 15:15:27 +0200
Subject: [PATCH 04/10] =?UTF-8?q?refactor:=20streamline=20K=C3=BCnneth=20r?=
 =?UTF-8?q?ecognition?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/ZeroLocusBundles.jl | 366 ++++++++++++++++------------------------
 1 file changed, 145 insertions(+), 221 deletions(-)

diff --git a/src/ZeroLocusBundles.jl b/src/ZeroLocusBundles.jl
index 8041ac0..6725c60 100644
--- a/src/ZeroLocusBundles.jl
+++ b/src/ZeroLocusBundles.jl
@@ -472,14 +472,10 @@ presentation is the normal sequence
 """
 function tangent_bundle(Z::ZeroLocus)
   ambient_tangent = filtered_tangent_bundle(ambient_variety(Z))
-  tangent_term =
-    if n_filtration_steps(ambient_tangent) == 1
-      total_bundle(ambient_tangent)
-    else
-      ambient_tangent
-    end
+  n_filtration_steps(ambient_tangent) == 1 &&
+    (ambient_tangent = total_bundle(ambient_tangent))
   terms = Dict{Int,Vector{_AmbientBundle}}(
-    0 => _AmbientBundle[tangent_term],
+    0 => _AmbientBundle[ambient_tangent],
     1 => _AmbientBundle[defining_bundle(Z)],
   )
   ZeroLocusBundle(Z, _AmbientBundlePresentation(terms))
@@ -607,132 +603,112 @@ end
 # ═══════════════════════════════════════════════════════════════════════════
 
 function _split_product_irrep(
-  representation::IrrepLevi,
+  irrep::IrrepLevi,
   left_ambient::PartialFlagVariety,
   right_ambient::PartialFlagVariety,
 )
-  coefficients_product = collect(Int, coefficients(p_dominant_weight(representation)))
-  left_rank = rank(dynkin_type(left_ambient))
-  right_rank = rank(dynkin_type(right_ambient))
-  length(coefficients_product) == left_rank + right_rank || return nothing
-
-  left_weight = WeightLatticeElem(
-    dynkin_type(left_ambient), coefficients_product[1:left_rank]
-  )
-  right_weight = WeightLatticeElem(
-    dynkin_type(right_ambient), coefficients_product[(left_rank + 1):end]
-  )
+  coefficients = collect(Int, Semisimple.coefficients(p_dominant_weight(irrep)))
+  left_type = dynkin_type(left_ambient)
+  right_type = dynkin_type(right_ambient)
+  left_rank = rank(left_type)
+  right_rank = rank(right_type)
+  length(coefficients) == left_rank + right_rank || return nothing
+
+  left_weight = WeightLatticeElem(left_type, coefficients[1:left_rank])
+  right_weight = WeightLatticeElem(right_type, coefficients[(left_rank + 1):end])
   (
     IrrepLevi(marked_dynkin_type(left_ambient), left_weight),
     IrrepLevi(marked_dynkin_type(right_ambient), right_weight),
   )
 end
 
-function _add_bipartite_edge!(edges, left, right, degree::Int, multiplicity::Int=1)
-  degrees = get!(edges, (left, right), Dict{Int,Int}())
-  degrees[degree] = get(degrees, degree, 0) + multiplicity
-  edges
+# Product terms are stored as `(left, right) => (degree, multiplicity)`.
+function _add_product_term!(terms, left, right, degree::Int, multiplicity::Int=1)
+  key = (left, right)
+  if haskey(terms, key)
+    old_degree, old_multiplicity = terms[key]
+    old_degree == degree || return false
+    terms[key] = (degree, old_multiplicity + multiplicity)
+  else
+    terms[key] = (degree, multiplicity)
+  end
+  true
 end
 
-function _bipartite_components(edges)
-  remaining = Set(keys(edges))
-  components = Vector{typeof(edges)}()
-  while !isempty(remaining)
-    seed = first(remaining)
-    edge_type = keytype(edges)
-    left_vertices = Set{fieldtype(edge_type, 1)}([seed[1]])
-    right_vertices = Set{fieldtype(edge_type, 2)}([seed[2]])
-    component_keys = Set{edge_type}()
-
-    changed = true
-    while changed
-      changed = false
-      for edge in remaining
-        if edge[1] in left_vertices || edge[2] in right_vertices
-          push!(component_keys, edge)
-          push!(left_vertices, edge[1])
-          push!(right_vertices, edge[2])
-          changed = true
+# Partition pairs into candidate summands. Pairs are linked when they share a
+# left or right factor; the transitive closure gives the maximal groups.
+function _product_term_components(terms)
+  pending = Set(keys(terms))
+  components = Vector{typeof(terms)}()
+
+  while !isempty(pending)
+    seed = pop!(pending)
+    component = typeof(terms)(seed => terms[seed])
+    frontier = [seed]
+
+    while !isempty(frontier)
+      pair = pop!(frontier)
+      for candidate in collect(pending)
+        if first(candidate) == first(pair) || last(candidate) == last(pair)
+          delete!(pending, candidate)
+          component[candidate] = terms[candidate]
+          push!(frontier, candidate)
         end
       end
-      setdiff!(remaining, component_keys)
     end
-
-    push!(components, typeof(edges)(edge => edges[edge] for edge in component_keys))
+    push!(components, component)
   end
   components
 end
 
 """
-Factor one connected bipartite multiset whose edge labels are additive degrees.
-
-For an external tensor product, an edge `(left, right)` has degree
-`left_degree + right_degree` and multiplicity
-`left_multiplicity * right_multiplicity`. The complete bipartite and rank-one
-checks make this a recognition routine: failure returns `nothing` rather than
-guessing a decomposition.
+Recover two factors from a connected group of terms `(left, right) => (degree,
+multiplicity)`. An external tensor product has rectangular support, additive
+degrees, and multiplicative multiplicities. Degrees are normalized by setting
+the first left degree to zero; multiplicities by the gcd of the first row.
 """
-function _rank_one_bipartite_factor(edges)
-  isempty(edges) && return nothing
-  all(length(degrees) == 1 for degrees in values(edges)) || return nothing
-
-  left_vertices = unique(first(edge) for edge in keys(edges))
-  right_vertices = unique(last(edge) for edge in keys(edges))
-  length(edges) == length(left_vertices) * length(right_vertices) || return nothing
-
-  edge_degree(left, right) = only(keys(edges[(left, right)]))
-  edge_multiplicity(left, right) = only(values(edges[(left, right)]))
-
-  left_anchor = first(left_vertices)
-  right_anchor = first(right_vertices)
-  left_degrees = Dict(left_anchor => 0)
-  right_degrees = Dict(
-    right => edge_degree(left_anchor, right) for right in right_vertices
-  )
-  for left in left_vertices
-    left_degrees[left] =
-      edge_degree(left, right_anchor) - right_degrees[right_anchor]
-  end
+function _factor_product_terms(terms)
+  isempty(terms) && return nothing
+  lefts = unique(first(pair) for pair in keys(terms))
+  rights = unique(last(pair) for pair in keys(terms))
+  length(terms) == length(lefts) * length(rights) || return nothing
+
+  degree(left, right) = first(terms[(left, right)])
+  multiplicity(left, right) = last(terms[(left, right)])
 
-  left_anchor_multiplicity = gcd(
-    (edge_multiplicity(left_anchor, right) for right in right_vertices)...
+  left0, right0 = first(lefts), first(rights)
+  left0_multiplicity = gcd((multiplicity(left0, right) for right in rights)...)
+  right_data = Dict(
+    right => (
+      degree(left0, right),
+      multiplicity(left0, right) ÷ left0_multiplicity,
+    ) for right in rights
   )
-  right_multiplicities = Dict(
-    right => edge_multiplicity(left_anchor, right) ÷ left_anchor_multiplicity for
-    right in right_vertices
+  right0_multiplicity = last(right_data[right0])
+  all(multiplicity(left, right0) % right0_multiplicity == 0 for left in lefts) ||
+    return nothing
+  left_data = Dict(
+    left => (
+      degree(left, right0) - degree(left0, right0),
+      multiplicity(left, right0) ÷ right0_multiplicity,
+    ) for left in lefts
   )
-  left_multiplicities = Dict{eltype(left_vertices),Int}()
-  for left in left_vertices
-    right_multiplicity = right_multiplicities[right_anchor]
-    edge_multiplicity(left, right_anchor) % right_multiplicity == 0 || return nothing
-    left_multiplicities[left] =
-      edge_multiplicity(left, right_anchor) ÷ right_multiplicity
-  end
 
-  for left in left_vertices, right in right_vertices
-    haskey(edges, (left, right)) || return nothing
-    edge_degree(left, right) == left_degrees[left] + right_degrees[right] ||
-      return nothing
-    expected_multiplicity = left_multiplicities[left] * right_multiplicities[right]
-    edge_multiplicity(left, right) == expected_multiplicity || return nothing
+  for left in lefts, right in rights
+    left_degree, left_multiplicity = left_data[left]
+    right_degree, right_multiplicity = right_data[right]
+    terms[(left, right)] == (
+      left_degree + right_degree,
+      left_multiplicity * right_multiplicity,
+    ) || return nothing
   end
-
-  (
-    Dict(
-      left => (left_degrees[left], left_multiplicities[left]) for
-      left in left_vertices
-    ),
-    Dict(
-      right => (right_degrees[right], right_multiplicities[right]) for
-      right in right_vertices
-    ),
-  )
+  left_data, right_data
 end
 
 function _filtered_bundle_from_factor_data(ambient::PartialFlagVariety, data)
   pieces = Dict{Int,Vector{IrrepLevi}}()
-  for (representation, (degree, multiplicity)) in data
-    append!(get!(pieces, degree, IrrepLevi[]), fill(representation, multiplicity))
+  for (irrep, (degree, multiplicity)) in data
+    append!(get!(pieces, degree, IrrepLevi[]), fill(irrep, multiplicity))
   end
   ordered_pieces = CompletelyReducibleBundle[
     CompletelyReducibleBundle(ambient, pieces[degree]) for
@@ -746,35 +722,26 @@ function _factor_filtered_bundle_on_product(
   left_ambient::PartialFlagVariety,
   right_ambient::PartialFlagVariety,
 )
-  edges = Dict{Tuple{IrrepLevi,IrrepLevi},Dict{Int,Int}}()
+  terms = Dict{Tuple{IrrepLevi,IrrepLevi},Tuple{Int,Int}}()
   for (degree, piece) in enumerate(graded_pieces(bundle))
-    for representation in components(piece)
-      split = _split_product_irrep(representation, left_ambient, right_ambient)
+    for irrep in components(piece)
+      split = _split_product_irrep(irrep, left_ambient, right_ambient)
       split === nothing && return nothing
-      _add_bipartite_edge!(edges, split[1], split[2], degree)
+      _add_product_term!(terms, split[1], split[2], degree) || return nothing
     end
   end
-  factorization = _rank_one_bipartite_factor(edges)
-  factorization === nothing && return nothing
-  left_data, right_data = factorization
-
-  left_filtered = _filtered_bundle_from_factor_data(left_ambient, left_data)
-  right_filtered = _filtered_bundle_from_factor_data(right_ambient, right_data)
-  left_options = if n_filtration_steps(left_filtered) == 1
-    _AmbientBundle[total_bundle(left_filtered), left_filtered]
-  else
-    _AmbientBundle[left_filtered]
-  end
-  right_options = if n_filtration_steps(right_filtered) == 1
-    _AmbientBundle[total_bundle(right_filtered), right_filtered]
-  else
-    _AmbientBundle[right_filtered]
-  end
-
-  for left in left_options, right in right_options
-    external_tensor_product(left, right) == bundle && return (left, right)
-  end
-  nothing
+  factor_data = _factor_product_terms(terms)
+  factor_data === nothing && return nothing
+  left_data, right_data = factor_data
+
+  left = _filtered_bundle_from_factor_data(left_ambient, left_data)
+  right = _filtered_bundle_from_factor_data(right_ambient, right_data)
+  options(F) = n_filtration_steps(F) == 1 ? (total_bundle(F), F) : (F,)
+  matches = [
+    pair for pair in Iterators.product(options(left), options(right)) if
+    external_tensor_product(pair...) == bundle
+  ]
+  length(matches) == 1 ? only(matches) : nothing
 end
 
 function _factor_ambient_bundle_on_product(
@@ -783,14 +750,15 @@ function _factor_ambient_bundle_on_product(
   right_ambient::PartialFlagVariety,
 )
   result = Tuple{_AmbientBundle,_AmbientBundle}[]
-  for representation in components(bundle)
-    split = _split_product_irrep(representation, left_ambient, right_ambient)
+  for irrep in components(bundle)
+    split = _split_product_irrep(irrep, left_ambient, right_ambient)
     split === nothing && return nothing
+    left, right = split
     push!(
       result,
       (
-        CompletelyReducibleBundle(left_ambient, IrrepLevi[split[1]]),
-        CompletelyReducibleBundle(right_ambient, IrrepLevi[split[2]]),
+        CompletelyReducibleBundle(left_ambient, IrrepLevi[left]),
+        CompletelyReducibleBundle(right_ambient, IrrepLevi[right]),
       ),
     )
   end
@@ -809,20 +777,15 @@ function _factor_ambient_bundle_on_product(
   factorization === nothing ? nothing : [factorization]
 end
 
-function _product_of_zero_loci(product_factors)
-  length(product_factors) == 1 && return only(product_factors)
-  product(product_factors[1], product_factors[2], product_factors[3:end]...)
-end
-
 function _product_bipartitions(Z::ZeroLocus)
-  product_factors = factors(Z)
-  result = Tuple{ZeroLocus,ZeroLocus}[]
-  for split_index in 1:(length(product_factors) - 1)
-    left = _product_of_zero_loci(product_factors[1:split_index])
-    right = _product_of_zero_loci(product_factors[(split_index + 1):end])
-    product(left, right) == Z && push!(result, (left, right))
-  end
-  result
+  parts = factors(Z)
+  partitions = [
+    (
+      reduce(product, parts[1:split]),
+      reduce(product, parts[(split + 1):end]),
+    ) for split in 1:(length(parts) - 1)
+  ]
+  filter(pair -> product(pair...) == Z, partitions)
 end
 
 function _presentation_from_factor_data(
@@ -838,85 +801,52 @@ function _presentation_from_factor_data(
   ZeroLocusBundle(locus, _AmbientBundlePresentation(terms))
 end
 
-function _factor_data_rank(data, degree_shift::Int)
-  sum(
-    (isodd(degree + degree_shift) ? -1 : 1) * multiplicity * rank(bundle) for
-    (bundle, (degree, multiplicity)) in data;
-    init=0,
-  )
-end
-
 function _factor_presentation_component(
-  edges, left_locus::ZeroLocus, right_locus::ZeroLocus
+  terms, left_locus::ZeroLocus, right_locus::ZeroLocus
 )
-  factorization = _rank_one_bipartite_factor(edges)
-  factorization === nothing && return nothing
-  left_data, right_data = factorization
+  factor_data = _factor_product_terms(terms)
+  factor_data === nothing && return nothing
+  left_data, right_data = factor_data
 
   shifts = intersect(
     Set(-degree for (_, (degree, _)) in left_data),
     Set(degree for (_, (degree, _)) in right_data),
   )
-  candidates = Tuple{ZeroLocusBundle,ZeroLocusBundle}[]
-  component_rank = sum(
-    (isodd(degree) ? -1 : 1) * multiplicity * rank(left) * rank(right) for
-    ((left, right), degrees) in edges for
-    (degree, multiplicity) in degrees;
+  factor_rank(data, shift) = sum(
+    (isodd(degree + shift) ? -1 : 1) * multiplicity * rank(bundle) for
+    (bundle, (degree, multiplicity)) in data;
     init=0,
   )
+  filter!(
+    shift -> factor_rank(left_data, shift) > 0 && factor_rank(right_data, -shift) > 0,
+    shifts,
+  )
+  length(shifts) == 1 || return nothing
 
-  for shift in shifts
-    left_rank = _factor_data_rank(left_data, shift)
-    right_rank = _factor_data_rank(right_data, -shift)
-    left_rank > 0 && right_rank > 0 || continue
-    left_rank * right_rank == component_rank || continue
-
-    left = _presentation_from_factor_data(left_locus, left_data, shift)
-    right = _presentation_from_factor_data(right_locus, right_data, -shift)
-    push!(candidates, (left, right))
-  end
-  length(candidates) == 1 ? only(candidates) : nothing
-end
-
-function _degree_zero_kunneth_decomposition(
-  F::ZeroLocusBundle, left_locus::ZeroLocus, right_locus::ZeroLocus
-)
-  terms = F.presentation.terms
-  length(terms) == 1 && haskey(terms, 0) || return nothing
-
-  left_ambient = ambient_variety(left_locus)
-  right_ambient = ambient_variety(right_locus)
-  decomposition = Tuple{ZeroLocusBundle,ZeroLocusBundle}[]
-  for summand in terms[0]
-    factorizations = _factor_ambient_bundle_on_product(
-      summand, left_ambient, right_ambient
-    )
-    factorizations === nothing && return nothing
-    for (left, right) in factorizations
-      push!(decomposition, (restrict(left_locus, left), restrict(right_locus, right)))
-    end
-  end
-  decomposition
+  shift = only(shifts)
+  (
+    _presentation_from_factor_data(left_locus, left_data, shift),
+    _presentation_from_factor_data(right_locus, right_data, -shift),
+  )
 end
 
 """
 Recognize a presentation as a direct sum of external tensor products.
 
 The recognition depends only on the current locus and presentation. It first
-finds a product decomposition of the zero locus, then checks complete
-bipartite rank-one conditions on the ambient presentation. Ambiguous or
-nonfactorable presentations return `nothing` and use the generic LES backend.
+finds a product decomposition of the zero locus. It then groups presentation
+terms that share a left or right factor and checks that every group is the
+rectangular grid produced by one external tensor product. Presentation degrees
+must split as sums and multiplicities as products. Ambiguous or nonfactorable
+presentations return `nothing` and use the generic LES backend.
 """
 function _kunneth_decomposition(
   F::ZeroLocusBundle, left_locus::ZeroLocus, right_locus::ZeroLocus
 )
-  degree_zero_decomposition = _degree_zero_kunneth_decomposition(F, left_locus, right_locus)
-  degree_zero_decomposition === nothing || return degree_zero_decomposition
-
   left_ambient = ambient_variety(left_locus)
   right_ambient = ambient_variety(right_locus)
 
-  edges = Dict{Tuple{_AmbientBundle,_AmbientBundle},Dict{Int,Int}}()
+  terms = Dict{Tuple{_AmbientBundle,_AmbientBundle},Tuple{Int,Int}}()
   for (degree, summands) in F.presentation.terms
     for summand in summands
       factorizations = _factor_ambient_bundle_on_product(
@@ -924,28 +854,24 @@ function _kunneth_decomposition(
       )
       factorizations === nothing && return nothing
       for (left, right) in factorizations
-        _add_bipartite_edge!(edges, left, right, degree)
+        _add_product_term!(terms, left, right, degree) || return nothing
       end
     end
   end
-  isempty(edges) && return nothing
+  isempty(terms) && return nothing
 
   decomposition = Tuple{ZeroLocusBundle,ZeroLocusBundle}[]
-  for component in _bipartite_components(edges)
-    factorization = _factor_presentation_component(
-      component, left_locus, right_locus
-    )
-    factorization === nothing && return nothing
-    push!(decomposition, factorization)
+  for component in _product_term_components(terms)
+    factors = _factor_presentation_component(component, left_locus, right_locus)
+    factors === nothing && return nothing
+    push!(decomposition, factors)
   end
-  sum(pair -> rank(pair[1]) * rank(pair[2]), decomposition; init=0) == rank(F) ||
-    return nothing
   decomposition
 end
 
 function _kunneth_decomposition(F::ZeroLocusBundle)
-  for (left_locus, right_locus) in _product_bipartitions(variety(F))
-    decomposition = _kunneth_decomposition(F, left_locus, right_locus)
+  for loci in _product_bipartitions(variety(F))
+    decomposition = _kunneth_decomposition(F, loci...)
     decomposition === nothing || return decomposition
   end
   nothing
@@ -958,13 +884,11 @@ function _kunneth_cohomology(F::ZeroLocusBundle)
   d = dimension(variety(F))
   entries = zeros(BigInt, d + 1)
   for (left, right) in decomposition
-    left_cohomology = cohomology(left)
-    right_cohomology = cohomology(right)
-    is_determined(left_cohomology) && is_determined(right_cohomology) || return nothing
-    for left_degree in 0:left_cohomology.max_degree
-      for right_degree in 0:right_cohomology.max_degree
-        entries[left_degree + right_degree + 1] +=
-          left_cohomology[left_degree].constant * right_cohomology[right_degree].constant
+    left_coh, right_coh = cohomology(left), cohomology(right)
+    is_determined(left_coh) && is_determined(right_coh) || return nothing
+    for p in 0:left_coh.max_degree
+      for q in 0:right_coh.max_degree
+        entries[p + q + 1] += left_coh[p].constant * right_coh[q].constant
       end
     end
   end

From 8f2b7917de8fd7f33bf07ad2b2ff0ab99192dbd1 Mon Sep 17 00:00:00 2001
From: Pieter Belmans <pieterbelmans@gmail.com>
Date: Tue, 1 Sep 2026 15:15:27 +0200
Subject: [PATCH 05/10] =?UTF-8?q?test:=20cover=20K=C3=BCnneth=20factor=20r?=
 =?UTF-8?q?ecognition?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/runtests.jl | 55 +++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 54 insertions(+), 1 deletion(-)

diff --git a/test/runtests.jl b/test/runtests.jl
index 7076e07..dfe8333 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -656,6 +656,21 @@ mdt(::Type{DT}, marked) where {DT<:DynkinType} = MarkedDynkinType(DT, marked)
     @test total_bundle(mixed_left) == external_tensor_product(total_bundle(F), M)
     @test total_bundle(mixed_right) == external_tensor_product(L, total_bundle(G))
     @test iszero(external_tensor_product(F, zero_bundle(Y)))
+
+    H = filtered_tangent_bundle(full_flag_variety(TypeB{2}))
+    FH = external_tensor_product(F, H)
+    filtered_factors = only(
+      PartialFlagVarieties._factor_ambient_bundle_on_product(FH, variety(F), variety(H))
+    )
+    @test external_tensor_product(filtered_factors...) == FH
+
+    one_step_product = external_tensor_product(G, G)
+    one_step_factors = only(
+      PartialFlagVarieties._factor_ambient_bundle_on_product(
+        one_step_product, variety(G), variety(G)
+      ),
+    )
+    @test external_tensor_product(one_step_factors...) == total_bundle(one_step_product)
   end
 
   @testset "Twist" begin
@@ -2265,6 +2280,45 @@ mdt(::Type{DT}, marked) where {DT<:DynkinType} = MarkedDynkinType(DT, marked)
   end
 
   @testset "Bundles on zero loci: external operations" begin
+    # An external tensor product has rectangular support, additive degrees,
+    # and rank-one multiplicities in its left/right factor grid.
+    factor_terms = PartialFlagVarieties._factor_product_terms
+    term_components = PartialFlagVarieties._product_term_components
+    add_term! = PartialFlagVarieties._add_product_term!
+    product_terms = Dict(
+      (:a, :x) => (1, 6),
+      (:a, :y) => (4, 8),
+      (:b, :x) => (2, 15),
+      (:b, :y) => (5, 20),
+    )
+    left_data, right_data = factor_terms(product_terms)
+    for ((left, right), (degree, multiplicity)) in product_terms
+      left_degree, left_multiplicity = left_data[left]
+      right_degree, right_multiplicity = right_data[right]
+      @test degree == left_degree + right_degree
+      @test multiplicity == left_multiplicity * right_multiplicity
+    end
+
+    disconnected_terms = merge(product_terms, Dict((:c, :z) => (0, 1)))
+    @test sort!(length.(term_components(disconnected_terms))) == [1, 4]
+    incomplete_terms = copy(product_terms)
+    delete!(incomplete_terms, (:b, :y))
+    @test all(
+      isnothing ∘ factor_terms,
+      (
+        empty(product_terms),
+        incomplete_terms,
+        merge(product_terms, Dict((:b, :y) => (6, 20))),
+        merge(product_terms, Dict((:b, :y) => (5, 21))),
+      ),
+    )
+
+    repeated_term = Dict{Tuple{Symbol,Symbol},Tuple{Int,Int}}()
+    @test add_term!(repeated_term, :a, :x, 2, 3)
+    @test add_term!(repeated_term, :a, :x, 2, 4)
+    @test repeated_term[(:a, :x)] == (2, 7)
+    @test !add_term!(repeated_term, :a, :x, 3)
+
     Z = zero_locus(line_bundle(projective_space(2), 1))
     W = zero_locus(line_bundle(projective_space(2), 2))
     ZW = product(Z, W)
@@ -2323,7 +2377,6 @@ mdt(::Type{DT}, marked) where {DT<:DynkinType} = MarkedDynkinType(DT, marked)
     )
     manual_bundle = restrict(manual_locus, manual_ambient_bundle)
     @test manual_locus == product(quartic, quartic)
-    @test length(PartialFlagVarieties._kunneth_decomposition(manual_bundle)) == 3
     @test cohomology(manual_bundle).entries == AffineExpr.([9, 0, 10, 0, 1])
   end
 

From 6135b81ee64da5978deed790bcca996d678a6067 Mon Sep 17 00:00:00 2001
From: Pieter Belmans <pieterbelmans@gmail.com>
Date: Tue, 1 Sep 2026 15:15:27 +0200
Subject: [PATCH 06/10] =?UTF-8?q?docs:=20explain=20K=C3=BCnneth=20factor?=
 =?UTF-8?q?=20recognition?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 docs/src/api/zero_loci.md | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/docs/src/api/zero_loci.md b/docs/src/api/zero_loci.md
index f97cbdf..af689bc 100644
--- a/docs/src/api/zero_loci.md
+++ b/docs/src/api/zero_loci.md
@@ -126,8 +126,11 @@ direct sum of external tensor products. If so, and the factor cohomology is
 determined, it applies the Künneth formula. This is structural recognition:
 the optimization also applies when the locus and bundle merely have the
 factorable form, regardless of whether `product` or an `external_*` constructor
-created them. Ambiguous or nonfactorable presentations safely use the generic
-solver.
+created them. Concretely, the recognizer groups terms sharing a factor and
+checks that each group forms the rectangular grid of an external tensor
+product: its presentation degrees must split as sums of factor degrees and its
+multiplicities as products of factor multiplicities. Ambiguous or nonfactorable
+presentations safely use the generic solver.
 
 !!! note "Generic bundle cohomology versus the Hodge engine"
     `cohomology(exterior_power(cotangent_bundle(Z), p))` evaluates that one

From 7f0d959a6b517c63c2816850c328810c623d51b4 Mon Sep 17 00:00:00 2001
From: Pieter Belmans <pieterbelmans@gmail.com>
Date: Tue, 1 Sep 2026 16:08:34 +0200
Subject: [PATCH 07/10] refactor: simplify product recognition

---
 src/ExternalProducts.jl | 194 ++++++++++++++++++++++++++++++++++
 src/ZeroLoci.jl         |  18 +---
 src/ZeroLocusBundles.jl | 226 +++++-----------------------------------
 3 files changed, 223 insertions(+), 215 deletions(-)

diff --git a/src/ExternalProducts.jl b/src/ExternalProducts.jl
index 3ec8304..9e990c4 100644
--- a/src/ExternalProducts.jl
+++ b/src/ExternalProducts.jl
@@ -19,6 +19,8 @@ function _lift_bundle_to_product(
   )
 end
 
+# Lift two ambient bundles to the common product ambient, placing the right
+# bundle after the left Dynkin block.
 function _lift_external_factors(
   product_ambient::PartialFlagVariety,
   E::_AmbientBundle,
@@ -96,3 +98,195 @@ function external_direct_sum(
   lifted_E, lifted_F = _lift_external_factors(product_ambient, E, F, right_offset)
   direct_sum(lifted_E, lifted_F)
 end
+
+# ═══════════════════════════════════════════════════════════════════════════════
+#  Structural factorization of ambient external products
+# ═══════════════════════════════════════════════════════════════════════════════
+
+# Partition `1:n` into connected components, joining all vertices occurring in
+# one support. Unused vertices remain singleton components.
+function _connected_support_components(supports, n)
+  parent = collect(1:n)
+  root(i) = parent[i] == i ? i : (parent[i] = root(parent[i]))
+  for support in supports, vertex in support
+    parent[root(vertex)] = root(first(support))
+  end
+  components = [Int[] for _ in 1:n]
+  for vertex in 1:n
+    push!(components[root(vertex)], vertex)
+  end
+  filter(!isempty, components)
+end
+
+# Split the highest weight of a product-group representation into its two
+# Dynkin blocks. This depends only on the requested ambient bipartition.
+function _split_product_irrep(
+  irrep::IrrepLevi,
+  left_ambient::PartialFlagVariety,
+  right_ambient::PartialFlagVariety,
+)
+  coefficients = collect(Int, Semisimple.coefficients(p_dominant_weight(irrep)))
+  left_type = dynkin_type(left_ambient)
+  right_type = dynkin_type(right_ambient)
+  left_rank = rank(left_type)
+  right_rank = rank(right_type)
+  length(coefficients) == left_rank + right_rank || return nothing
+
+  left_weight = WeightLatticeElem(left_type, coefficients[1:left_rank])
+  right_weight = WeightLatticeElem(right_type, coefficients[(left_rank + 1):end])
+  (
+    IrrepLevi(marked_dynkin_type(left_ambient), left_weight),
+    IrrepLevi(marked_dynkin_type(right_ambient), right_weight),
+  )
+end
+
+# Product terms are stored as `(left, right) => (degree, multiplicity)`.
+# Repeated pairs must occur in the same degree to admit this factorization.
+function _add_product_term!(terms, left, right, degree::Int, multiplicity::Int=1)
+  key = (left, right)
+  if haskey(terms, key)
+    old_degree, old_multiplicity = terms[key]
+    old_degree == degree || return false
+    terms[key] = (degree, old_multiplicity + multiplicity)
+  else
+    terms[key] = (degree, multiplicity)
+  end
+  true
+end
+
+# Partition pairs into candidate summands. Pairs are linked when they share a
+# left or right factor; the transitive closure gives the maximal groups.
+function _product_term_components(terms)
+  pairs = collect(keys(terms))
+  lefts = unique(first(pair) for pair in pairs)
+  rights = unique(last(pair) for pair in pairs)
+  left_index = Dict(left => index for (index, left) in enumerate(lefts))
+  right_index = Dict(right => index for (index, right) in enumerate(rights))
+  supports = [
+    (left_index[left], length(lefts) + right_index[right]) for
+    (left, right) in pairs
+  ]
+  blocks = _connected_support_components(supports, length(lefts) + length(rights))
+  [
+    typeof(terms)(
+      pair => terms[pair] for (pair, support) in zip(pairs, supports) if
+      first(support) in block
+    ) for block in blocks
+  ]
+end
+
+# Recover two factors from a connected term group. External products have
+# rectangular support, additive degrees, and multiplicative multiplicities.
+function _factor_product_terms(terms)
+  isempty(terms) && return nothing
+  lefts = unique(first(pair) for pair in keys(terms))
+  rights = unique(last(pair) for pair in keys(terms))
+  length(terms) == length(lefts) * length(rights) || return nothing
+
+  degree(left, right) = first(terms[(left, right)])
+  multiplicity(left, right) = last(terms[(left, right)])
+
+  # The split is defined up to an opposite degree shift and a common integer
+  # factor. Normalize with left degree zero and a primitive right first row.
+  left0, right0 = first(lefts), first(rights)
+  left_scale = gcd((multiplicity(left0, right) for right in rights)...)
+  right_data = Dict(
+    right => (
+      degree(left0, right),
+      multiplicity(left0, right) ÷ left_scale,
+    ) for right in rights
+  )
+  right_scale = last(right_data[right0])
+  all(multiplicity(left, right0) % right_scale == 0 for left in lefts) ||
+    return nothing
+  left_data = Dict(
+    left => (
+      degree(left, right0) - degree(left0, right0),
+      multiplicity(left, right0) ÷ right_scale,
+    ) for left in lefts
+  )
+
+  for left in lefts, right in rights
+    left_degree, left_multiplicity = left_data[left]
+    right_degree, right_multiplicity = right_data[right]
+    terms[(left, right)] == (
+      left_degree + right_degree,
+      left_multiplicity * right_multiplicity,
+    ) || return nothing
+  end
+  left_data, right_data
+end
+
+# Rebuild a filtered factor from `(filtration degree, multiplicity)` data for
+# each irreducible representation.
+function _filtered_bundle_from_factor_data(ambient::PartialFlagVariety, data)
+  pieces = Dict{Int,Vector{IrrepLevi}}()
+  for (irrep, (degree, multiplicity)) in data
+    append!(get!(pieces, degree, IrrepLevi[]), fill(irrep, multiplicity))
+  end
+  ordered_pieces = CompletelyReducibleBundle[
+    CompletelyReducibleBundle(ambient, pieces[degree]) for
+    degree in sort!(collect(keys(pieces)))
+  ]
+  FilteredBundle(ambient, ordered_pieces)
+end
+
+# Factor a multi-step filtered bundle by factoring its grid of irreducible
+# graded pieces, then verify the reconstructed external product structurally.
+function _factor_filtered_bundle_on_product(
+  bundle::FilteredBundle,
+  left_ambient::PartialFlagVariety,
+  right_ambient::PartialFlagVariety,
+)
+  terms = Dict{Tuple{IrrepLevi,IrrepLevi},Tuple{Int,Int}}()
+  for (degree, piece) in enumerate(graded_pieces(bundle))
+    for irrep in components(piece)
+      split = _split_product_irrep(irrep, left_ambient, right_ambient)
+      split === nothing && return nothing
+      _add_product_term!(terms, split[1], split[2], degree) || return nothing
+    end
+  end
+  factor_data = _factor_product_terms(terms)
+  factor_data === nothing && return nothing
+  left_data, right_data = factor_data
+
+  left = _filtered_bundle_from_factor_data(left_ambient, left_data)
+  right = _filtered_bundle_from_factor_data(right_ambient, right_data)
+  normalize(F) = n_filtration_steps(F) == 1 ? total_bundle(F) : F
+  factor_pair = normalize(left), normalize(right)
+  external_tensor_product(factor_pair...) == bundle ? factor_pair : nothing
+end
+
+# Split every irreducible summand of a completely reducible ambient bundle.
+# The result is its direct-sum decomposition into external tensor products.
+function _factor_ambient_bundle_on_product(
+  bundle::CompletelyReducibleBundle,
+  left_ambient::PartialFlagVariety,
+  right_ambient::PartialFlagVariety,
+)
+  splits = [
+    _split_product_irrep(irrep, left_ambient, right_ambient) for
+    irrep in components(bundle)
+  ]
+  any(isnothing, splits) && return nothing
+  [
+    (
+      CompletelyReducibleBundle(left_ambient, IrrepLevi[split[1]]),
+      CompletelyReducibleBundle(right_ambient, IrrepLevi[split[2]]),
+    ) for split in splits
+  ]
+end
+
+# A one-step filtration is normalized to its total bundle; a genuine
+# multi-step filtration is factored as one filtered external product.
+function _factor_ambient_bundle_on_product(
+  bundle::FilteredBundle,
+  left_ambient::PartialFlagVariety,
+  right_ambient::PartialFlagVariety,
+)
+  n_filtration_steps(bundle) == 1 && return _factor_ambient_bundle_on_product(
+    total_bundle(bundle), left_ambient, right_ambient
+  )
+  factorization = _factor_filtered_bundle_on_product(bundle, left_ambient, right_ambient)
+  factorization === nothing ? nothing : [factorization]
+end
diff --git a/src/ZeroLoci.jl b/src/ZeroLoci.jl
index d444c20..17093aa 100644
--- a/src/ZeroLoci.jl
+++ b/src/ZeroLoci.jl
@@ -210,7 +210,7 @@ function factors(Z::ZeroLocus)
   ]
   supports = [findall(block -> any(!iszero, block), row) for row in summand_rows]
 
-  blocks = _connected_ambient_factors(supports, length(ambient_factors))
+  blocks = _connected_support_components(supports, length(ambient_factors))
   length(blocks) == 1 && return [Z]
 
   parts = ZeroLocus[]
@@ -239,22 +239,6 @@ function factors(Z::ZeroLocus)
   filter(part -> dimension(part) >= 1 || euler_characteristic(part) >= 2, parts)
 end
 
-# Partition the ambient factors `1:n` into connected blocks, joining two factors
-# whenever some bundle summand is supported on both (union–find with path
-# compression). Untouched factors form singleton blocks.
-function _connected_ambient_factors(supports, n)
-  parent = collect(1:n)
-  root(i) = parent[i] == i ? i : (parent[i] = root(parent[i]))
-  for support in supports, factor in support
-    parent[root(factor)] = root(first(support))
-  end
-  blocks = [Int[] for _ in 1:n]
-  for factor in 1:n
-    push!(blocks[root(factor)], factor)
-  end
-  return filter(!isempty, blocks)
-end
-
 """
     n_factors(Z::ZeroLocus) -> Int
 
diff --git a/src/ZeroLocusBundles.jl b/src/ZeroLocusBundles.jl
index 6725c60..3122e56 100644
--- a/src/ZeroLocusBundles.jl
+++ b/src/ZeroLocusBundles.jl
@@ -25,11 +25,14 @@ struct _AmbientBundlePresentation
   end
 end
 
+# Wrap one ambient bundle as a one-term presentation in the requested degree.
 _AmbientBundlePresentation(degree::Int, bundle::_AmbientBundle) =
   _AmbientBundlePresentation(
     Dict{Int,Vector{_AmbientBundle}}(degree => _AmbientBundle[bundle])
   )
 
+# Compare summand multisets; their order within one presentation degree carries
+# no mathematical information.
 function _same_summands(left::Vector{_AmbientBundle}, right::Vector{_AmbientBundle})
   length(left) == length(right) || return false
   unmatched = trues(length(right))
@@ -99,6 +102,7 @@ variety(F::ZeroLocusBundle) = F.locus
 """Return the ambient partial flag variety of the base of `F`."""
 ambient_variety(F::ZeroLocusBundle) = ambient_variety(variety(F))
 
+# Guard binary bundle operations against mixing different zero loci.
 function _check_same_locus(F::ZeroLocusBundle, G::ZeroLocusBundle, operation::String)
   variety(F) == variety(G) || throw(
     ArgumentError("$operation requires bundles on the same zero locus.")
@@ -187,6 +191,8 @@ function _lift_bundle_to_product(
   ZeroLocusBundle(product_locus, _AmbientBundlePresentation(terms))
 end
 
+# Lift two presentations to their common product zero locus, placing the right
+# presentation after the left ambient Dynkin block.
 function _lift_external_factors(F::ZeroLocusBundle, G::ZeroLocusBundle)
   product_locus = product(variety(F), variety(G))
   right_offset = rank(dynkin_type(ambient_variety(F)))
@@ -535,6 +541,8 @@ end
 #  Additive invariants and cohomology
 # ═══════════════════════════════════════════════════════════════════════════════
 
+# Evaluate the Euler characteristic of an ambient bundle after restriction;
+# a filtration contributes the sum of its graded pieces.
 _euler_characteristic_on_restriction(Z::ZeroLocus, F::CompletelyReducibleBundle) =
   _euler_characteristic_from_counts(Z, _to_counts(F))
 
@@ -563,6 +571,7 @@ end
 
 chi(F::ZeroLocusBundle) = euler_characteristic(F)
 
+# Dispatch an ambient summand to the appropriate restriction LES backend.
 function _restriction_cohomology(
   Z::ZeroLocus, F::CompletelyReducibleBundle, var_counter::Ref{Int}
 )
@@ -575,6 +584,8 @@ function _restriction_cohomology(
   _restrict_to_zero_locus_les(Z, F, var_counter)
 end
 
+# Add the restriction cohomologies of all ambient summands in one presentation
+# degree; the presentation overload supplies an empty degree when necessary.
 function _presentation_term_cohomology(
   Z::ZeroLocus, summands::Vector{_AmbientBundle}, var_counter::Ref{Int}
 )
@@ -602,192 +613,8 @@ end
 #  Structural Künneth recognition
 # ═══════════════════════════════════════════════════════════════════════════
 
-function _split_product_irrep(
-  irrep::IrrepLevi,
-  left_ambient::PartialFlagVariety,
-  right_ambient::PartialFlagVariety,
-)
-  coefficients = collect(Int, Semisimple.coefficients(p_dominant_weight(irrep)))
-  left_type = dynkin_type(left_ambient)
-  right_type = dynkin_type(right_ambient)
-  left_rank = rank(left_type)
-  right_rank = rank(right_type)
-  length(coefficients) == left_rank + right_rank || return nothing
-
-  left_weight = WeightLatticeElem(left_type, coefficients[1:left_rank])
-  right_weight = WeightLatticeElem(right_type, coefficients[(left_rank + 1):end])
-  (
-    IrrepLevi(marked_dynkin_type(left_ambient), left_weight),
-    IrrepLevi(marked_dynkin_type(right_ambient), right_weight),
-  )
-end
-
-# Product terms are stored as `(left, right) => (degree, multiplicity)`.
-function _add_product_term!(terms, left, right, degree::Int, multiplicity::Int=1)
-  key = (left, right)
-  if haskey(terms, key)
-    old_degree, old_multiplicity = terms[key]
-    old_degree == degree || return false
-    terms[key] = (degree, old_multiplicity + multiplicity)
-  else
-    terms[key] = (degree, multiplicity)
-  end
-  true
-end
-
-# Partition pairs into candidate summands. Pairs are linked when they share a
-# left or right factor; the transitive closure gives the maximal groups.
-function _product_term_components(terms)
-  pending = Set(keys(terms))
-  components = Vector{typeof(terms)}()
-
-  while !isempty(pending)
-    seed = pop!(pending)
-    component = typeof(terms)(seed => terms[seed])
-    frontier = [seed]
-
-    while !isempty(frontier)
-      pair = pop!(frontier)
-      for candidate in collect(pending)
-        if first(candidate) == first(pair) || last(candidate) == last(pair)
-          delete!(pending, candidate)
-          component[candidate] = terms[candidate]
-          push!(frontier, candidate)
-        end
-      end
-    end
-    push!(components, component)
-  end
-  components
-end
-
-"""
-Recover two factors from a connected group of terms `(left, right) => (degree,
-multiplicity)`. An external tensor product has rectangular support, additive
-degrees, and multiplicative multiplicities. Degrees are normalized by setting
-the first left degree to zero; multiplicities by the gcd of the first row.
-"""
-function _factor_product_terms(terms)
-  isempty(terms) && return nothing
-  lefts = unique(first(pair) for pair in keys(terms))
-  rights = unique(last(pair) for pair in keys(terms))
-  length(terms) == length(lefts) * length(rights) || return nothing
-
-  degree(left, right) = first(terms[(left, right)])
-  multiplicity(left, right) = last(terms[(left, right)])
-
-  left0, right0 = first(lefts), first(rights)
-  left0_multiplicity = gcd((multiplicity(left0, right) for right in rights)...)
-  right_data = Dict(
-    right => (
-      degree(left0, right),
-      multiplicity(left0, right) ÷ left0_multiplicity,
-    ) for right in rights
-  )
-  right0_multiplicity = last(right_data[right0])
-  all(multiplicity(left, right0) % right0_multiplicity == 0 for left in lefts) ||
-    return nothing
-  left_data = Dict(
-    left => (
-      degree(left, right0) - degree(left0, right0),
-      multiplicity(left, right0) ÷ right0_multiplicity,
-    ) for left in lefts
-  )
-
-  for left in lefts, right in rights
-    left_degree, left_multiplicity = left_data[left]
-    right_degree, right_multiplicity = right_data[right]
-    terms[(left, right)] == (
-      left_degree + right_degree,
-      left_multiplicity * right_multiplicity,
-    ) || return nothing
-  end
-  left_data, right_data
-end
-
-function _filtered_bundle_from_factor_data(ambient::PartialFlagVariety, data)
-  pieces = Dict{Int,Vector{IrrepLevi}}()
-  for (irrep, (degree, multiplicity)) in data
-    append!(get!(pieces, degree, IrrepLevi[]), fill(irrep, multiplicity))
-  end
-  ordered_pieces = CompletelyReducibleBundle[
-    CompletelyReducibleBundle(ambient, pieces[degree]) for
-    degree in sort!(collect(keys(pieces)))
-  ]
-  FilteredBundle(ambient, ordered_pieces)
-end
-
-function _factor_filtered_bundle_on_product(
-  bundle::FilteredBundle,
-  left_ambient::PartialFlagVariety,
-  right_ambient::PartialFlagVariety,
-)
-  terms = Dict{Tuple{IrrepLevi,IrrepLevi},Tuple{Int,Int}}()
-  for (degree, piece) in enumerate(graded_pieces(bundle))
-    for irrep in components(piece)
-      split = _split_product_irrep(irrep, left_ambient, right_ambient)
-      split === nothing && return nothing
-      _add_product_term!(terms, split[1], split[2], degree) || return nothing
-    end
-  end
-  factor_data = _factor_product_terms(terms)
-  factor_data === nothing && return nothing
-  left_data, right_data = factor_data
-
-  left = _filtered_bundle_from_factor_data(left_ambient, left_data)
-  right = _filtered_bundle_from_factor_data(right_ambient, right_data)
-  options(F) = n_filtration_steps(F) == 1 ? (total_bundle(F), F) : (F,)
-  matches = [
-    pair for pair in Iterators.product(options(left), options(right)) if
-    external_tensor_product(pair...) == bundle
-  ]
-  length(matches) == 1 ? only(matches) : nothing
-end
-
-function _factor_ambient_bundle_on_product(
-  bundle::CompletelyReducibleBundle,
-  left_ambient::PartialFlagVariety,
-  right_ambient::PartialFlagVariety,
-)
-  result = Tuple{_AmbientBundle,_AmbientBundle}[]
-  for irrep in components(bundle)
-    split = _split_product_irrep(irrep, left_ambient, right_ambient)
-    split === nothing && return nothing
-    left, right = split
-    push!(
-      result,
-      (
-        CompletelyReducibleBundle(left_ambient, IrrepLevi[left]),
-        CompletelyReducibleBundle(right_ambient, IrrepLevi[right]),
-      ),
-    )
-  end
-  result
-end
-
-function _factor_ambient_bundle_on_product(
-  bundle::FilteredBundle,
-  left_ambient::PartialFlagVariety,
-  right_ambient::PartialFlagVariety,
-)
-  n_filtration_steps(bundle) == 1 && return _factor_ambient_bundle_on_product(
-    total_bundle(bundle), left_ambient, right_ambient
-  )
-  factorization = _factor_filtered_bundle_on_product(bundle, left_ambient, right_ambient)
-  factorization === nothing ? nothing : [factorization]
-end
-
-function _product_bipartitions(Z::ZeroLocus)
-  parts = factors(Z)
-  partitions = [
-    (
-      reduce(product, parts[1:split]),
-      reduce(product, parts[(split + 1):end]),
-    ) for split in 1:(length(parts) - 1)
-  ]
-  filter(pair -> product(pair...) == Z, partitions)
-end
-
+# Turn factor data back into a zero-locus-bundle presentation, applying the
+# chosen opposite cohomological shift.
 function _presentation_from_factor_data(
   locus::ZeroLocus, data, degree_shift::Int
 )
@@ -801,6 +628,8 @@ function _presentation_from_factor_data(
   ZeroLocusBundle(locus, _AmbientBundlePresentation(terms))
 end
 
+# Factor one connected presentation component and choose the unique shift for
+# which both factor presentations have positive rank in degree zero.
 function _factor_presentation_component(
   terms, left_locus::ZeroLocus, right_locus::ZeroLocus
 )
@@ -830,16 +659,8 @@ function _factor_presentation_component(
   )
 end
 
-"""
-Recognize a presentation as a direct sum of external tensor products.
-
-The recognition depends only on the current locus and presentation. It first
-finds a product decomposition of the zero locus. It then groups presentation
-terms that share a left or right factor and checks that every group is the
-rectangular grid produced by one external tensor product. Presentation degrees
-must split as sums and multiplicities as products. Ambiguous or nonfactorable
-presentations return `nothing` and use the generic LES backend.
-"""
+# Recognize the presentation as a direct sum of external tensor products for
+# one fixed bipartition of its zero locus. Failure is deliberately conservative.
 function _kunneth_decomposition(
   F::ZeroLocusBundle, left_locus::ZeroLocus, right_locus::ZeroLocus
 )
@@ -869,14 +690,23 @@ function _kunneth_decomposition(
   decomposition
 end
 
+# Try every contiguous bipartition of the recognized zero-locus factors and
+# return the first valid presentation decomposition.
 function _kunneth_decomposition(F::ZeroLocusBundle)
-  for loci in _product_bipartitions(variety(F))
-    decomposition = _kunneth_decomposition(F, loci...)
+  Z = variety(F)
+  parts = factors(Z)
+  for split in 1:(length(parts) - 1)
+    left = reduce(product, parts[1:split])
+    right = reduce(product, parts[(split + 1):end])
+    product(left, right) == Z || continue
+    decomposition = _kunneth_decomposition(F, left, right)
     decomposition === nothing || return decomposition
   end
   nothing
 end
 
+# Convolve determined factor cohomologies. Symbolic factor cohomology rejects
+# the shortcut so the caller can fall back to the generic presentation solver.
 function _kunneth_cohomology(F::ZeroLocusBundle)
   decomposition = _kunneth_decomposition(F)
   decomposition === nothing && return nothing

From 1d56ba389ba562b61c4f81e7cdcee1827bc6e8e4 Mon Sep 17 00:00:00 2001
From: Pieter Belmans <pieterbelmans@gmail.com>
Date: Tue, 1 Sep 2026 16:08:34 +0200
Subject: [PATCH 08/10] test: cover product recognition fallbacks

---
 test/runtests.jl | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/test/runtests.jl b/test/runtests.jl
index dfe8333..25353b1 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -657,6 +657,13 @@ mdt(::Type{DT}, marked) where {DT<:DynkinType} = MarkedDynkinType(DT, marked)
     @test total_bundle(mixed_right) == external_tensor_product(L, total_bundle(G))
     @test iszero(external_tensor_product(F, zero_bundle(Y)))
 
+    mixed_factors = only(
+      PartialFlagVarieties._factor_ambient_bundle_on_product(
+        mixed_left, variety(F), variety(M)
+      ),
+    )
+    @test external_tensor_product(mixed_factors...) == mixed_left
+
     H = filtered_tangent_bundle(full_flag_variety(TypeB{2}))
     FH = external_tensor_product(F, H)
     filtered_factors = only(
@@ -2368,6 +2375,19 @@ mdt(::Type{DT}, marked) where {DT<:DynkinType} = MarkedDynkinType(DT, marked)
         line_bundle(product_ambient, [0, 4]),
       ),
     )
+    nonfactorable_filtration = FilteredBundle(
+      product_ambient,
+      CompletelyReducibleBundle[
+        line_bundle(product_ambient, [1, 0]),
+        line_bundle(product_ambient, [0, 1]),
+      ],
+    )
+    @test isnothing(
+      PartialFlagVarieties._kunneth_decomposition(
+        restrict(manual_locus, nonfactorable_filtration)
+      ),
+    )
+
     manual_ambient_bundle = direct_sum(
       direct_sum(
         structure_sheaf(product_ambient),

From febd221019062bdbcd05884bd7f82d7d39353942 Mon Sep 17 00:00:00 2001
From: Pieter Belmans <pieterbelmans@gmail.com>
Date: Tue, 1 Sep 2026 16:40:54 +0200
Subject: [PATCH 09/10] =?UTF-8?q?refactor:=20isolate=20K=C3=BCnneth=20reco?=
 =?UTF-8?q?gnition?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/ExternalProducts.jl     | 192 ------------------------
 src/Kunneth.jl              | 286 ++++++++++++++++++++++++++++++++++++
 src/PartialFlagVarieties.jl |   1 +
 src/ZeroLocusBundles.jl     | 116 ---------------
 test/runtests.jl            |   6 +-
 5 files changed, 290 insertions(+), 311 deletions(-)
 create mode 100644 src/Kunneth.jl

diff --git a/src/ExternalProducts.jl b/src/ExternalProducts.jl
index 9e990c4..f3e875a 100644
--- a/src/ExternalProducts.jl
+++ b/src/ExternalProducts.jl
@@ -98,195 +98,3 @@ function external_direct_sum(
   lifted_E, lifted_F = _lift_external_factors(product_ambient, E, F, right_offset)
   direct_sum(lifted_E, lifted_F)
 end
-
-# ═══════════════════════════════════════════════════════════════════════════════
-#  Structural factorization of ambient external products
-# ═══════════════════════════════════════════════════════════════════════════════
-
-# Partition `1:n` into connected components, joining all vertices occurring in
-# one support. Unused vertices remain singleton components.
-function _connected_support_components(supports, n)
-  parent = collect(1:n)
-  root(i) = parent[i] == i ? i : (parent[i] = root(parent[i]))
-  for support in supports, vertex in support
-    parent[root(vertex)] = root(first(support))
-  end
-  components = [Int[] for _ in 1:n]
-  for vertex in 1:n
-    push!(components[root(vertex)], vertex)
-  end
-  filter(!isempty, components)
-end
-
-# Split the highest weight of a product-group representation into its two
-# Dynkin blocks. This depends only on the requested ambient bipartition.
-function _split_product_irrep(
-  irrep::IrrepLevi,
-  left_ambient::PartialFlagVariety,
-  right_ambient::PartialFlagVariety,
-)
-  coefficients = collect(Int, Semisimple.coefficients(p_dominant_weight(irrep)))
-  left_type = dynkin_type(left_ambient)
-  right_type = dynkin_type(right_ambient)
-  left_rank = rank(left_type)
-  right_rank = rank(right_type)
-  length(coefficients) == left_rank + right_rank || return nothing
-
-  left_weight = WeightLatticeElem(left_type, coefficients[1:left_rank])
-  right_weight = WeightLatticeElem(right_type, coefficients[(left_rank + 1):end])
-  (
-    IrrepLevi(marked_dynkin_type(left_ambient), left_weight),
-    IrrepLevi(marked_dynkin_type(right_ambient), right_weight),
-  )
-end
-
-# Product terms are stored as `(left, right) => (degree, multiplicity)`.
-# Repeated pairs must occur in the same degree to admit this factorization.
-function _add_product_term!(terms, left, right, degree::Int, multiplicity::Int=1)
-  key = (left, right)
-  if haskey(terms, key)
-    old_degree, old_multiplicity = terms[key]
-    old_degree == degree || return false
-    terms[key] = (degree, old_multiplicity + multiplicity)
-  else
-    terms[key] = (degree, multiplicity)
-  end
-  true
-end
-
-# Partition pairs into candidate summands. Pairs are linked when they share a
-# left or right factor; the transitive closure gives the maximal groups.
-function _product_term_components(terms)
-  pairs = collect(keys(terms))
-  lefts = unique(first(pair) for pair in pairs)
-  rights = unique(last(pair) for pair in pairs)
-  left_index = Dict(left => index for (index, left) in enumerate(lefts))
-  right_index = Dict(right => index for (index, right) in enumerate(rights))
-  supports = [
-    (left_index[left], length(lefts) + right_index[right]) for
-    (left, right) in pairs
-  ]
-  blocks = _connected_support_components(supports, length(lefts) + length(rights))
-  [
-    typeof(terms)(
-      pair => terms[pair] for (pair, support) in zip(pairs, supports) if
-      first(support) in block
-    ) for block in blocks
-  ]
-end
-
-# Recover two factors from a connected term group. External products have
-# rectangular support, additive degrees, and multiplicative multiplicities.
-function _factor_product_terms(terms)
-  isempty(terms) && return nothing
-  lefts = unique(first(pair) for pair in keys(terms))
-  rights = unique(last(pair) for pair in keys(terms))
-  length(terms) == length(lefts) * length(rights) || return nothing
-
-  degree(left, right) = first(terms[(left, right)])
-  multiplicity(left, right) = last(terms[(left, right)])
-
-  # The split is defined up to an opposite degree shift and a common integer
-  # factor. Normalize with left degree zero and a primitive right first row.
-  left0, right0 = first(lefts), first(rights)
-  left_scale = gcd((multiplicity(left0, right) for right in rights)...)
-  right_data = Dict(
-    right => (
-      degree(left0, right),
-      multiplicity(left0, right) ÷ left_scale,
-    ) for right in rights
-  )
-  right_scale = last(right_data[right0])
-  all(multiplicity(left, right0) % right_scale == 0 for left in lefts) ||
-    return nothing
-  left_data = Dict(
-    left => (
-      degree(left, right0) - degree(left0, right0),
-      multiplicity(left, right0) ÷ right_scale,
-    ) for left in lefts
-  )
-
-  for left in lefts, right in rights
-    left_degree, left_multiplicity = left_data[left]
-    right_degree, right_multiplicity = right_data[right]
-    terms[(left, right)] == (
-      left_degree + right_degree,
-      left_multiplicity * right_multiplicity,
-    ) || return nothing
-  end
-  left_data, right_data
-end
-
-# Rebuild a filtered factor from `(filtration degree, multiplicity)` data for
-# each irreducible representation.
-function _filtered_bundle_from_factor_data(ambient::PartialFlagVariety, data)
-  pieces = Dict{Int,Vector{IrrepLevi}}()
-  for (irrep, (degree, multiplicity)) in data
-    append!(get!(pieces, degree, IrrepLevi[]), fill(irrep, multiplicity))
-  end
-  ordered_pieces = CompletelyReducibleBundle[
-    CompletelyReducibleBundle(ambient, pieces[degree]) for
-    degree in sort!(collect(keys(pieces)))
-  ]
-  FilteredBundle(ambient, ordered_pieces)
-end
-
-# Factor a multi-step filtered bundle by factoring its grid of irreducible
-# graded pieces, then verify the reconstructed external product structurally.
-function _factor_filtered_bundle_on_product(
-  bundle::FilteredBundle,
-  left_ambient::PartialFlagVariety,
-  right_ambient::PartialFlagVariety,
-)
-  terms = Dict{Tuple{IrrepLevi,IrrepLevi},Tuple{Int,Int}}()
-  for (degree, piece) in enumerate(graded_pieces(bundle))
-    for irrep in components(piece)
-      split = _split_product_irrep(irrep, left_ambient, right_ambient)
-      split === nothing && return nothing
-      _add_product_term!(terms, split[1], split[2], degree) || return nothing
-    end
-  end
-  factor_data = _factor_product_terms(terms)
-  factor_data === nothing && return nothing
-  left_data, right_data = factor_data
-
-  left = _filtered_bundle_from_factor_data(left_ambient, left_data)
-  right = _filtered_bundle_from_factor_data(right_ambient, right_data)
-  normalize(F) = n_filtration_steps(F) == 1 ? total_bundle(F) : F
-  factor_pair = normalize(left), normalize(right)
-  external_tensor_product(factor_pair...) == bundle ? factor_pair : nothing
-end
-
-# Split every irreducible summand of a completely reducible ambient bundle.
-# The result is its direct-sum decomposition into external tensor products.
-function _factor_ambient_bundle_on_product(
-  bundle::CompletelyReducibleBundle,
-  left_ambient::PartialFlagVariety,
-  right_ambient::PartialFlagVariety,
-)
-  splits = [
-    _split_product_irrep(irrep, left_ambient, right_ambient) for
-    irrep in components(bundle)
-  ]
-  any(isnothing, splits) && return nothing
-  [
-    (
-      CompletelyReducibleBundle(left_ambient, IrrepLevi[split[1]]),
-      CompletelyReducibleBundle(right_ambient, IrrepLevi[split[2]]),
-    ) for split in splits
-  ]
-end
-
-# A one-step filtration is normalized to its total bundle; a genuine
-# multi-step filtration is factored as one filtered external product.
-function _factor_ambient_bundle_on_product(
-  bundle::FilteredBundle,
-  left_ambient::PartialFlagVariety,
-  right_ambient::PartialFlagVariety,
-)
-  n_filtration_steps(bundle) == 1 && return _factor_ambient_bundle_on_product(
-    total_bundle(bundle), left_ambient, right_ambient
-  )
-  factorization = _factor_filtered_bundle_on_product(bundle, left_ambient, right_ambient)
-  factorization === nothing ? nothing : [factorization]
-end
diff --git a/src/Kunneth.jl b/src/Kunneth.jl
new file mode 100644
index 0000000..2e168f5
--- /dev/null
+++ b/src/Kunneth.jl
@@ -0,0 +1,286 @@
+# ═══════════════════════════════════════════════════════════════════════════════
+#  Structural Künneth recognition
+#
+#  No product provenance is stored. Recognition therefore runs backwards from
+#  product-group representations and ambient presentation terms, accepting only
+#  unambiguous external tensor-product decompositions.
+# ═══════════════════════════════════════════════════════════════════════════════
+
+# Partition `1:n_vertices` into connected components, joining all vertices in
+# one support. Unused vertices remain singleton components.
+function _connected_support_components(supports, n_vertices)
+  parent = collect(1:n_vertices)
+  root(i) = parent[i] == i ? i : (parent[i] = root(parent[i]))
+  for support in supports, vertex in support
+    parent[root(vertex)] = root(first(support))
+  end
+  components = [Int[] for _ in 1:n_vertices]
+  for vertex in 1:n_vertices
+    push!(components[root(vertex)], vertex)
+  end
+  filter(!isempty, components)
+end
+
+# Split a product-group highest weight at the boundary between the two ambient
+# Dynkin types.
+function _split_product_irrep(
+  irrep::IrrepLevi,
+  left_ambient::PartialFlagVariety,
+  right_ambient::PartialFlagVariety,
+)
+  coefficients = collect(Int, Semisimple.coefficients(p_dominant_weight(irrep)))
+  left_type = dynkin_type(left_ambient)
+  right_type = dynkin_type(right_ambient)
+  left_rank = rank(left_type)
+  length(coefficients) == left_rank + rank(right_type) || return nothing
+
+  left_weight = WeightLatticeElem(left_type, coefficients[1:left_rank])
+  right_weight = WeightLatticeElem(right_type, coefficients[(left_rank + 1):end])
+  (
+    IrrepLevi(marked_dynkin_type(left_ambient), left_weight),
+    IrrepLevi(marked_dynkin_type(right_ambient), right_weight),
+  )
+end
+
+# Add `(left, right) => (degree, multiplicity)` to a product grid. Repeated
+# factor pairs must have the same degree.
+function _add_product_term!(terms, pair, degree::Int, multiplicity::Int=1)
+  if haskey(terms, pair)
+    old_degree, old_multiplicity = terms[pair]
+    old_degree == degree || return false
+    terms[pair] = (degree, old_multiplicity + multiplicity)
+  else
+    terms[pair] = (degree, multiplicity)
+  end
+  true
+end
+
+# Group product-grid keys by shared left or right factor. Returning keys instead
+# of sub-dictionaries avoids copying all term values.
+function _product_term_components(terms)
+  pairs = collect(keys(terms))
+  lefts = unique(first(pair) for pair in pairs)
+  rights = unique(last(pair) for pair in pairs)
+  left_index = Dict(left => index for (index, left) in enumerate(lefts))
+  right_index = Dict(right => index for (index, right) in enumerate(rights))
+  supports = [
+    (left_index[left], length(lefts) + right_index[right]) for
+    (left, right) in pairs
+  ]
+  blocks = _connected_support_components(supports, length(lefts) + length(rights))
+  [
+    [pair for (pair, support) in zip(pairs, supports) if first(support) in block]
+    for block in blocks
+  ]
+end
+
+# Recover factors of one product grid. External products have rectangular
+# support, additive degrees, and multiplicative multiplicities.
+function _factor_product_terms(terms, component=keys(terms))
+  isempty(component) && return nothing
+  lefts = unique(first(pair) for pair in component)
+  rights = unique(last(pair) for pair in component)
+  length(component) == length(lefts) * length(rights) || return nothing
+
+  term_degree(left, right) = first(terms[(left, right)])
+  term_multiplicity(left, right) = last(terms[(left, right)])
+
+  # Normalize the opposite degree shift at the first left factor and the common
+  # multiplicity scale by the gcd of its row.
+  left_anchor, right_anchor = first(lefts), first(rights)
+  left_scale = gcd((term_multiplicity(left_anchor, right) for right in rights)...)
+  right_data = Dict(
+    right => (
+      term_degree(left_anchor, right),
+      term_multiplicity(left_anchor, right) ÷ left_scale,
+    ) for right in rights
+  )
+  right_scale = last(right_data[right_anchor])
+  all(term_multiplicity(left, right_anchor) % right_scale == 0 for left in lefts) ||
+    return nothing
+  left_data = Dict(
+    left => (
+      term_degree(left, right_anchor) - term_degree(left_anchor, right_anchor),
+      term_multiplicity(left, right_anchor) ÷ right_scale,
+    ) for left in lefts
+  )
+
+  for left in lefts, right in rights
+    left_degree, left_multiplicity = left_data[left]
+    right_degree, right_multiplicity = right_data[right]
+    terms[(left, right)] == (
+      left_degree + right_degree,
+      left_multiplicity * right_multiplicity,
+    ) || return nothing
+  end
+  left_data, right_data
+end
+
+# Expand factor data into terms grouped by degree. This is shared by filtered
+# bundles and zero-locus-bundle presentations.
+function _graded_factor_terms(data, ::Type{T}, shift::Int=0) where {T}
+  terms = Dict{Int,Vector{T}}()
+  for (term, (degree, multiplicity)) in data
+    append!(get!(terms, degree + shift, T[]), fill(term, multiplicity))
+  end
+  terms
+end
+
+# Rebuild a filtered factor from its irreducible factor data.
+function _filtered_bundle_from_factor_data(ambient::PartialFlagVariety, data)
+  terms = _graded_factor_terms(data, IrrepLevi)
+  FilteredBundle(
+    ambient,
+    CompletelyReducibleBundle[
+      CompletelyReducibleBundle(ambient, terms[degree]) for
+      degree in sort!(collect(keys(terms)))
+    ],
+  )
+end
+
+# Split every irreducible summand of a completely reducible ambient bundle.
+function _factor_ambient_bundle_on_product(
+  bundle::CompletelyReducibleBundle,
+  left_ambient::PartialFlagVariety,
+  right_ambient::PartialFlagVariety,
+)
+  splits = [
+    _split_product_irrep(irrep, left_ambient, right_ambient) for
+    irrep in components(bundle)
+  ]
+  any(isnothing, splits) && return nothing
+  [
+    (
+      CompletelyReducibleBundle(left_ambient, IrrepLevi[split[1]]),
+      CompletelyReducibleBundle(right_ambient, IrrepLevi[split[2]]),
+    ) for split in splits
+  ]
+end
+
+# Normalize a one-step filtration to its total bundle. For a genuine filtration,
+# factor its irreducible grid and verify the reconstructed external product.
+function _factor_ambient_bundle_on_product(
+  bundle::FilteredBundle,
+  left_ambient::PartialFlagVariety,
+  right_ambient::PartialFlagVariety,
+)
+  n_filtration_steps(bundle) == 1 && return _factor_ambient_bundle_on_product(
+    total_bundle(bundle), left_ambient, right_ambient
+  )
+
+  terms = Dict{Tuple{IrrepLevi,IrrepLevi},Tuple{Int,Int}}()
+  for (degree, piece) in enumerate(graded_pieces(bundle)), irrep in components(piece)
+    split = _split_product_irrep(irrep, left_ambient, right_ambient)
+    split === nothing && return nothing
+    _add_product_term!(terms, split, degree) || return nothing
+  end
+  factor_data = _factor_product_terms(terms)
+  factor_data === nothing && return nothing
+
+  left_data, right_data = factor_data
+  left = _filtered_bundle_from_factor_data(left_ambient, left_data)
+  right = _filtered_bundle_from_factor_data(right_ambient, right_data)
+  normalize_factor(F) = n_filtration_steps(F) == 1 ? total_bundle(F) : F
+  factor_pair = normalize_factor(left), normalize_factor(right)
+  external_tensor_product(factor_pair...) == bundle ? [factor_pair] : nothing
+end
+
+# Rebuild a zero-locus-bundle factor with the chosen cohomological shift.
+function _presentation_from_factor_data(
+  locus::ZeroLocus, data, degree_shift::Int
+)
+  terms = _graded_factor_terms(data, _AmbientBundle, degree_shift)
+  ZeroLocusBundle(locus, _AmbientBundlePresentation(terms))
+end
+
+# Factor one connected presentation component and choose the unique shift for
+# which both factor presentations have positive rank in degree zero.
+function _factor_presentation_component(
+  terms, component, left_locus::ZeroLocus, right_locus::ZeroLocus
+)
+  factor_data = _factor_product_terms(terms, component)
+  factor_data === nothing && return nothing
+  left_data, right_data = factor_data
+
+  shifts = intersect(
+    Set(-degree for (_, (degree, _)) in left_data),
+    Set(degree for (_, (degree, _)) in right_data),
+  )
+  factor_rank(data, shift) = sum(
+    (isodd(degree + shift) ? -1 : 1) * multiplicity * rank(bundle) for
+    (bundle, (degree, multiplicity)) in data;
+    init=0,
+  )
+  filter!(
+    shift -> factor_rank(left_data, shift) > 0 && factor_rank(right_data, -shift) > 0,
+    shifts,
+  )
+  length(shifts) == 1 || return nothing
+
+  shift = only(shifts)
+  (
+    _presentation_from_factor_data(left_locus, left_data, shift),
+    _presentation_from_factor_data(right_locus, right_data, -shift),
+  )
+end
+
+# Recognize a presentation as a direct sum of external products for one fixed
+# bipartition of its zero locus.
+function _kunneth_decomposition(
+  F::ZeroLocusBundle, left_locus::ZeroLocus, right_locus::ZeroLocus
+)
+  left_ambient = ambient_variety(left_locus)
+  right_ambient = ambient_variety(right_locus)
+  terms = Dict{Tuple{_AmbientBundle,_AmbientBundle},Tuple{Int,Int}}()
+
+  for (degree, summands) in F.presentation.terms, summand in summands
+    factorizations = _factor_ambient_bundle_on_product(summand, left_ambient, right_ambient)
+    factorizations === nothing && return nothing
+    for (left, right) in factorizations
+      _add_product_term!(terms, (left, right), degree) || return nothing
+    end
+  end
+  isempty(terms) && return nothing
+
+  decomposition = Tuple{ZeroLocusBundle,ZeroLocusBundle}[]
+  for component in _product_term_components(terms)
+    factor_pair = _factor_presentation_component(terms, component, left_locus, right_locus)
+    factor_pair === nothing && return nothing
+    push!(decomposition, factor_pair)
+  end
+  decomposition
+end
+
+# Try each contiguous bipartition of the recognized zero-locus factors.
+function _kunneth_decomposition(F::ZeroLocusBundle)
+  Z = variety(F)
+  locus_factors = factors(Z)
+  for split in 1:(length(locus_factors) - 1)
+    left = reduce(product, locus_factors[1:split])
+    right = reduce(product, locus_factors[(split + 1):end])
+    product(left, right) == Z || continue
+    decomposition = _kunneth_decomposition(F, left, right)
+    decomposition === nothing || return decomposition
+  end
+  nothing
+end
+
+# Convolve determined factor cohomologies; otherwise leave the generic
+# presentation solver to retain its symbolic answer.
+function _kunneth_cohomology(F::ZeroLocusBundle)
+  decomposition = _kunneth_decomposition(F)
+  decomposition === nothing && return nothing
+
+  d = dimension(variety(F))
+  entries = zeros(BigInt, d + 1)
+  for (left, right) in decomposition
+    left_cohomology = cohomology(left)
+    right_cohomology = cohomology(right)
+    is_determined(left_cohomology) && is_determined(right_cohomology) || return nothing
+    for p in 0:left_cohomology.max_degree, q in 0:right_cohomology.max_degree
+      entries[p + q + 1] +=
+        left_cohomology[p].constant * right_cohomology[q].constant
+    end
+  end
+  Cohomology{AffineExpr}(AffineExpr.(entries), d)
+end
diff --git a/src/PartialFlagVarieties.jl b/src/PartialFlagVarieties.jl
index 217bb49..a45b338 100644
--- a/src/PartialFlagVarieties.jl
+++ b/src/PartialFlagVarieties.jl
@@ -58,6 +58,7 @@ include("Constructions.jl")
 include("Koszul.jl")
 include("ZeroLoci.jl")
 include("ZeroLocusBundles.jl")
+include("Kunneth.jl")
 include("Labels.jl")
 include("ExceptionalCollections.jl")
 include("Hodge.jl")
diff --git a/src/ZeroLocusBundles.jl b/src/ZeroLocusBundles.jl
index 3122e56..9b3e708 100644
--- a/src/ZeroLocusBundles.jl
+++ b/src/ZeroLocusBundles.jl
@@ -609,122 +609,6 @@ function _presentation_term_cohomology(
   )
 end
 
-# ═══════════════════════════════════════════════════════════════════════════
-#  Structural Künneth recognition
-# ═══════════════════════════════════════════════════════════════════════════
-
-# Turn factor data back into a zero-locus-bundle presentation, applying the
-# chosen opposite cohomological shift.
-function _presentation_from_factor_data(
-  locus::ZeroLocus, data, degree_shift::Int
-)
-  terms = Dict{Int,Vector{_AmbientBundle}}()
-  for (bundle, (degree, multiplicity)) in data
-    append!(
-      get!(terms, degree + degree_shift, _AmbientBundle[]),
-      fill(bundle, multiplicity),
-    )
-  end
-  ZeroLocusBundle(locus, _AmbientBundlePresentation(terms))
-end
-
-# Factor one connected presentation component and choose the unique shift for
-# which both factor presentations have positive rank in degree zero.
-function _factor_presentation_component(
-  terms, left_locus::ZeroLocus, right_locus::ZeroLocus
-)
-  factor_data = _factor_product_terms(terms)
-  factor_data === nothing && return nothing
-  left_data, right_data = factor_data
-
-  shifts = intersect(
-    Set(-degree for (_, (degree, _)) in left_data),
-    Set(degree for (_, (degree, _)) in right_data),
-  )
-  factor_rank(data, shift) = sum(
-    (isodd(degree + shift) ? -1 : 1) * multiplicity * rank(bundle) for
-    (bundle, (degree, multiplicity)) in data;
-    init=0,
-  )
-  filter!(
-    shift -> factor_rank(left_data, shift) > 0 && factor_rank(right_data, -shift) > 0,
-    shifts,
-  )
-  length(shifts) == 1 || return nothing
-
-  shift = only(shifts)
-  (
-    _presentation_from_factor_data(left_locus, left_data, shift),
-    _presentation_from_factor_data(right_locus, right_data, -shift),
-  )
-end
-
-# Recognize the presentation as a direct sum of external tensor products for
-# one fixed bipartition of its zero locus. Failure is deliberately conservative.
-function _kunneth_decomposition(
-  F::ZeroLocusBundle, left_locus::ZeroLocus, right_locus::ZeroLocus
-)
-  left_ambient = ambient_variety(left_locus)
-  right_ambient = ambient_variety(right_locus)
-
-  terms = Dict{Tuple{_AmbientBundle,_AmbientBundle},Tuple{Int,Int}}()
-  for (degree, summands) in F.presentation.terms
-    for summand in summands
-      factorizations = _factor_ambient_bundle_on_product(
-        summand, left_ambient, right_ambient
-      )
-      factorizations === nothing && return nothing
-      for (left, right) in factorizations
-        _add_product_term!(terms, left, right, degree) || return nothing
-      end
-    end
-  end
-  isempty(terms) && return nothing
-
-  decomposition = Tuple{ZeroLocusBundle,ZeroLocusBundle}[]
-  for component in _product_term_components(terms)
-    factors = _factor_presentation_component(component, left_locus, right_locus)
-    factors === nothing && return nothing
-    push!(decomposition, factors)
-  end
-  decomposition
-end
-
-# Try every contiguous bipartition of the recognized zero-locus factors and
-# return the first valid presentation decomposition.
-function _kunneth_decomposition(F::ZeroLocusBundle)
-  Z = variety(F)
-  parts = factors(Z)
-  for split in 1:(length(parts) - 1)
-    left = reduce(product, parts[1:split])
-    right = reduce(product, parts[(split + 1):end])
-    product(left, right) == Z || continue
-    decomposition = _kunneth_decomposition(F, left, right)
-    decomposition === nothing || return decomposition
-  end
-  nothing
-end
-
-# Convolve determined factor cohomologies. Symbolic factor cohomology rejects
-# the shortcut so the caller can fall back to the generic presentation solver.
-function _kunneth_cohomology(F::ZeroLocusBundle)
-  decomposition = _kunneth_decomposition(F)
-  decomposition === nothing && return nothing
-
-  d = dimension(variety(F))
-  entries = zeros(BigInt, d + 1)
-  for (left, right) in decomposition
-    left_coh, right_coh = cohomology(left), cohomology(right)
-    is_determined(left_coh) && is_determined(right_coh) || return nothing
-    for p in 0:left_coh.max_degree
-      for q in 0:right_coh.max_degree
-        entries[p + q + 1] += left_coh[p].constant * right_coh[q].constant
-      end
-    end
-  end
-  Cohomology{AffineExpr}(AffineExpr.(entries), d)
-end
-
 """
 Compute cohomology from a complex which is exact away from degree zero.
 
diff --git a/test/runtests.jl b/test/runtests.jl
index 25353b1..961093b 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -2321,10 +2321,10 @@ mdt(::Type{DT}, marked) where {DT<:DynkinType} = MarkedDynkinType(DT, marked)
     )
 
     repeated_term = Dict{Tuple{Symbol,Symbol},Tuple{Int,Int}}()
-    @test add_term!(repeated_term, :a, :x, 2, 3)
-    @test add_term!(repeated_term, :a, :x, 2, 4)
+    @test add_term!(repeated_term, (:a, :x), 2, 3)
+    @test add_term!(repeated_term, (:a, :x), 2, 4)
     @test repeated_term[(:a, :x)] == (2, 7)
-    @test !add_term!(repeated_term, :a, :x, 3)
+    @test !add_term!(repeated_term, (:a, :x), 3)
 
     Z = zero_locus(line_bundle(projective_space(2), 1))
     W = zero_locus(line_bundle(projective_space(2), 2))

From 5aa4b88903e520da76e881d103a29e933267351a Mon Sep 17 00:00:00 2001
From: Pieter Belmans <pieterbelmans@gmail.com>
Date: Tue, 1 Sep 2026 17:12:02 +0200
Subject: [PATCH 10/10] =?UTF-8?q?refactor:=20simplify=20K=C3=BCnneth=20rec?=
 =?UTF-8?q?ognition?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/FilteredBundle.jl   |  30 +++----
 src/Kunneth.jl          | 173 +++++++++++++---------------------------
 src/ZeroLoci.jl         |  17 +++-
 src/ZeroLocusBundles.jl |   4 +-
 4 files changed, 92 insertions(+), 132 deletions(-)

diff --git a/src/FilteredBundle.jl b/src/FilteredBundle.jl
index 13c38f0..3acb84c 100644
--- a/src/FilteredBundle.jl
+++ b/src/FilteredBundle.jl
@@ -143,6 +143,20 @@ equals the empty filtered bundle on the same variety.
 """
 Base.iszero(F::FilteredBundle) = all(iszero, graded_pieces(F))
 
+# Assemble a filtered bundle from irreducible components indexed by filtration
+# degree, omitting absent degrees while preserving their order.
+function _filtered_bundle_from_graded_components(
+  X::PartialFlagVariety, terms::AbstractDict{Int,<:AbstractVector{IrrepLevi}}
+)
+  FilteredBundle(
+    X,
+    [
+      CompletelyReducibleBundle(X, terms[degree]) for
+      degree in sort!(collect(keys(terms)))
+    ],
+  )
+end
+
 # ═══════════════════════════════════════════════════════════════════════════════
 #  Tensor products involving FilteredBundle
 # ═══════════════════════════════════════════════════════════════════════════════
@@ -183,13 +197,7 @@ function tensor_product(F::FilteredBundle, G::FilteredBundle)
     end
   end
 
-  FilteredBundle(
-    variety(F),
-    CompletelyReducibleBundle[
-      CompletelyReducibleBundle(variety(F), terms[degree]) for
-      degree in sort!(collect(keys(terms)))
-    ],
-  )
+  _filtered_bundle_from_graded_components(variety(F), terms)
 end
 
 # ═══════════════════════════════════════════════════════════════════════════════
@@ -365,13 +373,7 @@ function _graded_power(power, F::FilteredBundle, k::Integer)
     append!(get!(weight_terms, filtration_degree, IrrepLevi[]), components(term))
   end
 
-  FilteredBundle(
-    F.variety,
-    CompletelyReducibleBundle[
-      CompletelyReducibleBundle(F.variety, weight_terms[filtration_degree]) for
-      filtration_degree in sort!(collect(keys(weight_terms)))
-    ],
-  )
+  _filtered_bundle_from_graded_components(F.variety, weight_terms)
 end
 
 """
diff --git a/src/Kunneth.jl b/src/Kunneth.jl
index 2e168f5..06b3b22 100644
--- a/src/Kunneth.jl
+++ b/src/Kunneth.jl
@@ -6,72 +6,51 @@
 #  unambiguous external tensor-product decompositions.
 # ═══════════════════════════════════════════════════════════════════════════════
 
-# Partition `1:n_vertices` into connected components, joining all vertices in
-# one support. Unused vertices remain singleton components.
-function _connected_support_components(supports, n_vertices)
-  parent = collect(1:n_vertices)
-  root(i) = parent[i] == i ? i : (parent[i] = root(parent[i]))
-  for support in supports, vertex in support
-    parent[root(vertex)] = root(first(support))
-  end
-  components = [Int[] for _ in 1:n_vertices]
-  for vertex in 1:n_vertices
-    push!(components[root(vertex)], vertex)
-  end
-  filter(!isempty, components)
-end
-
 # Split a product-group highest weight at the boundary between the two ambient
-# Dynkin types.
+# Dynkin types. Callers have already validated the product ambient.
 function _split_product_irrep(
   irrep::IrrepLevi,
   left_ambient::PartialFlagVariety,
   right_ambient::PartialFlagVariety,
 )
   coefficients = collect(Int, Semisimple.coefficients(p_dominant_weight(irrep)))
-  left_type = dynkin_type(left_ambient)
-  right_type = dynkin_type(right_ambient)
-  left_rank = rank(left_type)
-  length(coefficients) == left_rank + rank(right_type) || return nothing
-
-  left_weight = WeightLatticeElem(left_type, coefficients[1:left_rank])
-  right_weight = WeightLatticeElem(right_type, coefficients[(left_rank + 1):end])
+  left_rank = rank(dynkin_type(left_ambient))
   (
-    IrrepLevi(marked_dynkin_type(left_ambient), left_weight),
-    IrrepLevi(marked_dynkin_type(right_ambient), right_weight),
+    IrrepLevi(marked_dynkin_type(left_ambient), coefficients[1:left_rank]),
+    IrrepLevi(marked_dynkin_type(right_ambient), coefficients[(left_rank + 1):end]),
   )
 end
 
 # Add `(left, right) => (degree, multiplicity)` to a product grid. Repeated
 # factor pairs must have the same degree.
 function _add_product_term!(terms, pair, degree::Int, multiplicity::Int=1)
-  if haskey(terms, pair)
-    old_degree, old_multiplicity = terms[pair]
-    old_degree == degree || return false
-    terms[pair] = (degree, old_multiplicity + multiplicity)
-  else
-    terms[pair] = (degree, multiplicity)
-  end
+  old_degree, old_multiplicity = get(terms, pair, (degree, 0))
+  old_degree == degree || return false
+  terms[pair] = (degree, old_multiplicity + multiplicity)
   true
 end
 
-# Group product-grid keys by shared left or right factor. Returning keys instead
-# of sub-dictionaries avoids copying all term values.
+# Group product-grid keys by shared left or right factor. Presentations are
+# small, so a direct component walk is clearer than a separate graph structure.
 function _product_term_components(terms)
-  pairs = collect(keys(terms))
-  lefts = unique(first(pair) for pair in pairs)
-  rights = unique(last(pair) for pair in pairs)
-  left_index = Dict(left => index for (index, left) in enumerate(lefts))
-  right_index = Dict(right => index for (index, right) in enumerate(rights))
-  supports = [
-    (left_index[left], length(lefts) + right_index[right]) for
-    (left, right) in pairs
-  ]
-  blocks = _connected_support_components(supports, length(lefts) + length(rights))
-  [
-    [pair for (pair, support) in zip(pairs, supports) if first(support) in block]
-    for block in blocks
-  ]
+  remaining = Set(keys(terms))
+  components = Vector{Vector{keytype(terms)}}()
+  while !isempty(remaining)
+    component = keytype(terms)[pop!(remaining)]
+    cursor = 1
+    while cursor <= length(component)
+      pair = component[cursor]
+      neighbors = [
+        candidate for candidate in remaining if
+        first(candidate) == first(pair) || last(candidate) == last(pair)
+      ]
+      append!(component, neighbors)
+      setdiff!(remaining, neighbors)
+      cursor += 1
+    end
+    push!(components, component)
+  end
+  components
 end
 
 # Recover factors of one product grid. External products have rectangular
@@ -82,43 +61,28 @@ function _factor_product_terms(terms, component=keys(terms))
   rights = unique(last(pair) for pair in component)
   length(component) == length(lefts) * length(rights) || return nothing
 
-  term_degree(left, right) = first(terms[(left, right)])
-  term_multiplicity(left, right) = last(terms[(left, right)])
+  degrees = [first(terms[(left, right)]) for left in lefts, right in rights]
+  multiplicities = [last(terms[(left, right)]) for left in lefts, right in rights]
+  degrees == degrees[:, 1] .+ degrees[1, :]' .- degrees[1, 1] || return nothing
+  multiplicities .* multiplicities[1, 1] ==
+  multiplicities[:, 1] * multiplicities[1, :]' || return nothing
 
   # Normalize the opposite degree shift at the first left factor and the common
-  # multiplicity scale by the gcd of its row.
-  left_anchor, right_anchor = first(lefts), first(rights)
-  left_scale = gcd((term_multiplicity(left_anchor, right) for right in rights)...)
-  right_data = Dict(
-    right => (
-      term_degree(left_anchor, right),
-      term_multiplicity(left_anchor, right) ÷ left_scale,
-    ) for right in rights
-  )
-  right_scale = last(right_data[right_anchor])
-  all(term_multiplicity(left, right_anchor) % right_scale == 0 for left in lefts) ||
-    return nothing
+  # multiplicity scale by the gcd of its row. The rank-one identity makes the
+  # division of the first column below exact.
+  row_gcd = reduce(gcd, @view multiplicities[1, :])
+  right_multiplicities = multiplicities[1, :] .÷ row_gcd
+  left_multiplicities = multiplicities[:, 1] .÷ first(right_multiplicities)
   left_data = Dict(
-    left => (
-      term_degree(left, right_anchor) - term_degree(left_anchor, right_anchor),
-      term_multiplicity(left, right_anchor) ÷ right_scale,
-    ) for left in lefts
+    zip(lefts, zip(degrees[:, 1] .- degrees[1, 1], left_multiplicities))
   )
-
-  for left in lefts, right in rights
-    left_degree, left_multiplicity = left_data[left]
-    right_degree, right_multiplicity = right_data[right]
-    terms[(left, right)] == (
-      left_degree + right_degree,
-      left_multiplicity * right_multiplicity,
-    ) || return nothing
-  end
+  right_data = Dict(zip(rights, zip(degrees[1, :], right_multiplicities)))
   left_data, right_data
 end
 
 # Expand factor data into terms grouped by degree. This is shared by filtered
 # bundles and zero-locus-bundle presentations.
-function _graded_factor_terms(data, ::Type{T}, shift::Int=0) where {T}
+function _graded_factor_terms(data::AbstractDict{T}, shift::Int=0) where {T}
   terms = Dict{Int,Vector{T}}()
   for (term, (degree, multiplicity)) in data
     append!(get!(terms, degree + shift, T[]), fill(term, multiplicity))
@@ -126,35 +90,19 @@ function _graded_factor_terms(data, ::Type{T}, shift::Int=0) where {T}
   terms
 end
 
-# Rebuild a filtered factor from its irreducible factor data.
-function _filtered_bundle_from_factor_data(ambient::PartialFlagVariety, data)
-  terms = _graded_factor_terms(data, IrrepLevi)
-  FilteredBundle(
-    ambient,
-    CompletelyReducibleBundle[
-      CompletelyReducibleBundle(ambient, terms[degree]) for
-      degree in sort!(collect(keys(terms)))
-    ],
-  )
-end
-
 # Split every irreducible summand of a completely reducible ambient bundle.
 function _factor_ambient_bundle_on_product(
   bundle::CompletelyReducibleBundle,
   left_ambient::PartialFlagVariety,
   right_ambient::PartialFlagVariety,
 )
-  splits = [
-    _split_product_irrep(irrep, left_ambient, right_ambient) for
-    irrep in components(bundle)
-  ]
-  any(isnothing, splits) && return nothing
-  [
+  map(components(bundle)) do irrep
+    left, right = _split_product_irrep(irrep, left_ambient, right_ambient)
     (
-      CompletelyReducibleBundle(left_ambient, IrrepLevi[split[1]]),
-      CompletelyReducibleBundle(right_ambient, IrrepLevi[split[2]]),
-    ) for split in splits
-  ]
+      CompletelyReducibleBundle(left_ambient, [left]),
+      CompletelyReducibleBundle(right_ambient, [right]),
+    )
+  end
 end
 
 # Normalize a one-step filtration to its total bundle. For a genuine filtration,
@@ -171,28 +119,20 @@ function _factor_ambient_bundle_on_product(
   terms = Dict{Tuple{IrrepLevi,IrrepLevi},Tuple{Int,Int}}()
   for (degree, piece) in enumerate(graded_pieces(bundle)), irrep in components(piece)
     split = _split_product_irrep(irrep, left_ambient, right_ambient)
-    split === nothing && return nothing
     _add_product_term!(terms, split, degree) || return nothing
   end
   factor_data = _factor_product_terms(terms)
   factor_data === nothing && return nothing
 
-  left_data, right_data = factor_data
-  left = _filtered_bundle_from_factor_data(left_ambient, left_data)
-  right = _filtered_bundle_from_factor_data(right_ambient, right_data)
-  normalize_factor(F) = n_filtration_steps(F) == 1 ? total_bundle(F) : F
-  factor_pair = normalize_factor(left), normalize_factor(right)
+  factor_pair = map((left_ambient, right_ambient), factor_data) do ambient, data
+    factor = _filtered_bundle_from_graded_components(
+      ambient, _graded_factor_terms(data)
+    )
+    n_filtration_steps(factor) == 1 ? total_bundle(factor) : factor
+  end
   external_tensor_product(factor_pair...) == bundle ? [factor_pair] : nothing
 end
 
-# Rebuild a zero-locus-bundle factor with the chosen cohomological shift.
-function _presentation_from_factor_data(
-  locus::ZeroLocus, data, degree_shift::Int
-)
-  terms = _graded_factor_terms(data, _AmbientBundle, degree_shift)
-  ZeroLocusBundle(locus, _AmbientBundlePresentation(terms))
-end
-
 # Factor one connected presentation component and choose the unique shift for
 # which both factor presentations have positive rank in degree zero.
 function _factor_presentation_component(
@@ -218,10 +158,11 @@ function _factor_presentation_component(
   length(shifts) == 1 || return nothing
 
   shift = only(shifts)
-  (
-    _presentation_from_factor_data(left_locus, left_data, shift),
-    _presentation_from_factor_data(right_locus, right_data, -shift),
-  )
+  map((left_locus, right_locus), factor_data, (shift, -shift)) do locus, data, offset
+    ZeroLocusBundle(
+      locus, _AmbientBundlePresentation(_graded_factor_terms(data, offset))
+    )
+  end
 end
 
 # Recognize a presentation as a direct sum of external products for one fixed
diff --git a/src/ZeroLoci.jl b/src/ZeroLoci.jl
index 17093aa..bcadc0b 100644
--- a/src/ZeroLoci.jl
+++ b/src/ZeroLoci.jl
@@ -210,7 +210,7 @@ function factors(Z::ZeroLocus)
   ]
   supports = [findall(block -> any(!iszero, block), row) for row in summand_rows]
 
-  blocks = _connected_support_components(supports, length(ambient_factors))
+  blocks = _connected_ambient_factors(supports, length(ambient_factors))
   length(blocks) == 1 && return [Z]
 
   parts = ZeroLocus[]
@@ -239,6 +239,21 @@ function factors(Z::ZeroLocus)
   filter(part -> dimension(part) >= 1 || euler_characteristic(part) >= 2, parts)
 end
 
+# Partition the ambient factors into connected blocks, joining the support of
+# each defining-bundle summand. Untouched factors remain singleton blocks.
+function _connected_ambient_factors(supports, n)
+  parent = collect(1:n)
+  root(i) = parent[i] == i ? i : (parent[i] = root(parent[i]))
+  for support in supports, factor in support
+    parent[root(factor)] = root(first(support))
+  end
+  blocks = [Int[] for _ in 1:n]
+  for factor in 1:n
+    push!(blocks[root(factor)], factor)
+  end
+  filter(!isempty, blocks)
+end
+
 """
     n_factors(Z::ZeroLocus) -> Int
 
diff --git a/src/ZeroLocusBundles.jl b/src/ZeroLocusBundles.jl
index 9b3e708..b58a642 100644
--- a/src/ZeroLocusBundles.jl
+++ b/src/ZeroLocusBundles.jl
@@ -15,7 +15,9 @@ export ZeroLocusBundle, restrict
 struct _AmbientBundlePresentation
   terms::Dict{Int,Vector{_AmbientBundle}}
 
-  function _AmbientBundlePresentation(terms::Dict{Int,Vector{_AmbientBundle}})
+  function _AmbientBundlePresentation(
+    terms::AbstractDict{Int,<:AbstractVector{<:_AmbientBundle}}
+  )
     cleaned = Dict{Int,Vector{_AmbientBundle}}()
     for (degree, summands) in terms
       kept = _AmbientBundle[summand for summand in summands if rank(summand) != 0]