Successors of finite product… to Common finite bases of…
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
TheoremSuccessors of finite product expansions#
For arbitrary ι : Type u, J : Finset ι and d : ι → WithBot ℕ∞,
ENat.WithBot.succ_sum_powerset_nonempty
states that the bottom-aware successor of the sum of ∏ i ∈ U, d i over nonempty
subsets U of J equals ∏ i ∈ J, WithBot.succ (d i). The equality is in ℕ∞;
the subset products and their sum are in WithBot ℕ∞. Empty J and arbitrary
bottom and top values are included, with no decidable-equality premise on ι.
The proof reuses Mathlib's whole finite-product expansion Finset.prod_add_one.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
ENat.WithBot.succ_sum_powerset_nonempty(theorem), declared in MinimalPrimes/Data/ENat/BigOperators.lean, line 45.
Read from the source at commit 45952e34, without running Lean.
Sources
Ranks of dependent pointwise products
For arbitrary ι : Type u, independently universed given preorders
β : ι → Type v, and a section f : ∀ i, β i,
Order.height_pi_eq_iSup_finset and Order.coheight_pi_eq_iSup_finset
state
Order.height f = ⨆ s : Finset ι, ∑ i ∈ s, Order.height (f i)
Order.coheight f = ⨆ s : Finset ι, ∑ i ∈ s, Order.coheight (f i)
The supremum includes every finite coordinate set, including the empty set.
No finite-support condition on f or finiteness assumption on the index is needed.
Infinitely many positive finite coordinate ranks, or one infinite coordinate rank,
can give infinite rank. The proof detects each finite strict series on finitely
many coordinates and reuses the finite product formula on that restriction;
the reverse bound fills the remaining coordinates with the supplied f.
For a finite index ι : Type u, independently universed given preorders
β : ι → Type v, and a section f : ∀ i, β i,
Order.height_pi and Order.coheight_pi
state
Order.height f = ∑ i, Order.height (f i)
Order.coheight f = ∑ i, Order.coheight (f i)
These are equalities in ℕ∞ for the original pointwise product preorder and the
original fibre preorders, including infinite ranks and unbounded finite chain
lengths with no attaining chain. No antisymmetry, fibre inhabitation, finite-height
or attainment hypothesis is required. An empty index gives both ranks zero;
the top of the pointwise Fin 2 → Fin 2 square has height two, not lexicographic
rank three. The proofs compose the binary rank identities with Mathlib's
order-isomorphism rank invariance, canonical finite-Pi head/tail splitting and
reindexing, and finite-sum formulas.
TheoremDimension from finite coordinate-restriction images#
For arbitrary ι : Type u and independently universed given preorders
β : ι → Type v,
Order.krullDim_pi_eq_iSup_range_restrict
states
Order.krullDim (∀ i, β i) =
⨆ J : Finset ι,
Order.krullDim (Set.range
(fun f : (∀ i, β i) => fun j : J => f j.1))
The equality is in WithBot ℕ∞. Every range has the inherited ordinary pointwise
subtype order, and every restriction starts from the original full product.
Thus an empty full product makes every image empty, even for J = ∅, giving
bottom on both sides. An empty ambient index instead gives dimension zero.
No nonemptiness, finite-index, finite-fibre, antisymmetry, finite-rank,
attainment or finite-support hypothesis is required; an infinite supremum need
not be attained by a finite image. These are not lexicographic or topological
products. The proof combines the point-height formulas above with Mathlib's
height transport, finite updates and surjective range reindexing.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Order.krullDim_pi_eq_iSup_range_restrict(theorem), declared in MinimalPrimes/Order/KrullDimension.lean, line 823.
Read from the source at commit 45952e34, without running Lean.
Sources
TheoremChain cardinalities of unions#
For an arbitrary relation r and subsets s, t of any type,
Set.chainHeight_union_le gives
(s ∪ t).chainHeight r ≤ s.chainHeight r + t.chainHeight r.
The pieces may overlap or be empty; neither relation laws nor finite heights or
attainment are required. The proof restricts each comparable subset to its two
intersections and uses ENat cardinality subadditivity.
For disjoint pieces with ∀ a ∈ s, ∀ b ∈ t, r a b ∨ r b a,
Set.chainHeight_union_of_disjoint_of_cross
gives equality: (s ∪ t).chainHeight r = s.chainHeight r + t.chainHeight r.
Cross comparisons need not have a consistent direction. The binary lexicographic-sum
formula below reuses this common-ambient union result.
For an arbitrary relation q : X → X → Prop, family P : κ → Set X and
J : Finset κ, the finite-family formula
Set.chainHeight_biUnion_finset_of_disjoint_of_cross
states
(⋃ i ∈ J, P i).chainHeight q = ∑ i ∈ J, (P i).chainHeight q.
Pairwise disjointness and cross comparability are required only on J:
for distinct i,j ∈ J, the pieces are disjoint and every point of P i compares
with every point of P j in either direction. There are no relation laws,
ambient finiteness, decidable-equality, nonemptiness or attainment assumptions.
Empty pieces and unbounded, unattained chain heights are included.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Set.chainHeight_union_le(theorem), declared in MinimalPrimes/Order/ChainHeight.lean, line 585.
Read from the source at commit 45952e34, without running Lean.
Sources
TheoremChain cardinalities of exclusive-piece unions#
For an arbitrary relation r on α : Type u and a family s : ι → Set α with
independent ι : Sort v,
Set.chainHeight_iUnion_of_not_rel gives
(⋃ i, s i).chainHeight r = ⨆ i, (s i).chainHeight r when points in
s i \ s j and s j \ s i cannot compare for every ordered pair i,j.
For each pair, the no-cross condition concerns only its opposite exclusive pieces;
all loops remain unrestricted. The family need not be directed, finite or nonempty,
and no relation laws or attainment are assumed.
The heights are ENat vertex cardinalities: the empty union and empty supremum are
zero, a singleton has height one, and unbounded finite chain sizes give top.
The proof shows that the traces of each chain on the pieces are inclusion-directed
and applies the existing directed-union formula to those traces. It does not choose
one piece containing the whole chain: nested finite initial segments of an infinite
chain satisfy the hypothesis but no piece contains their union.
The retained Set.chainHeight_union_of_not_rel is the Bool-family corollary, giving
the two-piece maximum formula with the same exclusive-piece hypothesis.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Set.chainHeight_iUnion_of_not_rel(theorem), declared in MinimalPrimes/Order/ChainHeight.lean, line 879.
Read from the source at commit 45952e34, without running Lean.
Sources
TheoremKrull dimension of exclusive-piece unions#
For a given preorder on α : Type u, an arbitrary independent ι : Sort v, and
s : ι → Set α,
Order.krullDim_iUnion_of_not_lt states
Order.krullDim (⋃ i, s i) = ⨆ i, Order.krullDim (s i) when points in
s i \ s j and s j \ s i satisfy ¬ a < b for every ordered pair i,j.
All membership subtypes inherit the given preorder. No antisymmetry, inhabitation,
finiteness, directedness or attainment is assumed.
The finite-cut comparisons Order.le_krullDim_iff_le_chainHeight and
Order.krullDim_le_iff_chainHeight_le relate dimension bounds n : ℕ to
strict-chain height bounds n + 1, without assuming finite height. Dimension lies
in WithBot ℕ∞ and counts strict steps, whereas chain height lies in ℕ∞ and
counts vertices. Empty sets have values bottom and zero, singletons zero and one,
and unbounded finite chains give top. These generic order interfaces are
Mathlib-upstream candidates.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Order.krullDim_iUnion_of_not_lt(theorem), declared in MinimalPrimes/Order/KrullDimension.lean, line 500.
Read from the source at commit 45952e34, without running Lean.
Sources
TheoremDimension comparison and arbitrary unions#
For arbitrary subsets of independently universed given preorders,
Order.krullDim_le_krullDim_iff_chainHeight_le_chainHeight
states
κ(s) ≤ κ(t) ↔ H(s) ≤ H(t), where κ is the dimension of the membership
subtype in WithBot ℕ∞ and H is ambient strict-chain vertex height in ℕ∞.
There is no map between the carriers, and each subtype inherits its given preorder.
Empty sets have values bottom and zero; singletons have values zero and one.
Distinct equivalent preorder points do not form a strict step. Infinite values
include unbounded finite chains without a longest or infinite chain.
For arbitrary subsets in one given preorder, Order.krullDim_union_le states
κ(s ∪ t) ≤ κ(s) ⊔ κ(t) ⊔ (κ(s) + κ(t) + 1).
No disjointness, upper/lower closure, directedness, antisymmetry, nonemptiness,
finiteness or attainment is assumed. All right-hand operations are in WithBot ℕ∞;
the separate joins preserve the other dimension when one piece is empty, even at top.
In the five-point total order, the alternating pieces {0, 2, 4} and {1, 3}
have dimensions two and one, while their union has dimension four: the additive
term is sharp and a maximum-only bound fails. Overlap is also allowed.
The comparison extends the finite-cut dimension/height equivalences to arbitrary
bounds, including bottom and top. The arbitrary-union bound relates the existing
Set.chainHeight_union_le and Set.chainHeight_toLex_sum height formulas to the
exact dimension formula Order.krullDim_toLex_sum for lexicographic sums.
These interfaces build on Mathlib's subtype orders, Krull dimension, strict-chain
height and extended-natural arithmetic.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Order.krullDim_le_krullDim_iff_chainHeight_le_chainHeight(theorem), declared in MinimalPrimes/Order/KrullDimension.lean, line 1108.
Read from the source at commit 45952e34, without running Lean.
Sources
TheoremKrull dimension under finite covers#
For one given preorder on α : Type u, an independent index ι : Type v,
I : Finset ι, a family s : ι → Set α, and t ⊆ ⋃ i ∈ I, s i,
Order.krullDim_le_iSup_of_subset_biUnion_finset
states
Order.krullDim t ≤
⨆ J ∈ I.powerset, ⨆ (_ : J.Nonempty),
(∑ i ∈ J, Order.krullDim (s i)) + ((J.card - 1 : ℕ) : WithBot ℕ∞)
All membership subtypes inherit the given preorder. The pieces may overlap or be
empty; there is no finiteness, antisymmetry, closure or attainment assumption on the
ambient order. Subtraction takes place in the natural numbers before casting.
Restricting to nonempty subfamilies makes the bound bottom for an empty family or
an all-empty cover, while singleton subfamilies preserve a piece of top dimension.
The three singleton pieces of a three-point total order give the sharp term two
from the full subfamily. A literal finite union is the reflexive-inclusion application.
The finite chain-height sum bound is already supplied by Mathlib's
Finset.apply_union_le_sum applied to Set.chainHeight_empty and
Set.chainHeight_union_le, followed by Set.chainHeight_mono for subsets.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Order.krullDim_le_iSup_of_subset_biUnion_finset(theorem), declared in MinimalPrimes/Order/KrullDimension.lean, line 1660.
Read from the source at commit 45952e34, without running Lean.
Sources
TheoremChain cardinalities of disjoint sums#
For arbitrary relations rα, rβ on independently universed types and arbitrary
sets s, t, Set.chainHeight_sum_liftRel
gives chain height max (s.chainHeight rα) (t.chainHeight rβ) for the union of the
two tagged images under Sum.LiftRel rα rβ. No cross-tag points compare.
Set.chainHeight_sum gives the same formula
for ordinary α ⊕ β less-than, induced by precisely the two given LT records.
Neither result requires relation laws, nonemptiness, finiteness or attainment.
The heights are ENat vertex cardinalities: two nonempty antichains have disjoint-sum
height one, unlike lexicographic-sum height two. Empty factors contribute zero;
unbounded finite heights are included without assuming an infinite or longest chain.
The proof specializes the exclusive-piece maximum formula above, reusing Mathlib's
relation embeddings and image-height transport to identify the two tagged-piece heights.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Set.chainHeight_sum_liftRel(theorem), declared in MinimalPrimes/Order/ChainHeight.lean, line 933.
Read from the source at commit 45952e34, without running Lean.
Sources
TheoremFinite localization near a minimal prime#
For a finite-type algebra over any commutative ring, module finiteness of the
residue-field fibre at a minimal prime gives finiteness after inverting an element
outside that prime. The map is the canonical localization of the given algebra map.
Algebra.FiniteType.exists_finite_awayMap_of_mem_minimalPrimes
requires no reducedness or Noetherian hypothesis and includes the zero algebra.
The supporting nil-integrality lemmas
lift monic relations using individual nilpotence rather than a uniformly nilpotent ideal.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Algebra.FiniteType.exists_finite_awayMap_of_mem_minimalPrimes(theorem), declared in MinimalPrimes/RingTheory/Ideal/MinimalPrimeLocalization.lean, line 197.
Read from the source at commit 45952e34, without running Lean.
Sources
TheoremDirected suprema of relations on a fixed set#
For any type α and fixed subset s,
Set.scottContinuous_chainHeight states that
r ↦ s.chainHeight r is Scott continuous for the pointwise implication order on relations
α → α → Prop. No order or relation laws on α are needed. Scott continuity preserves
suprema of nonempty directed families, not arbitrary joins or bottom.
For a directed family r : ι → α → α → Prop, with independent ι : Sort v,
Set.chainHeight_iSup_of_directed gives
H(⨆ i, r i) = H(⊥) ⊔ ⨆ i, H(r i), where H(r) = s.chainHeight r takes values in
ENat and ⊔ is maximum. The false-relation baseline is zero for empty s and one
otherwise; it is essential when ι is empty. The proof captures all distinct-point
comparisons of a finite chain in one relation, without sorting or assuming attainment.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Set.scottContinuous_chainHeight(theorem), declared in MinimalPrimes/Order/ChainHeight.lean, line 806.
Read from the source at commit 45952e34, without running Lean.
Sources
TheoremDirected unions: chain cardinality and order dimension#
For an inclusion-directed family s : ι → Set α, with independent carrier and
index universes and an arbitrary index ι : Sort v,
Set.chainHeight_iUnion_of_directed
identifies the ENat chain height of the union with the supremum of the piece
heights for any relation on α. With only a preorder on α,
Order.krullDim_iUnion_of_directed
gives the analogous equality for the induced subtype orders in WithBot ℕ∞.
The relation invariant counts vertices; order dimension counts strict steps.
Empty unions have values zero and bottom respectively, and infinite suprema
need not be attained by a piece. No nonemptiness, antisymmetry or finite-height
assumption is required. The proofs capture finite chain witnesses in one piece;
they do not select a longest or infinite chain. These are relation-height and
induced-order formulas, not topological subspace dimension formulas.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Set.chainHeight_iUnion_of_directed(theorem), declared in MinimalPrimes/Order/ChainHeight.lean, line 216.
Read from the source at commit 45952e34, without running Lean.
Sources
TheoremChain cardinalities of lexicographic products#
For arbitrary relations rα, rβ on independently universed types and arbitrary
sets s, t, Set.chainHeight_prod_lex
proves that the chain height of s ×ˢ t for Prod.Lex rα rβ is the product of
the factor chain heights, provided rα is irreflexive on s. Neither relation
needs to be transitive; the second may have loops. Set.chainHeight_toLex_prod
transports this formula to the canonical less-than relation on the image under toLex,
with only LT on both types and first-relation Std.Irrefl.
These are ENat vertex cardinalities, not edge counts, Krull dimensions or
ordinal ranks. Empty factors give zero even beside infinite height. The proof
uses products of comparable subsets for the lower bound and finite first-coordinate
fibre counting for the upper bound, so it neither sorts a nontransitive comparable
set nor assumes a longest chain exists. It does not assert the analogous formula
for canonical weak ≤ in arbitrary preorders.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Set.chainHeight_prod_lex(theorem), declared in MinimalPrimes/Order/ChainHeight.lean, line 251.
Read from the source at commit 45952e34, without running Lean.
Sources
TheoremChain cardinalities of lexicographic sums#
For arbitrary relations rα, rβ on independently universed types and arbitrary
sets s, t, Set.chainHeight_sum_lex
proves that the union of the two injection images has chain height
s.chainHeight rα + t.chainHeight rβ for Sum.Lex rα rβ. Within each tag the
factor relation is used, and every left-tagged point precedes every right-tagged
point. No irreflexivity, transitivity, nonemptiness or finiteness is assumed.
Set.chainHeight_toLex_sum transports the formula under toLex to the canonical
less-than relation on α ⊕ₗ β, using only the given LT records on both factors.
The heights count vertices in ENat: two singleton blocks, or two nonempty
antichains, give height two. The disjoint relation Sum.LiftRel, used by ordinary
Sum less-than, is different. Empty factors contribute zero, including beside top.
The proof applies the disjoint cross-comparable union formula and Mathlib's
relation-embedding transport. Its union core glues subset chains by cross comparison,
without sorting chains or assuming their heights are attained. Unbounded finite
chain cardinalities are included.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Set.chainHeight_sum_lex(theorem), declared in MinimalPrimes/Order/ChainHeight.lean, line 624.
Read from the source at commit 45952e34, without running Lean.
Sources
- Chain cardinalities of dependent lexicographic sums
- Krull dimension of dependent lexicographic sums
- Krull dimension of lexicographic sums
TheoremKrull dimension of lexicographic products#
For arbitrary subsets s, t of independently universed preorders,
Order.krullDim_toLex_prod states
κ(toLex '' (s ×ˢ t)) = κ(s) * κ(t) + κ(s) + κ(t) in WithBot ℕ∞.
The carrier is the membership subtype of that image in α ×ₗ β, with the
Prod.Lex preorder of the given factor preorders. Ties in the first coordinate
require equality, not preorder equivalence. No antisymmetry, nonemptiness,
finiteness or attainment is assumed.
An empty factor gives bottom even beside top. In the stock arithmetic,
⊥ * 0 = 0, but the explicit bottom summand still absorbs the whole polynomial.
A singleton factor preserves the other dimension, including bottom and top;
top with dimension zero gives top despite its zero multiplication term.
Two distinct equivalent first coordinates with three-point chain fibres give
two incomparable fibres and dimension two. Infinite dimension includes
unbounded finite chains without a longest or infinite chain.
Fin 2 ×ₗ Fin 3 has dimension five, whereas its pointwise product has dimension
three and its tagged lexicographic sum has dimension four.
The vertex-height input is the existing whole Set.chainHeight_toLex_prod
formula, together with the finite-cut dimension comparisons above.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Order.krullDim_toLex_prod(theorem), declared in MinimalPrimes/Order/KrullDimension.lean, line 1031.
Read from the source at commit 45952e34, without running Lean.
Sources
Point heights and coheights of binary lexicographic products
For independently universed given preorders α : Type u, β : Type v and points
a : α, b : β, put Hβ = (Set.univ : Set β).chainHeight (· < ·). The formulas
Order.height_toLex_prod and Order.coheight_toLex_prod
are
height (toLex (a, b)) = height a * Hβ + height b
coheight (toLex (a, b)) = coheight a * Hβ + coheight b
All arithmetic is in ℕ∞. Both use the same whole-second-factor strict-chain
vertex cardinality, not its Krull dimension, the rank of b, or the cardinality
of β. The target retains Mathlib's binary Prod.Lex preorder on α ×ₗ β:
toLex (a, b) ≤ toLex (a', b') means a < a' or a = a' ∧ b ≤ b';
strict comparison replaces the second ≤ by <. Distinct weakly equivalent
first coordinates therefore give incomparable fibres. Within a fixed first
coordinate, distinct weakly equivalent second points remain mutually weakly
comparable. This is the binary preorder, not the equality-or-strict partial order
on dependent functions or the pointwise product order.
The supporting identities Order.height_eq_chainHeight_Iio and
Order.coheight_eq_chainHeight_Ioi identify point height and coheight with the
strict-chain vertex heights of the original strict lower and upper segments.
They use the given preorder's strict relation, without decomposing a closed
segment into its strict segment and an endpoint, which fails for general preorders.
There is no linearity, antisymmetry, finiteness, decidable equality, global
nonemptiness, bottom/top, finite-height or attainment hypothesis. The supplied
points inhabit both factors; empty strict segments have height zero, and
0 * ⊤ = 0. Infinite values include unbounded finite chains without a longest
or infinite chain.
The middle-point client gives both
height four and coheight four at toLex ((1 : Fin 3), (1 : Fin 3)), whereas the
pointwise pair has both ranks two. Here Hβ = 3, not the second-factor dimension
two. The proofs combine the strict-segment identities with the existing whole
lexicographic product, disjoint-union, singleton-slice and direction-reversal
chain-height APIs.
DefinitionSemimodules, annihilators and faithful actions on dependent reduced products#
For independent families R i, M i of semirings and additive commutative monoids,
with given Module (R i) (M i) records and an arbitrary filter F,
Filter.Product.module supplies
pointwise semimodule data on the existing F.Product M over the existing scalar
semiring F.Product R. The data are named rather than globally registered:
the given fibre actions stay fixed even when scalar and vector carriers coincide.
Representative equations characterize zero, addition, natural scaling and scalar
action. A represented scalar acts on every opaque vector by Filter.Product.map.
The additive record agrees with the existing semiring parent; constant records
recover Mathlib's two-germ module after identifying both base records.
The torsion-free criterion
Filter.Product.isTorsionFree_iff identifies torsion-freeness of this semimodule
over F.Product R with eventual torsion-freeness of the given fibre semimodules.
Torsion-freeness uses full injectivity of the action of every two-sided regular
scalar. The represented-scalar readout reduces action injectivity to eventual
fibre injectivity, and regular-scalar sections give reflection. No additive
inverses, cancellation, domain, properness or nontriviality assumption is required.
The varying-family client
applies the criterion to free semimodules of ranks n + 1 over ℕ × ZMod (n + 2)
along the cofinite filter, and uses the faithfulness criterion for the same family.
The annihilator and faithfulness criteria
retain these same given records. Filter.Product.coe_mem_annihilator_iff says that
a represented scalar annihilates the whole semimodule exactly when its values
annihilate the fibre semimodules eventually. Filter.Product.faithfulSMul_iff
says that the action is faithful exactly when the given fibre actions are faithful
eventually. Faithfulness compares two scalars on all vectors, unlike
represented-scalar injectivity; a zero annihilator does not characterize it at this
semiring floor. The weaker faithfulSMul_smul_iff needs only given fibre actions
and scalar/vector zeros, while smul_coe_eq_smul_coe_iff detects equality of two
represented actions using only vector zeros. These zeros provide total sections,
not zero-preservation laws. Bottom filters, empty indices and zero fibres remain
included, with independent scalar and vector universes.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Filter.Product.module(def), declared in MinimalPrimes/Order/Filter/Product/Module.lean, line 233.
Read from the source at commit 45952e34, without running Lean.
Sources
Matrix rings over dependent reduced products
For an arbitrary filter F, given semirings R i and a fixed index type J with
Fintype J and DecidableEq J, the
matrix leaf constructs
Filter.Product.matrixRingEquiv between F.Product (fun i => Matrix J J (R i))
and Matrix J J (F.Product R). Its underlying equivalence composes the existing
finite-Pi equivalences. The source and target retain the given semirings and stock
matrix records: multiplication is a finite row-column sum, not pointwise entry
multiplication. Representative and all-point entry equations in both directions
form its characteristic interface. Filter.Product.isUnit_matrix_coe_iff states
invertibility of a represented matrix exactly on the eventual unit locus of those
same fibre matrices; it does not assert that each entry is a scalar unit.
Index, coefficient and matrix-index universes are independent; empty matrices,
empty index types, bottom filters and zero semirings are included. There are no
commutativity, ring, field, properness or nontriviality hypotheses.
DefinitionCommon finite bases of dependent reduced products#
For the same given semiring and semimodule records, a family of given bases
b i : Module.Basis J (R i) (M i) with one common finite index J induces
Filter.Product.basis of
F.Product M over the existing scalar semiring F.Product R. Its vector at j
is represented by fun i => b i j, and coefficients are the existing varying
maps of the fibre coefficients, on represented and opaque vectors alike.
For standard function bases on J → R i, the whole coordinate equivalence agrees
with Filter.Product.piComparison. All four carrier universes are independent;
empty J, bottom filters and zero semirings are included. No commutativity,
faithfulness, properness or nontriviality hypothesis is imposed. A family of
unbounded varying ranks is not an instance of this common finite-index construction.
Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.
Lean
Filter.Product.basis(def), declared in MinimalPrimes/Order/Filter/Product/Basis.lean, line 168.
Read from the source at commit 45952e34, without running Lean.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.