Sage preamble definition catalogue — audit report

Audit of sage-preamble-definition-catalogue.md against the pinned Mathlib (.lake/packages/mathlib) and the lean-reference-corpus zoekt index. Evidence rule: an entry is checked only when a tool result named the exact declaration and file path.

1. Entries marked checked

51 of 285 entries are checked, each with a citation sub-line naming the owning declaration and file (all Mathlib/..., verified against the pinned checkout).

2. Entries left unchecked (residues)

234 of 285 entries remain unchecked. These are Sage-source machinery, named lattices and genus/Nikulin data, Galois/profinite group constructions, scheme facades, module/lattice method surfaces, or formalizations not found in the pinned Mathlib, lean-reference-corpus, or in-repo sources.

3. Full residue list

4. Uncertain or partial matches left unchecked

Each entry below has a verified Mathlib neighbour but not an exact owner for the whole bundle, so it stays unchecked per the evidence rule.

On 2026-08-16, 13 entries formerly listed here were re-verified directly against the pinned checkout and checked in the catalogue: BaseChangeFunctor (100), BaseChangeAdjunction (103), is_galois/galois_group (193), integral_basis (195), is_central (202), ProfiniteGroups (216), AbsoluteGaloisGroups (217), AbsoluteGaloisGroup (233), RingedSpaces (251), structure_sheaf/underlying_space/stalk (259), GradedModules/GradedAlgebras (290), FractionalIdeal (307), orthogonal_complement (331). The earlier “not found” claims were false negatives: several searches targeted the wrong file or directory (Algebra/Central/Defs.lean, FieldTheory/Galois/Basic.lean, AlgebraicGeometry/), and extension-of-scalars / base-change-adjunction exist in Algebra/Category/ModuleCat/ChangeOfRings.lean.

  • ConditionSet / ImageSet / PowerSet / SubsetsOfSize / FiniteSubsets: Set.image — Data/Set/Defs.lean:261; Set.powerset — Data/Set/Defs.lean:254; Finset.powersetCard — Data/Finset/Powerset.lean:198; ConditionSet/FiniteSubsets absent as standalone.
  • Ar(X,Y) / IsoAr(X,Y): Hom-set is foundational X ⟶ Y notation; no standalone Ar/IsoAr declaration.
  • SubObject / SuperObject / CoveringObject / CoveredObject: Only Subobject evidenced; SuperObject/CoveredObject absent.
  • DiagramCategory / DirectedSystem / InverseSystem: Diagrams are Functor in Mathlib; DirectedSystem class exists — Order/DirectedInverseSystem.lean:69 — but for direct systems over a preorder, not the inverse-system notion here; no named InverseSystem.
  • CartesianProductOfSets: Set.prod — Data/Set/Operations.lean:211; Finset.product exists; entry bundles a distinction claim.
  • AlgebraBaseChangeFunctor: Extension-of-scalars functor for algebras absent; AlgCat.restrictScalars — Algebra/Category/AlgCat/Basic.lean:261 — is the only verified half.
  • FreeModuleOnGroupFunctor: No named free-module-on-group functor; ModuleCat.free covers only the module ingredient.
  • TrivialActionFunctor: Action category exists; Action.trivial — CategoryTheory/Action/Basic.lean:73 — verifies the trivial-action construction, but the ε* : Lat → Lat_G functor is Sage design.
  • FramedAlgebras(R): Framing (chosen surjection) notion absent.
  • FreeAlgebras(R): FreeAlgebra verified; the category-of-free-algebras/grading aspects unverified.
  • FinitelyPresentedAlgebras(R); FramedFGAlgebras(R): Algebra.FinitePresentation (class) — RingTheory/FinitePresentation.lean:44 — verified; FramedFGAlgebras absent.
  • is_algebra / is_free / is_finitely_presented flags: Three-valued predicate machinery absent; Module.Free/FinitePresentation are the reachable parts.
  • FinitelyPresentedAlgebra F/I; FGAlgebra: Ideal.quotient exists; presented-algebra declaration unverified.
  • base_change (algebras): No verified base-change for algebras.
  • discriminant d_K: NumberField.discr and classNumber verified; signature via card_real_embeddings/card_complex_embeddings; ramified-primes part unverified.
  • element theory: norm/trace/minpoly/IsIntegral verified; charpoly/Bézout-inverse/embeddings parts unverified.
  • R^n: Product-module/Pi structure exists; a named R^n declaration unverified.
  • OwnedGroups: Group verified; the owned-groups Sage facade bundle unverified.
  • GroupsWithChosenFinitePresentation: GroupPresentation not found in Mathlib GroupTheory.
  • AbelianGroupEndomorphismRing End(A): Module.End/AddCommGroup (M →ₗ[R] N) exist; the End(A)-ring declaration unverified.
  • Schemes(S): Scheme verified; the 11-axiom bundle partial: Normal/Projective/QuasiAffine/QuasiProjective/FiniteType absent.
  • AffineSpaces / ProjectiveSpaces / ClosedSubschemes / OpenSubschemes: IsOpenImmersion/IsClosedImmersion verified; QuasiAffine/QuasiProjective/FiniteType parts absent.
  • Varieties(S): Smooth verified; variety = smooth+integral+proper bundle unverified.
  • DivisorGroups / ClassGroups / PicardGroups: Divisor-group machinery absent; ClassGroup — RingTheory/ClassGroup/Basic.lean:88 — verified; PicardGroup comparisons unverified.
  • SchemeMorphism: Scheme.Hom exists; the Sage facade bundle (compose/pullback/evaluate) unverified.
  • Pic(𝔸ⁿ)=0 / Cl(ℙⁿ)=ℤ theorems: Theorem statements; no verified formalization.
  • FinitelyGeneratedModules(R): Module.FG verified; the pure/framed stratification semantics differ.
  • FramedModules(R): Framing (surjection witness) notion absent.
  • FractionFieldQuotients(R): FractionRing/Localization exist; the K/𝔞 quotient bundle unverified.
  • BasedFreeModule: Module.Basis exists; the based-free-module declaration unverified.
  • FinitelyPresentedModule: No Module.FinitePresentation path pinned; only Algebra.FinitePresentation (rings/algebras) exists.
  • hermite_form / invariant_factor_form: smithNormalForm verified; hermite normal form absent (only the Hermite polynomial — RingTheory/Polynomial/Hermite/Basic.lean:48).
  • smith_form_module_generators bundle: Components (SNF/finrank/exponent/Fintype.card/IsTorsionFree) verified individually; the bundle is unchecked.
  • vector_space: Module 𝕜 V verified; a named VectorSpace declaration unverified.

