An explicit basis for finite dependent products

This is the usual product basis, packaged so its basis vectors are definitionally a named single-coordinate function. Keeping the construction generic prevents downstream elaboration from specializing the internals of Pi.basis to large dependent module families.

noncomputable def MagnitudeConjecture.explicitBasisOfFamily {ι R M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (v : ι → M) (h : ∀ (i : ι), b i = v i) : Module.Basis ι R M

Rebuild a basis with an extensionally equal family as its explicit coefficient function.

@[simp]

theorem MagnitudeConjecture.explicitBasisOfFamily_apply {ι R M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (v : ι → M) (h : ∀ (i : ι), b i = v i) (i : ι) : (explicitBasisOfFamily b v h) i = v i

noncomputable def MagnitudeConjecture.piSingle {η : Type u} {M : η → Type u} [(a : η) → Zero (M a)] (a : η) (x : M a) (b : η) : M b

Insert a value into one coordinate of a dependent product, using one canonical classical decidable equality hidden behind a named definition.

theorem MagnitudeConjecture.piSingle_congr {η : Type u} {M : η → Type u} [(a : η) → Zero (M a)] {a : η} {x y : M a} (h : x = y) : piSingle a x = piSingle a y

Equality in the selected coordinate gives equality of the corresponding single-coordinate vectors.

def MagnitudeConjecture.piReindexLinearEquiv {R : Type u₁} {η : Type u₂} {ι : Type u₃} {M : η → Type u₄} [Semiring R] [(a : η) → AddCommMonoid (M a)] [(a : η) → Module R (M a)] (e : ι ≃ η) : ((i : ι) → M (e i)) ≃ₗ[R] (a : η) → M a

Reindex a dependent product along an equivalence. Keeping this wrapper generic prevents concrete large module families from expanding the internals of LinearEquiv.piCongrLeft during downstream elaboration.

noncomputable def MagnitudeConjecture.piBasisVector {R η : Type u} {ι M : η → Type u} [Semiring R] [Fintype η] [(a : η) → AddCommMonoid (M a)] [(a : η) → Module R (M a)] (s : (a : η) → Module.Basis (ι a) R (M a)) (t : (a : η) × ι a) (a : η) : M a

A basis vector inserted into one coordinate of a dependent product.

@[simp]

theorem MagnitudeConjecture.piBasisVector_mk {R η : Type u} {ι M : η → Type u} [Semiring R] [Fintype η] [(a : η) → AddCommMonoid (M a)] [(a : η) → Module R (M a)] (s : (a : η) → Module.Basis (ι a) R (M a)) (a : η) (i : ι a) : piBasisVector s ⟨a, i⟩ = piSingle a ((s a) i)

theorem MagnitudeConjecture.span_range_piBasisVector_eq_top {R η : Type u} {ι M : η → Type u} [Semiring R] [Fintype η] [(a : η) → AddCommMonoid (M a)] [(a : η) → Module R (M a)] (s : (a : η) → Module.Basis (ι a) R (M a)) : Submodule.span R (Set.range (piBasisVector s)) = ⊤

The named single-coordinate basis vectors span the dependent product.

noncomputable def MagnitudeConjecture.piExplicitBasis {R η : Type u} {ι M : η → Type u} [Semiring R] [Fintype η] [(a : η) → AddCommMonoid (M a)] [(a : η) → Module R (M a)] (s : (a : η) → Module.Basis (ι a) R (M a)) : Module.Basis ((a : η) × ι a) R ((a : η) → M a)

The explicit single-coordinate basis of a finite dependent product.

@[simp]

theorem MagnitudeConjecture.piExplicitBasis_apply {R η : Type u} {ι M : η → Type u} [Semiring R] [Fintype η] [(a : η) → AddCommMonoid (M a)] [(a : η) → Module R (M a)] (s : (a : η) → Module.Basis (ι a) R (M a)) (t : (a : η) × ι a) : (piExplicitBasis s) t = piBasisVector s t