Cardinalities of fibers of sign-valued functions #
This file records cardinality results for functions valued in SignType.
Since a sign takes only the three values 0, -1 and 1, the cardinality of the zero fiber of a
sign-valued function on a finite type is determined by the size of the domain together with the
cardinalities of the two nonzero fibers. This is what makes two sign-valued functions comparable
fiberwise once their positive and negative fibers are known to match: it upgrades an agreement of
the two nonzero fibers to an agreement of all three, as happens for the sign-valued
diagonalizations of two real quadratic forms with the same dimension and the same indices of
inertia.
Main results #
SignType.ncard_fiber_zero_add_ncard_fiber_neg_add_ncard_fiber_pos: the three fibers of a sign-valued function exhaust its domain.