5. Citation-format problems and naming notes

  • Cone/Cocone live in CategoryTheory/Limits/Cones.lean (plural file name), not Cone.lean.
  • HasBiproduct is a class in CategoryTheory/Limits/Shapes/Biproducts.lean (the Shapes layer); Preadditive/Biproducts.lean holds the additive theory on top.
  • The catalogue’s AlternatingAlgebra is ExteriorAlgebra in Mathlib (LinearAlgebra/ExteriorAlgebra/Basic.lean).
  • The catalogue’s DividedPowerAlgebra is the abbrev DividedPowerAlgebra in RingTheory/DividedPowerAlgebra/Init.lean.
  • TensorAlgebra lives in LinearAlgebra/TensorAlgebra/, not Algebra/TensorAlgebra/.
  • ModuleCat is a structure (Basic.lean:57); it is not a def or abbrev.
  • FreeAlgebra.lift is a def (an equivalence (X → A) ≃ (FreeAlgebra R X →ₐ[R] A)) at Algebra/FreeAlgebra.lean:369; liftFun (:111) is the underlying map.
  • Module.Free is a class at LinearAlgebra/FreeModule/Basic.lean:43 — distinct from Module.FG (Algebra/Module/Defs.lean).
  • Uncountable is a class (Data/Countable/Defs.lean:125); Set.Finite/Set.Infinite have no standalone def line (cite the file; finite_def theorem at :56).
  • Cardinal.aleph (:417, Aleph.lean); Cardinal.aleph0 (:478, SetTheory/Cardinal/Defs.lean).
  • Spec.structureSheaf def at StructureSheaf.lean:890; structureSheafInType (:171) is the type-level variant.
  • dpow (divided powers) at RingTheory/DividedPowers/SubDPIdeal.lean:554 is the operation for divided-power structures on ideals; the catalogue’s divided-power-algebra Γ notion shares the operation name in a different construction.
  • No Scheme.toTop/underlying_space declaration found; the L207 bundle therefore stays unchecked despite two of three components verifying.
  • The unicode in entry titles (Δ[n], ℵ, ⊣, γ, ℵ₀) round-trips through the file unchanged; checkboxes and citations were the only edits.

Appendix: checked entries