oxilean-std 0.1.2

//! Auto-generated module
//!
//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)

use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};

use super::types::{
    DGAlgebra, GaloisExtensionData, GradedModule, GradedRing, HopfAlgebraData, KoszulComplex,
    KrullDimEstimator, LocalRing, PrimaryDecompositionData,
};

pub fn app(f: Expr, a: Expr) -> Expr {
    Expr::App(Box::new(f), Box::new(a))
}
pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
    app(app(f, a), b)
}
pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
    app(app2(f, a, b), c)
}
pub fn cst(s: &str) -> Expr {
    Expr::Const(Name::str(s), vec![])
}
pub fn prop() -> Expr {
    Expr::Sort(Level::zero())
}
pub fn type0() -> Expr {
    Expr::Sort(Level::succ(Level::zero()))
}
pub fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
    Expr::Pi(bi, Name::str(name), Box::new(dom), Box::new(body))
}
pub fn arrow(a: Expr, b: Expr) -> Expr {
    pi(BinderInfo::Default, "_", a, b)
}
pub fn impl_pi(name: &str, dom: Expr, body: Expr) -> Expr {
    pi(BinderInfo::Implicit, name, dom, body)
}
pub fn bvar(n: u32) -> Expr {
    Expr::BVar(n)
}
pub fn nat_ty() -> Expr {
    cst("Nat")
}
/// `Module R M : Prop`
///
/// An R-module: an abelian group M equipped with a scalar action of ring R
/// satisfying the module axioms.
pub fn module_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("M", type0(), prop()))
}
/// `Algebra R A : Prop`
///
/// An R-algebra: an R-module A that is also a ring, with the scalar action
/// compatible with ring multiplication (r • (a * b) = (r • a) * b).
pub fn algebra_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("A", type0(), prop()))
}
/// `LinearMap R M N : Type`
///
/// An R-linear map f : M →ₗ\[R\] N: a group homomorphism satisfying
/// f(r • m) = r • f(m) for all r : R, m : M.
pub fn linear_map_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("M", type0(), impl_pi("N", type0(), type0())),
    )
}
/// `TensorProduct R M N : Type`
///
/// The tensor product M ⊗\[R\] N of two R-modules, defined as the
/// free R-module on (M × N) quotiented by bilinearity relations.
pub fn tensor_product_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("M", type0(), impl_pi("N", type0(), type0())),
    )
}
/// `ExteriorAlgebra R M : Type`
///
/// The exterior (Grassmann) algebra ∧(M) over R: the quotient of the
/// tensor algebra T(M) by the ideal generated by {m ⊗ m | m ∈ M}.
pub fn exterior_algebra_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("M", type0(), type0()))
}
/// `GradedRing ι R : Prop`
///
/// A ℤ-graded (or ι-graded) ring: a ring R with a decomposition
/// R = ⊕ᵢ Rᵢ such that Rᵢ · Rⱼ ⊆ Rᵢ₊ⱼ.
pub fn graded_ring_ty() -> Expr {
    impl_pi("ι", type0(), impl_pi("R", type0(), prop()))
}
/// `GradedModule ι R M : Prop`
///
/// A graded module M over a graded ring R: M = ⊕ᵢ Mᵢ with
/// Rᵢ · Mⱼ ⊆ Mᵢ₊ⱼ.
pub fn graded_module_ty() -> Expr {
    impl_pi(
        "ι",
        type0(),
        impl_pi("R", type0(), impl_pi("M", type0(), prop())),
    )
}
/// `Derivation R A M : Type`
///
/// An R-derivation from an R-algebra A into an A-module M: an R-linear map
/// d : A → M satisfying the Leibniz rule d(a * b) = a • d(b) + d(a) • b.
pub fn derivation_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("A", type0(), impl_pi("M", type0(), type0())),
    )
}
/// `LieAlgebra R L : Prop`
///
/// A Lie algebra over R: an R-module L equipped with a bilinear bracket
/// \[·,·\] : L × L → L that is antisymmetric and satisfies the Jacobi identity.
pub fn lie_algebra_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("L", type0(), prop()))
}
/// `LieModule R L M : Prop`
///
/// A Lie module: an R-module M with a Lie algebra L acting on M by
/// derivations, i.e., \[x, y\] • m = x • (y • m) - y • (x • m).
pub fn lie_module_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("L", type0(), impl_pi("M", type0(), prop())),
    )
}
/// `LieBracket : ∀ (L : Type), L → L → L`
///
/// The Lie bracket operation \[x, y\] on a Lie algebra L.
pub fn lie_bracket_ty() -> Expr {
    impl_pi("L", type0(), arrow(bvar(0), arrow(bvar(1), bvar(2))))
}
/// `JacobiIdentity : ∀ (R L : Type) \[LieAlgebra R L\] (x y z : L), Prop`
///
/// The Jacobi identity: [x,\[y,z\]] + [y,\[z,x\]] + [z,\[x,y\]] = 0.
pub fn jacobi_identity_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi(
            "L",
            type0(),
            arrow(bvar(0), arrow(bvar(1), arrow(bvar(2), prop()))),
        ),
    )
}
/// `PBWBasis : ∀ (R g : Type) \[LieAlgebra R g\], Prop`
///
/// The Poincaré-Birkhoff-Witt theorem: the universal enveloping algebra
/// U(g) has a basis of ordered monomials in a basis of g.
pub fn pbw_basis_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("g", type0(), prop()))
}
/// `FilteredRing R : Prop`
///
/// A filtered ring: a ring R equipped with a descending filtration
/// R = F₀R ⊇ F₁R ⊇ F₂R ⊇ … such that FᵢR · FⱼR ⊆ Fᵢ₊ⱼR.
pub fn filtered_ring_ty() -> Expr {
    impl_pi("R", type0(), prop())
}
/// `AssociatedGraded R : Type`
///
/// The associated graded ring gr(R) = ⊕ᵢ FᵢR / Fᵢ₊₁R of a filtered ring R.
/// Encodes the passage from filtered to graded structure.
pub fn associated_graded_ty() -> Expr {
    impl_pi("R", type0(), type0())
}
/// `FormalPowerSeries R : Type`
///
/// The formal power series ring R[\[X\]] over R: infinite sums ∑ aₙXⁿ
/// with coefficient-wise addition and Cauchy product multiplication.
pub fn formal_power_series_ty() -> Expr {
    impl_pi("R", type0(), type0())
}
/// `IAdicTopology R I : Prop`
///
/// The I-adic topology on ring R defined by the ideal I: a neighbourhood
/// basis of 0 given by the powers {Iⁿ | n ≥ 0}.
pub fn i_adic_topology_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("I", type0(), prop()))
}
/// `CompleteRing R I : Prop`
///
/// A ring R that is complete with respect to its I-adic topology:
/// every Cauchy sequence in the I-adic metric converges in R.
pub fn complete_ring_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("I", type0(), prop()))
}
/// `ArtinRees R I M : Prop`
///
/// The Artin-Rees lemma: for a Noetherian ring R, ideal I, and
/// finitely generated module M with submodule N, there exists k such that
/// IⁿM ∩ N = Iⁿ⁻ᵏ(IᵏM ∩ N) for all n ≥ k.
pub fn artin_rees_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("I", type0(), impl_pi("M", type0(), prop())),
    )
}
/// `IntegralExtension R S : Prop`
///
/// S is an integral extension of R: every element of S satisfies a monic
/// polynomial with coefficients in R.
pub fn integral_extension_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("S", type0(), prop()))
}
/// `IntegralClosure R S : Type`
///
/// The integral closure of R in S: the subring of S consisting of all
/// elements integral over R.
pub fn integral_closure_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("S", type0(), type0()))
}
/// `IntegrallyClosedDomain R : Prop`
///
/// An integrally closed domain: an integral domain R that equals its own
/// integral closure in its fraction field.
pub fn integrally_closed_domain_ty() -> Expr {
    impl_pi("R", type0(), prop())
}
/// `GoingUp R S : Prop`
///
/// The going-up theorem: if R ⊆ S is an integral extension and P ⊆ Q are
/// primes of R lying under P' of S, then there exists Q' ⊇ P' in S lying
/// over Q.
pub fn going_up_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("S", type0(), prop()))
}
/// `GoingDown R S : Prop`
///
/// The going-down theorem: holds for flat extensions; if P ⊇ Q are primes
/// of R with P' lying over P in S, then there exists Q' ⊆ P' lying over Q.
pub fn going_down_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("S", type0(), prop()))
}
/// `LyingOver R S : Prop`
///
/// The lying-over theorem: for an integral extension R ⊆ S, every prime
/// ideal of R is the contraction of some prime ideal of S.
pub fn lying_over_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("S", type0(), prop()))
}
/// `KrullDimension R : Nat`
///
/// The Krull dimension of ring R: the supremum of lengths of chains of
/// prime ideals p₀ ⊊ p₁ ⊊ … ⊊ pₙ in R.
pub fn krull_dimension_ty() -> Expr {
    impl_pi("R", type0(), nat_ty())
}
/// `IdealHeight R P : Nat`
///
/// The height (rank) of a prime ideal P in ring R: the supremum of lengths
/// of chains of prime ideals contained in P.
pub fn ideal_height_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("P", arrow(bvar(0), prop()), nat_ty()))
}
/// `NoetherianRing R : Prop`
///
/// A Noetherian ring: every ascending chain of ideals I₁ ⊆ I₂ ⊆ … stabilises,
/// equivalently every ideal is finitely generated.
pub fn noetherian_ring_ty() -> Expr {
    impl_pi("R", type0(), prop())
}
/// `ArtinianRing R : Prop`
///
/// An Artinian ring: every descending chain of ideals I₁ ⊇ I₂ ⊇ … stabilises.
/// By Hopkins-Levitzki, Artinian rings are also Noetherian.
pub fn artinian_ring_ty() -> Expr {
    impl_pi("R", type0(), prop())
}
/// `HopkinsLevitzki R : Prop`
///
/// The Hopkins-Levitzki theorem: a ring R is Artinian if and only if
/// it is Noetherian and has Krull dimension 0.
pub fn hopkins_levitzki_ty() -> Expr {
    impl_pi("R", type0(), prop())
}
/// `PrimaryIdeal R Q : Prop`
///
/// Q is a primary ideal of R: whenever xy ∈ Q, either x ∈ Q or
/// yⁿ ∈ Q for some n ≥ 1 (i.e., y ∈ √Q).
pub fn primary_ideal_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("Q", arrow(bvar(0), prop()), prop()))
}
/// `PrimaryDecomposition R I : Prop`
///
/// I has a primary decomposition: I = Q₁ ∩ Q₂ ∩ … ∩ Qₙ where each Qᵢ
/// is a primary ideal. (Lasker-Noether: holds when R is Noetherian.)
pub fn primary_decomposition_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("I", arrow(bvar(0), prop()), prop()))
}
/// `LaskerNoether R : Prop`
///
/// The Lasker-Noether theorem: every ideal in a Noetherian ring R admits
/// a primary decomposition.
pub fn lasker_noether_ty() -> Expr {
    impl_pi("R", type0(), prop())
}
/// `AssociatedPrimes R M : Type`
///
/// The set of associated primes Ass(M) of an R-module M: the set of prime
/// ideals P of R such that P = Ann(m) for some m ∈ M.
pub fn associated_primes_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("M", type0(), type0()))
}
/// `Localization R S : Type`
///
/// The localization S⁻¹R of a ring R at a multiplicative subset S:
/// equivalence classes of fractions r/s with r ∈ R, s ∈ S.
pub fn localization_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("S", arrow(bvar(0), prop()), type0()))
}
/// `LocalizationModule R S M : Type`
///
/// The localisation S⁻¹M of an R-module M at multiplicative set S.
pub fn localization_module_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("M", type0(), impl_pi("S", arrow(bvar(1), prop()), type0())),
    )
}
/// `NakayamasLemma R M I : Prop`
///
/// Nakayama's lemma: if M is a finitely generated R-module, I ⊆ J(R)
/// (Jacobson radical), and IM = M, then M = 0.
pub fn nakayamas_lemma_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("M", type0(), impl_pi("I", arrow(bvar(1), prop()), prop())),
    )
}
/// `CohenMacaulay R : Prop`
///
/// A Cohen-Macaulay ring: a Noetherian ring R in which depth(M,R) = dim(R)
/// for every maximal ideal M (equivalently, every system of parameters is
/// a regular sequence).
pub fn cohen_macaulay_ty() -> Expr {
    impl_pi("R", type0(), prop())
}
/// `RegularLocalRing R : Prop`
///
/// A regular local ring: a Noetherian local ring (R, m) whose embedding
/// dimension equals its Krull dimension (μ(m) = dim R).
pub fn regular_local_ring_ty() -> Expr {
    impl_pi("R", type0(), prop())
}
/// `RegularSequence R M seq : Prop`
///
/// A regular sequence on an R-module M: a sequence x₁,…,xₙ ∈ R such that
/// x₁ is a non-zero-divisor on M, and each xᵢ is a non-zero-divisor on
/// M/(x₁,…,xᵢ₋₁)M.
pub fn regular_sequence_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi(
            "M",
            type0(),
            impl_pi("seq", app(cst("List"), bvar(1)), prop()),
        ),
    )
}
/// `ModuleDepth R M I : Nat`
///
/// The I-depth of an R-module M: the length of a maximal M-regular sequence
/// in the ideal I, equal to the infimum of i such that Extⁱ_R(R/I, M) ≠ 0.
pub fn module_depth_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("M", type0(), impl_pi("I", arrow(bvar(1), prop()), nat_ty())),
    )
}
/// `ProjectiveDimension R M : Nat`
///
/// The projective dimension pd(M) of an R-module M: the minimum length
/// of a projective resolution 0 → Pₙ → … → P₀ → M → 0.
pub fn projective_dimension_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("M", type0(), nat_ty()))
}
/// `AuslanderBuchsbaum R M : Prop`
///
/// The Auslander-Buchsbaum formula: for a finitely generated R-module M
/// over a regular local ring R with pd(M) < ∞,
/// pd(M) + depth(M) = depth(R).
pub fn auslander_buchsbaum_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("M", type0(), prop()))
}
/// `GorensteinRing R : Prop`
///
/// A Gorenstein ring: a Noetherian ring R that has finite injective dimension
/// as a module over itself. Equivalent to: R is Cohen-Macaulay and the
/// canonical module is isomorphic to R.
pub fn gorenstein_ring_ty() -> Expr {
    impl_pi("R", type0(), prop())
}
/// `GradedMorphism ι R S : Prop`
///
/// A graded ring homomorphism f : R → S of ι-graded rings: a ring
/// homomorphism preserving degrees, i.e., f(Rᵢ) ⊆ Sᵢ for all i.
pub fn graded_morphism_ty() -> Expr {
    impl_pi(
        "ι",
        type0(),
        impl_pi("R", type0(), impl_pi("S", type0(), prop())),
    )
}
/// `HomogeneousIdeal ι R I : Prop`
///
/// A homogeneous ideal of a graded ring R: an ideal I that is generated
/// by homogeneous elements, equivalently I = ⊕ᵢ (I ∩ Rᵢ).
pub fn homogeneous_ideal_ty() -> Expr {
    impl_pi(
        "ι",
        type0(),
        impl_pi("R", type0(), impl_pi("I", arrow(bvar(0), prop()), prop())),
    )
}
/// `HilbertFunction ι R : Nat → Nat`
///
/// The Hilbert function of a graded R-module M: H(n) = rank of the n-th
/// homogeneous component Mₙ as a free module over R₀.
pub fn hilbert_function_ty() -> Expr {
    impl_pi(
        "ι",
        type0(),
        impl_pi("R", type0(), arrow(nat_ty(), nat_ty())),
    )
}
/// `JacobsonRadical R : Type`
///
/// The Jacobson radical J(R) of ring R: the intersection of all maximal
/// left ideals, equivalently {r ∈ R | 1 - rs is a unit for all s ∈ R}.
pub fn jacobson_radical_ty() -> Expr {
    impl_pi("R", type0(), type0())
}
/// `NilRadical R : Type`
///
/// The nilradical √0 of ring R: the ideal of nilpotent elements,
/// equal to the intersection of all prime ideals of R.
pub fn nil_radical_ty() -> Expr {
    impl_pi("R", type0(), type0())
}
/// `SymmetricAlgebra R M : Type`
///
/// The symmetric algebra Sym(M) over R: the quotient of the tensor algebra
/// T(M) by the ideal generated by {m ⊗ n - n ⊗ m | m, n ∈ M}.
pub fn symmetric_algebra_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("M", type0(), type0()))
}
/// `DividedPowerAlgebra R M : Type`
///
/// The divided power algebra Γ(M) over R: the free R-module with basis
/// {γₙ(m)} satisfying divided-power relations, dual to the symmetric algebra.
pub fn divided_power_algebra_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("M", type0(), type0()))
}
/// `Bialgebra R H : Prop`
///
/// A bialgebra: an R-algebra H equipped with compatible comultiplication
/// Δ : H → H ⊗ H and counit ε : H → R making H simultaneously an algebra
/// and a coalgebra, with Δ and ε being algebra homomorphisms.
pub fn bialgebra_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("H", type0(), prop()))
}
/// `HopfAlgebra R H : Prop`
///
/// A Hopf algebra: a bialgebra H equipped with an antipode map
/// S : H → H satisfying the antipode axioms m(S ⊗ id)Δ = ηε = m(id ⊗ S)Δ.
pub fn hopf_algebra_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("H", type0(), prop()))
}
/// `Antipode R H : H → H`
///
/// The antipode of a Hopf algebra: the unique anti-automorphism S : H → H
/// satisfying the Hopf algebra axioms, analogous to group inversion.
pub fn antipode_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("H", type0(), arrow(bvar(0), bvar(1))))
}
/// `Comultiplication R H : H → H ⊗ H`
///
/// The comultiplication (coproduct) map Δ : H → H ⊗ H of a coalgebra,
/// satisfying coassociativity: (Δ ⊗ id)Δ = (id ⊗ Δ)Δ.
pub fn comultiplication_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi(
            "H",
            type0(),
            arrow(
                bvar(0),
                app3(cst("TensorProduct"), bvar(1), bvar(1), bvar(1)),
            ),
        ),
    )
}
/// `Comodule R H M : Prop`
///
/// An H-comodule: an R-module M equipped with a coaction ρ : M → H ⊗ M
/// satisfying comodule axioms (coassociativity and counit).
pub fn comodule_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("H", type0(), impl_pi("M", type0(), prop())),
    )
}
/// `CoalgebraMap R C D : Prop`
///
/// A coalgebra homomorphism f : C → D: a map preserving comultiplication
/// and counit, i.e., (f ⊗ f)Δ_C = Δ_D f and ε_D f = ε_C.
pub fn coalgebra_map_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("C", type0(), impl_pi("D", type0(), prop())),
    )
}
/// `MoritaEquivalent R S : Prop`
///
/// Two rings R and S are Morita equivalent: the categories R-Mod and S-Mod
/// are equivalent as abelian categories. This holds iff S ≅ Mₙ(R) for some n,
/// or equivalently S is a full matrix ring over R.
pub fn morita_equivalent_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("S", type0(), prop()))
}
/// `DerivedMoritaEquivalent R S : Prop`
///
/// Derived Morita equivalence: the derived categories D(R-Mod) and D(S-Mod)
/// are equivalent as triangulated categories.
pub fn derived_morita_equivalent_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("S", type0(), prop()))
}
/// `TiltingModule R T : Prop`
///
/// A tilting module: a finitely generated R-module T with pd(T) ≤ 1,
/// Ext¹(T,T) = 0, and every projective R-module is a direct summand of
/// a finite direct sum of copies of T.
pub fn tilting_module_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("T", type0(), prop()))
}
/// `ProgressiveEquivalence R S : Prop`
///
/// The Morita context: a six-tuple (R, S, P, Q, θ, φ) witnessing a Morita
/// equivalence, where P is an R-S-bimodule and Q is an S-R-bimodule.
pub fn morita_context_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("S", type0(), prop()))
}
/// `OreExtension R σ δ : Type`
///
/// The Ore extension (skew polynomial ring) R\[x; σ, δ\]: the free left
/// R-module with basis {xⁿ} and multiplication xa = σ(a)x + δ(a),
/// where σ is an endomorphism and δ a σ-derivation of R.
pub fn ore_extension_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi(
            "σ",
            arrow(bvar(0), bvar(1)),
            impl_pi("δ", arrow(bvar(1), bvar(2)), type0()),
        ),
    )
}
/// `SkewPolynomialRing R σ : Type`
///
/// The skew polynomial ring R\[x; σ\]: Ore extension with δ = 0.
/// Multiplication satisfies xa = σ(a)x for all a ∈ R.
pub fn skew_polynomial_ring_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("σ", arrow(bvar(0), bvar(1)), type0()))
}
/// `OreCondition R S : Prop`
///
/// The Ore condition: a multiplicative set S satisfies the left Ore condition
/// if for every r ∈ R, s ∈ S there exist r' ∈ R, s' ∈ S with s'r = r's.
pub fn ore_condition_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("S", arrow(bvar(0), prop()), prop()))
}
/// `WeylAlgebra R n : Type`
///
/// The n-th Weyl algebra Aₙ(R): the R-algebra generated by x₁,…,xₙ,∂₁,…,∂ₙ
/// with relations \[∂ᵢ, xⱼ\] = δᵢⱼ and all other generators commuting.
pub fn weyl_algebra_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("n", nat_ty(), type0()))
}
/// `HilbertSeries ι R : Type`
///
/// The Hilbert series of a graded R-module: a formal power series H(t) = Σ hₙtⁿ
/// where hₙ = rank(Mₙ). Encodes the growth of the module dimensions.
pub fn hilbert_series_ty() -> Expr {
    impl_pi("ι", type0(), impl_pi("R", type0(), type0()))
}
/// `CastelnuovoMumfordRegularity R M : Nat`
///
/// The Castelnuovo-Mumford regularity reg(M) of a graded module M over R:
/// the minimum integer r such that the i-th syzygy of M is generated in
/// degrees ≤ r + i.
pub fn castelnuovo_mumford_regularity_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("M", type0(), nat_ty()))
}
/// `GradedFreeResolution R M : Prop`
///
/// A graded free resolution of a graded R-module M: an exact complex
/// 0 → Fₙ → … → F₁ → F₀ → M → 0 of graded free R-modules.
pub fn graded_free_resolution_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("M", type0(), prop()))
}
/// `GlobalDimension R : Nat`
///
/// The global (homological) dimension gl.dim(R): the supremum of projective
/// dimensions of all R-modules, equal to the minimum length of a projective
/// resolution over all R-modules.
pub fn global_dimension_ty() -> Expr {
    impl_pi("R", type0(), nat_ty())
}
/// `InjectiveDimension R M : Nat`
///
/// The injective dimension id(M) of an R-module M: the minimum length of
/// an injective resolution 0 → M → I₀ → I₁ → … → Iₙ → 0.
pub fn injective_dimension_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("M", type0(), nat_ty()))
}
/// `FlatDimension R M : Nat`
///
/// The flat dimension fd(M) of an R-module M: the minimum length of a flat
/// resolution. Always fd(M) ≤ pd(M), with equality when R is Noetherian.
pub fn flat_dimension_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("M", type0(), nat_ty()))
}
/// `WeakGlobalDimension R : Nat`
///
/// The weak (finitistic) global dimension w.gl.dim(R): the supremum of flat
/// dimensions of all R-modules. For Noetherian rings equals the global dimension.
pub fn weak_global_dimension_ty() -> Expr {
    impl_pi("R", type0(), nat_ty())
}
/// `GaloisExtension K L : Prop`
///
/// A Galois extension: a field extension L/K that is both normal (every
/// irreducible polynomial over K splits completely in L) and separable.
pub fn galois_extension_ty() -> Expr {
    impl_pi("K", type0(), impl_pi("L", type0(), prop()))
}
/// `GaloisGroup K L : Type`
///
/// The Galois group Gal(L/K): the group of field automorphisms of L that fix
/// K pointwise, whose order equals \[L:K\] for a Galois extension.
pub fn galois_group_ty() -> Expr {
    impl_pi("K", type0(), impl_pi("L", type0(), type0()))
}
/// `FundamentalTheoremGalois K L : Prop`
///
/// The fundamental theorem of Galois theory: there is an order-reversing
/// bijection between subgroups of Gal(L/K) and intermediate fields K ⊆ E ⊆ L.
pub fn fundamental_theorem_galois_ty() -> Expr {
    impl_pi("K", type0(), impl_pi("L", type0(), prop()))
}
/// `SolvableExtension K L : Prop`
///
/// A solvable extension: L/K is solvable by radicals iff Gal(L/K) is a
/// solvable group (has a subnormal series with abelian quotients).
pub fn solvable_extension_ty() -> Expr {
    impl_pi("K", type0(), impl_pi("L", type0(), prop()))
}
/// `SeparableExtension K L : Prop`
///
/// A separable extension: every element of L is algebraic over K with a
/// separable (squarefree) minimal polynomial over K.
pub fn separable_extension_ty() -> Expr {
    impl_pi("K", type0(), impl_pi("L", type0(), prop()))
}
/// `CentralSimpleAlgebra K A : Prop`
///
/// A central simple algebra over a field K: a finite-dimensional K-algebra A
/// with centre Z(A) = K and no non-trivial two-sided ideals.
pub fn central_simple_algebra_ty() -> Expr {
    impl_pi("K", type0(), impl_pi("A", type0(), prop()))
}
/// `BrauerGroup K : Type`
///
/// The Brauer group Br(K) of a field K: the group of Morita equivalence
/// classes of central simple K-algebras, with tensor product as group operation.
pub fn brauer_group_ty() -> Expr {
    impl_pi("K", type0(), type0())
}
/// `WedderburnTheorem A : Prop`
///
/// Wedderburn's theorem: every finite simple ring (division ring) is a matrix
/// ring over a division algebra; equivalently, every finite division ring is
/// a field.
pub fn wedderburn_theorem_ty() -> Expr {
    impl_pi("A", type0(), prop())
}
/// `ArtinWedderburn R : Prop`
///
/// The Artin-Wedderburn theorem: a semisimple ring R is isomorphic to a
/// direct product ∏ Mₙᵢ(Dᵢ) of matrix rings over division rings Dᵢ.
pub fn artin_wedderburn_ty() -> Expr {
    impl_pi("R", type0(), prop())
}
/// `SchurLemma R M N : Prop`
///
/// Schur's lemma: any non-zero homomorphism between simple R-modules M and N
/// is an isomorphism; End_R(M) is a division ring for a simple module M.
pub fn schur_lemma_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("M", type0(), impl_pi("N", type0(), prop())),
    )
}
/// `WittVectors R : Type`
///
/// The ring of Witt vectors W(R): for a ring R, W(R) = Rᴺ as a set with
/// addition and multiplication given by universal polynomials (Witt polynomials).
pub fn witt_vectors_ty() -> Expr {
    impl_pi("R", type0(), type0())
}
/// `LambdaRing R : Prop`
///
/// A lambda-ring (or special λ-ring): a commutative ring R equipped with
/// operations λⁿ : R → R for n ≥ 0 satisfying the axioms analogous to
/// exterior power operations in representation theory.
pub fn lambda_ring_ty() -> Expr {
    impl_pi("R", type0(), prop())
}
/// `TeichmullerLift R p : Prop`
///
/// The Teichmüller lift: the unique multiplicative section of the projection
/// W(R) → R, sending elements of R to their representatives in W(R).
pub fn teichmuller_lift_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("p", nat_ty(), prop()))
}
/// `OrderedGroup G : Prop`
///
/// A totally ordered group: a group G equipped with a total order ≤ compatible
/// with the group operation: a ≤ b implies ca ≤ cb and ac ≤ bc.
pub fn ordered_group_ty() -> Expr {
    impl_pi("G", type0(), prop())
}
/// `LatticeOrderedRing R : Prop`
///
/// A lattice-ordered ring (l-ring): a ring R that is also a lattice with
/// the compatibility condition: 0 ≤ a and 0 ≤ b implies 0 ≤ ab.
pub fn lattice_ordered_ring_ty() -> Expr {
    impl_pi("R", type0(), prop())
}
/// `ValuedField K Γ : Prop`
///
/// A valued field: a field K with a non-archimedean valuation v : K → Γ ∪ {∞}
/// where Γ is an ordered abelian group, satisfying v(xy) = v(x) + v(y) and
/// v(x + y) ≥ min(v(x), v(y)).
pub fn valued_field_ty() -> Expr {
    impl_pi("K", type0(), impl_pi("Γ", type0(), prop()))
}
/// `DifferentialGradedAlgebra R A : Prop`
///
/// A differential graded algebra (dgA): a graded R-algebra A* equipped with
/// a differential d : Aⁿ → Aⁿ⁺¹ satisfying d² = 0 and the graded Leibniz rule
/// d(a·b) = d(a)·b + (-1)^|a| a·d(b).
pub fn differential_graded_algebra_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("A", type0(), prop()))
}
/// `AInfinityAlgebra R A : Prop`
///
/// An A∞-algebra: a graded R-module A with a sequence of operations
/// mₙ : A^⊗n → A of degree 2-n satisfying the A∞-relations (Stasheff identities),
/// generalising associativity up to coherent homotopy.
pub fn a_infinity_algebra_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("A", type0(), prop()))
}
/// `DGModule R A M : Prop`
///
/// A differential graded module over a dgA: a chain complex M over R with a
/// graded A-module structure compatible with the differentials of A and M.
pub fn dg_module_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("A", type0(), impl_pi("M", type0(), prop())),
    )
}
/// `QuasiIsomorphism R A B : Prop`
///
/// A quasi-isomorphism: a chain map f : A → B of dgAs (or dg-modules) that
/// induces isomorphisms on all cohomology groups Hⁿ(f) : Hⁿ(A) → Hⁿ(B).
pub fn quasi_isomorphism_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("A", type0(), impl_pi("B", type0(), prop())),
    )
}
/// `Operad R P : Prop`
///
/// A (symmetric) operad in R-modules: a collection P(n) of R-modules for n ≥ 0
/// with composition maps γ : P(k) ⊗ P(n₁) ⊗ … ⊗ P(nₖ) → P(n₁+…+nₖ)
/// satisfying associativity, unity, and equivariance axioms.
pub fn operad_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("P", type0(), prop()))
}
/// `OperadAlgebra R P A : Prop`
///
/// A P-algebra: an R-module A with a morphism of operads γ_A : P → End_A,
/// where End_A(n) = Hom_R(A^⊗n, A) is the endomorphism operad.
pub fn operad_algebra_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("P", type0(), impl_pi("A", type0(), prop())),
    )
}
/// `CyclicOperad R P : Prop`
///
/// A cyclic operad: an operad P equipped with additional Sₙ₊₁-equivariance
/// that extends the Sₙ-action, analogous to cyclic (Connes) homology.
pub fn cyclic_operad_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("P", type0(), prop()))
}
/// `Associahedron n : Type`
///
/// The Stasheff associahedron Kₙ: the (n-2)-dimensional polytope whose faces
/// correspond to ways of bracketing a product of n items. Governs A∞-algebras.
pub fn associahedron_ty() -> Expr {
    impl_pi("n", nat_ty(), type0())
}
/// `BoundedDerivedCategory R : Type`
///
/// The bounded derived category D^b(R-Mod): the localisation of the category
/// of bounded chain complexes of R-modules at quasi-isomorphisms.
pub fn bounded_derived_category_ty() -> Expr {
    impl_pi("R", type0(), type0())
}
/// `TStructure R D : Prop`
///
/// A t-structure on a triangulated category D: a pair of full subcategories
/// (D≤0, D≥0) satisfying three axioms relating them via the shift functor \[1\].
pub fn t_structure_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("D", type0(), prop()))
}
/// `KoszulDuality R A B : Prop`
///
/// Koszul duality: two quadratic algebras A and A! are Koszul duals to each
/// other, with D^b(A-Mod) ≃ D^b(A!-Mod) (the Beilinson-Ginzburg-Soergel theorem).
pub fn koszul_duality_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("A", type0(), impl_pi("B", type0(), prop())),
    )
}
/// `KoszulAlgebra R A : Prop`
///
/// A Koszul algebra: a graded algebra A = ⊕ Aₙ that is Koszul as a module
/// over A₀, meaning the Koszul complex resolves A₀ as an A-module.
pub fn koszul_algebra_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("A", type0(), prop()))
}
/// `KoszulResolution R A : Type`
///
/// The Koszul resolution of a Koszul algebra A: the minimal free resolution
/// of the trivial A-module given by the Koszul complex K(A).
pub fn koszul_resolution_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("A", type0(), type0()))
}
/// `DerivedFunctor R F : Type`
///
/// A derived functor: the total derived functor RF (or LF) of an additive
/// functor F : R-Mod → S-Mod, defined on the derived category D(R-Mod).
pub fn derived_functor_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("F", type0(), type0()))
}
/// `VertexAlgebra R V : Prop`
///
/// A vertex algebra: an R-module V with a distinguished vacuum vector |0⟩,
/// a translation operator T, and a state-field correspondence
/// Y : V → End(V)[\[z, z⁻¹\]] satisfying locality, translation covariance, and
/// vacuum axioms.
pub fn vertex_algebra_ty() -> Expr {
    impl_pi("R", type0(), impl_pi("V", type0(), prop()))
}
/// `ConformalVertex R V c : Prop`
///
/// A conformal vertex algebra of central charge c: a vertex algebra V with a
/// distinguished conformal vector ω ∈ V₂ whose modes Lₙ = ω_(n+1) satisfy the
/// Virasoro algebra with central charge c.
pub fn conformal_vertex_ty() -> Expr {
    impl_pi(
        "R",
        type0(),
        impl_pi("V", type0(), impl_pi("c", type0(), prop())),
    )
}
/// `PrimeSpectrum R : Type`
///
/// The prime spectrum Spec(R): the set of all prime ideals of R, equipped with
/// the Zariski topology where closed sets are V(I) = {p prime | I ⊆ p}.
pub fn prime_spectrum_ty() -> Expr {
    impl_pi("R", type0(), type0())
}
/// `MaximalSpectrum R : Type`
///
/// The maximal spectrum mSpec(R): the subset of Spec(R) consisting of all
/// maximal ideals, corresponding to points of the affine variety.
pub fn maximal_spectrum_ty() -> Expr {
    impl_pi("R", type0(), type0())
}
/// `ZariskiTopology R : Prop`
///
/// The Zariski topology on Spec(R): a topology where the closed sets are
/// the sets V(I) for ideals I ⊆ R, and the basic open sets are D(f) = {p | f ∉ p}.
pub fn zariski_topology_ty() -> Expr {
    impl_pi("R", type0(), prop())
}
/// `StructureSheaf R : Type`
///
/// The structure sheaf O_X on X = Spec(R): the sheaf of rings on Spec(R)
/// with O_X(D(f)) = Rᶠ (the localisation of R at {1, f, f², …}).
pub fn structure_sheaf_ty() -> Expr {
    impl_pi("R", type0(), type0())
}
/// Register all advanced abstract algebra axioms into the given kernel environment.
pub fn register_abstract_algebra_adv(env: &mut Environment) {
    let axioms: &[(&str, Expr)] = &[
        ("Module", module_ty()),
        ("Algebra", algebra_ty()),
        ("LinearMap", linear_map_ty()),
        ("TensorProduct", tensor_product_ty()),
        ("ExteriorAlgebra", exterior_algebra_ty()),
        ("GradedRing", graded_ring_ty()),
        ("GradedModule", graded_module_ty()),
        ("Derivation", derivation_ty()),
        ("LieAlgebra", lie_algebra_ty()),
        ("LieModule", lie_module_ty()),
        ("LieBracket", lie_bracket_ty()),
        ("JacobiIdentity", jacobi_identity_ty()),
        ("PBWBasis", pbw_basis_ty()),
        ("FilteredRing", filtered_ring_ty()),
        ("AssociatedGraded", associated_graded_ty()),
        ("FormalPowerSeries", formal_power_series_ty()),
        ("IAdicTopology", i_adic_topology_ty()),
        ("CompleteRing", complete_ring_ty()),
        ("ArtinRees", artin_rees_ty()),
        ("IntegralExtension", integral_extension_ty()),
        ("IntegralClosure", integral_closure_ty()),
        ("IntegrallyClosedDomain", integrally_closed_domain_ty()),
        ("GoingUp", going_up_ty()),
        ("GoingDown", going_down_ty()),
        ("LyingOver", lying_over_ty()),
        ("KrullDimension", krull_dimension_ty()),
        ("IdealHeight", ideal_height_ty()),
        ("NoetherianRing", noetherian_ring_ty()),
        ("ArtinianRing", artinian_ring_ty()),
        ("HopkinsLevitzki", hopkins_levitzki_ty()),
        ("PrimaryIdeal", primary_ideal_ty()),
        ("PrimaryDecomposition", primary_decomposition_ty()),
        ("LaskerNoether", lasker_noether_ty()),
        ("AssociatedPrimes", associated_primes_ty()),
        ("Localization", localization_ty()),
        ("LocalizationModule", localization_module_ty()),
        ("NakayamasLemma", nakayamas_lemma_ty()),
        ("CohenMacaulay", cohen_macaulay_ty()),
        ("RegularLocalRing", regular_local_ring_ty()),
        ("RegularSequence", regular_sequence_ty()),
        ("ModuleDepth", module_depth_ty()),
        ("ProjectiveDimension", projective_dimension_ty()),
        ("AuslanderBuchsbaum", auslander_buchsbaum_ty()),
        ("GorensteinRing", gorenstein_ring_ty()),
        ("GradedMorphism", graded_morphism_ty()),
        ("HomogeneousIdeal", homogeneous_ideal_ty()),
        ("HilbertFunction", hilbert_function_ty()),
        ("JacobsonRadical", jacobson_radical_ty()),
        ("NilRadical", nil_radical_ty()),
        ("SymmetricAlgebra", symmetric_algebra_ty()),
        ("DividedPowerAlgebra", divided_power_algebra_ty()),
        ("Bialgebra", bialgebra_ty()),
        ("HopfAlgebra", hopf_algebra_ty()),
        ("Antipode", antipode_ty()),
        ("Comultiplication", comultiplication_ty()),
        ("Comodule", comodule_ty()),
        ("CoalgebraMap", coalgebra_map_ty()),
        ("MoritaEquivalent", morita_equivalent_ty()),
        ("DerivedMoritaEquivalent", derived_morita_equivalent_ty()),
        ("TiltingModule", tilting_module_ty()),
        ("MoritaContext", morita_context_ty()),
        ("OreExtension", ore_extension_ty()),
        ("SkewPolynomialRing", skew_polynomial_ring_ty()),
        ("OreCondition", ore_condition_ty()),
        ("WeylAlgebra", weyl_algebra_ty()),
        ("HilbertSeries", hilbert_series_ty()),
        (
            "CastelnuovoMumfordRegularity",
            castelnuovo_mumford_regularity_ty(),
        ),
        ("GradedFreeResolution", graded_free_resolution_ty()),
        ("GlobalDimension", global_dimension_ty()),
        ("InjectiveDimension", injective_dimension_ty()),
        ("FlatDimension", flat_dimension_ty()),
        ("WeakGlobalDimension", weak_global_dimension_ty()),
        ("GaloisExtension", galois_extension_ty()),
        ("GaloisGroup", galois_group_ty()),
        ("FundamentalTheoremGalois", fundamental_theorem_galois_ty()),
        ("SolvableExtension", solvable_extension_ty()),
        ("SeparableExtension", separable_extension_ty()),
        ("CentralSimpleAlgebra", central_simple_algebra_ty()),
        ("BrauerGroup", brauer_group_ty()),
        ("WedderburnTheorem", wedderburn_theorem_ty()),
        ("ArtinWedderburn", artin_wedderburn_ty()),
        ("SchurLemma", schur_lemma_ty()),
        ("WittVectors", witt_vectors_ty()),
        ("LambdaRing", lambda_ring_ty()),
        ("TeichmullerLift", teichmuller_lift_ty()),
        ("OrderedGroup", ordered_group_ty()),
        ("LatticeOrderedRing", lattice_ordered_ring_ty()),
        ("ValuedField", valued_field_ty()),
        (
            "DifferentialGradedAlgebra",
            differential_graded_algebra_ty(),
        ),
        ("AInfinityAlgebra", a_infinity_algebra_ty()),
        ("DGModule", dg_module_ty()),
        ("QuasiIsomorphism", quasi_isomorphism_ty()),
        ("Operad", operad_ty()),
        ("OperadAlgebra", operad_algebra_ty()),
        ("CyclicOperad", cyclic_operad_ty()),
        ("Associahedron", associahedron_ty()),
        ("BoundedDerivedCategory", bounded_derived_category_ty()),
        ("TStructure", t_structure_ty()),
        ("KoszulDuality", koszul_duality_ty()),
        ("KoszulAlgebra", koszul_algebra_ty()),
        ("KoszulResolution", koszul_resolution_ty()),
        ("DerivedFunctor", derived_functor_ty()),
        ("VertexAlgebra", vertex_algebra_ty()),
        ("ConformalVertex", conformal_vertex_ty()),
        ("PrimeSpectrum", prime_spectrum_ty()),
        ("MaximalSpectrum", maximal_spectrum_ty()),
        ("ZariskiTopology", zariski_topology_ty()),
        ("StructureSheaf", structure_sheaf_ty()),
    ];
    for (name, ty) in axioms {
        env.add(Declaration::Axiom {
            name: Name::str(*name),
            univ_params: vec![],
            ty: ty.clone(),
        })
        .ok();
    }
}
#[cfg(test)]
mod tests {
    use super::*;
    fn registered_env() -> Environment {
        let mut env = Environment::new();
        register_abstract_algebra_adv(&mut env);
        env
    }
    #[test]
    fn test_module_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("Module")).is_some());
    }
    #[test]
    fn test_algebra_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("Algebra")).is_some());
    }
    #[test]
    fn test_linear_map_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("LinearMap")).is_some());
    }
    #[test]
    fn test_tensor_product_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("TensorProduct")).is_some());
    }
    #[test]
    fn test_exterior_algebra_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("ExteriorAlgebra")).is_some());
    }
    #[test]
    fn test_lie_algebra_and_bracket_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("LieAlgebra")).is_some());
        assert!(env.get(&Name::str("LieBracket")).is_some());
    }
    #[test]
    fn test_jacobi_identity_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("JacobiIdentity")).is_some());
    }
    #[test]
    fn test_pbw_basis_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("PBWBasis")).is_some());
    }
    #[test]
    fn test_filtered_ring_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("FilteredRing")).is_some());
    }
    #[test]
    fn test_associated_graded_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("AssociatedGraded")).is_some());
    }
    #[test]
    fn test_formal_power_series_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("FormalPowerSeries")).is_some());
    }
    #[test]
    fn test_i_adic_topology_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("IAdicTopology")).is_some());
    }
    #[test]
    fn test_complete_ring_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("CompleteRing")).is_some());
    }
    #[test]
    fn test_artin_rees_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("ArtinRees")).is_some());
    }
    #[test]
    fn test_integral_extension_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("IntegralExtension")).is_some());
    }
    #[test]
    fn test_integral_closure_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("IntegralClosure")).is_some());
    }
    #[test]
    fn test_integrally_closed_domain_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("IntegrallyClosedDomain")).is_some());
    }
    #[test]
    fn test_going_up_down_lying_over_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("GoingUp")).is_some());
        assert!(env.get(&Name::str("GoingDown")).is_some());
        assert!(env.get(&Name::str("LyingOver")).is_some());
    }
    #[test]
    fn test_krull_dim_and_height_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("KrullDimension")).is_some());
        assert!(env.get(&Name::str("IdealHeight")).is_some());
    }
    #[test]
    fn test_noetherian_artinian_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("NoetherianRing")).is_some());
        assert!(env.get(&Name::str("ArtinianRing")).is_some());
        assert!(env.get(&Name::str("HopkinsLevitzki")).is_some());
    }
    #[test]
    fn test_primary_decomposition_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("PrimaryIdeal")).is_some());
        assert!(env.get(&Name::str("PrimaryDecomposition")).is_some());
        assert!(env.get(&Name::str("LaskerNoether")).is_some());
        assert!(env.get(&Name::str("AssociatedPrimes")).is_some());
    }
    #[test]
    fn test_localization_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("Localization")).is_some());
        assert!(env.get(&Name::str("LocalizationModule")).is_some());
    }
    #[test]
    fn test_nakayamas_lemma_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("NakayamasLemma")).is_some());
    }
    #[test]
    fn test_cohen_macaulay_and_regular_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("CohenMacaulay")).is_some());
        assert!(env.get(&Name::str("RegularLocalRing")).is_some());
        assert!(env.get(&Name::str("RegularSequence")).is_some());
        assert!(env.get(&Name::str("ModuleDepth")).is_some());
    }
    #[test]
    fn test_auslander_buchsbaum_gorenstein_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("ProjectiveDimension")).is_some());
        assert!(env.get(&Name::str("AuslanderBuchsbaum")).is_some());
        assert!(env.get(&Name::str("GorensteinRing")).is_some());
    }
    #[test]
    fn test_graded_morphism_and_homogeneous_ideal_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("GradedMorphism")).is_some());
        assert!(env.get(&Name::str("HomogeneousIdeal")).is_some());
        assert!(env.get(&Name::str("HilbertFunction")).is_some());
    }
    #[test]
    fn test_radicals_and_algebras_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("JacobsonRadical")).is_some());
        assert!(env.get(&Name::str("NilRadical")).is_some());
        assert!(env.get(&Name::str("SymmetricAlgebra")).is_some());
        assert!(env.get(&Name::str("DividedPowerAlgebra")).is_some());
    }
    #[test]
    fn test_graded_ring_basic() {
        let mut gr = GradedRing::new("k");
        gr.add_generator(0, "1");
        gr.add_generator(1, "x");
        gr.add_generator(1, "y");
        gr.add_generator(2, "x^2");
        gr.add_generator(2, "xy");
        gr.add_generator(2, "y^2");
        assert_eq!(gr.component_rank(0), 1);
        assert_eq!(gr.component_rank(1), 2);
        assert_eq!(gr.component_rank(2), 3);
        assert_eq!(gr.component_rank(3), 0);
        assert!(gr.is_standard_graded());
        let degrees = gr.degrees();
        assert_eq!(degrees, vec![0, 1, 2]);
    }
    #[test]
    fn test_graded_ring_non_standard() {
        let mut gr = GradedRing::new("Z");
        gr.add_generator(-1, "t_inv");
        gr.add_generator(0, "1");
        gr.add_generator(1, "t");
        assert!(!gr.is_standard_graded());
    }
    #[test]
    fn test_local_ring_regular() {
        let lr = LocalRing::new("k[[x,y]]", vec!["x".to_string(), "y".to_string()], "k")
            .with_krull_dim(2);
        assert!(lr.is_regular());
        assert_eq!(lr.embedding_dimension(), 2);
        assert!(lr.is_in_maximal_ideal("x"));
        assert!(!lr.is_in_maximal_ideal("1"));
    }
    #[test]
    fn test_local_ring_non_regular() {
        let lr = LocalRing::new("k[[x,y]]/(xy)", vec!["x".to_string(), "y".to_string()], "k")
            .with_krull_dim(1);
        assert!(!lr.is_regular());
    }
    #[test]
    fn test_primary_decomposition_data() {
        let mut pd = PrimaryDecompositionData::new(2, vec!["x^2".to_string(), "y".to_string()]);
        pd.add_component(vec!["x^2".to_string()], vec!["x".to_string()]);
        pd.add_component(vec!["y".to_string()], vec!["y".to_string()]);
        assert_eq!(pd.num_components(), 2);
        assert!(pd.is_irredundant());
    }
    #[test]
    fn test_primary_decomposition_redundant() {
        let mut pd = PrimaryDecompositionData::new(5, vec!["x".to_string()]);
        pd.add_component(vec!["x".to_string()], vec!["x".to_string()]);
        pd.add_component(
            vec!["x".to_string(), "y".to_string()],
            vec!["x".to_string()],
        );
        assert_eq!(pd.num_components(), 2);
    }
    #[test]
    fn test_graded_module_poincare() {
        let mut m = GradedModule::new("k[x,y]");
        m.set_rank(0, 1);
        m.set_rank(1, 2);
        m.set_rank(2, 3);
        m.set_rank(3, 4);
        let ps = m.poincare_series();
        assert_eq!(ps, vec![(0, 1), (1, 2), (2, 3), (3, 4)]);
        assert_eq!(m.total_rank(), 10);
        assert_eq!(m.euler_characteristic(), -2);
    }
    #[test]
    fn test_graded_module_euler_characteristic() {
        let mut m = GradedModule::new("trivial");
        m.set_rank(0, 1);
        m.set_rank(2, 1);
        assert_eq!(m.euler_characteristic(), 2);
    }
    #[test]
    fn test_krull_dim_estimator_chain() {
        let mut est = KrullDimEstimator::new();
        est.add_prime(vec![]);
        est.add_prime(vec!["x".to_string()]);
        est.add_prime(vec!["x".to_string(), "y".to_string()]);
        assert_eq!(est.estimate_krull_dim(), 2);
    }
    #[test]
    fn test_krull_dim_estimator_empty() {
        let est = KrullDimEstimator::new();
        assert_eq!(est.estimate_krull_dim(), 0);
    }
    #[test]
    fn test_krull_dim_estimator_field() {
        let mut est = KrullDimEstimator::new();
        est.add_prime(vec![]);
        assert_eq!(est.estimate_krull_dim(), 0);
    }
    #[test]
    fn test_krull_dim_maximal_chains() {
        let mut est = KrullDimEstimator::new();
        est.add_prime(vec![]);
        est.add_prime(vec!["x".to_string()]);
        est.add_prime(vec!["y".to_string()]);
        est.add_prime(vec!["x".to_string(), "y".to_string()]);
        let chains = est.maximal_chains();
        assert!(!chains.is_empty());
    }
    #[test]
    fn test_total_new_axioms_count() {
        let env = registered_env();
        let new_axioms = [
            "FilteredRing",
            "AssociatedGraded",
            "FormalPowerSeries",
            "IAdicTopology",
            "CompleteRing",
            "ArtinRees",
            "IntegralExtension",
            "IntegralClosure",
            "IntegrallyClosedDomain",
            "GoingUp",
            "GoingDown",
            "LyingOver",
            "KrullDimension",
            "IdealHeight",
            "NoetherianRing",
            "ArtinianRing",
            "HopkinsLevitzki",
            "PrimaryIdeal",
            "PrimaryDecomposition",
            "LaskerNoether",
            "AssociatedPrimes",
            "Localization",
            "LocalizationModule",
            "NakayamasLemma",
            "CohenMacaulay",
            "RegularLocalRing",
            "RegularSequence",
            "ModuleDepth",
            "ProjectiveDimension",
            "AuslanderBuchsbaum",
            "GorensteinRing",
            "GradedMorphism",
            "HomogeneousIdeal",
            "HilbertFunction",
            "JacobsonRadical",
            "NilRadical",
            "SymmetricAlgebra",
            "DividedPowerAlgebra",
        ];
        for name in &new_axioms {
            assert!(
                env.get(&Name::str(*name)).is_some(),
                "Axiom '{}' not registered",
                name
            );
        }
    }
    #[test]
    fn test_hopf_algebra_axioms_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("Bialgebra")).is_some());
        assert!(env.get(&Name::str("HopfAlgebra")).is_some());
        assert!(env.get(&Name::str("Antipode")).is_some());
        assert!(env.get(&Name::str("Comultiplication")).is_some());
        assert!(env.get(&Name::str("Comodule")).is_some());
        assert!(env.get(&Name::str("CoalgebraMap")).is_some());
    }
    #[test]
    fn test_morita_theory_axioms_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("MoritaEquivalent")).is_some());
        assert!(env.get(&Name::str("DerivedMoritaEquivalent")).is_some());
        assert!(env.get(&Name::str("TiltingModule")).is_some());
        assert!(env.get(&Name::str("MoritaContext")).is_some());
    }
    #[test]
    fn test_noncommutative_axioms_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("OreExtension")).is_some());
        assert!(env.get(&Name::str("SkewPolynomialRing")).is_some());
        assert!(env.get(&Name::str("OreCondition")).is_some());
        assert!(env.get(&Name::str("WeylAlgebra")).is_some());
    }
    #[test]
    fn test_graded_hilbert_axioms_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("HilbertSeries")).is_some());
        assert!(env
            .get(&Name::str("CastelnuovoMumfordRegularity"))
            .is_some());
        assert!(env.get(&Name::str("GradedFreeResolution")).is_some());
    }
    #[test]
    fn test_homological_dimension_axioms_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("GlobalDimension")).is_some());
        assert!(env.get(&Name::str("InjectiveDimension")).is_some());
        assert!(env.get(&Name::str("FlatDimension")).is_some());
        assert!(env.get(&Name::str("WeakGlobalDimension")).is_some());
    }
    #[test]
    fn test_galois_theory_axioms_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("GaloisExtension")).is_some());
        assert!(env.get(&Name::str("GaloisGroup")).is_some());
        assert!(env.get(&Name::str("FundamentalTheoremGalois")).is_some());
        assert!(env.get(&Name::str("SolvableExtension")).is_some());
        assert!(env.get(&Name::str("SeparableExtension")).is_some());
    }
    #[test]
    fn test_brauer_group_axioms_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("CentralSimpleAlgebra")).is_some());
        assert!(env.get(&Name::str("BrauerGroup")).is_some());
        assert!(env.get(&Name::str("WedderburnTheorem")).is_some());
        assert!(env.get(&Name::str("ArtinWedderburn")).is_some());
        assert!(env.get(&Name::str("SchurLemma")).is_some());
    }
    #[test]
    fn test_witt_lambda_axioms_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("WittVectors")).is_some());
        assert!(env.get(&Name::str("LambdaRing")).is_some());
        assert!(env.get(&Name::str("TeichmullerLift")).is_some());
    }
    #[test]
    fn test_ordered_lattice_axioms_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("OrderedGroup")).is_some());
        assert!(env.get(&Name::str("LatticeOrderedRing")).is_some());
        assert!(env.get(&Name::str("ValuedField")).is_some());
    }
    #[test]
    fn test_dga_axioms_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("DifferentialGradedAlgebra")).is_some());
        assert!(env.get(&Name::str("AInfinityAlgebra")).is_some());
        assert!(env.get(&Name::str("DGModule")).is_some());
        assert!(env.get(&Name::str("QuasiIsomorphism")).is_some());
    }
    #[test]
    fn test_operad_axioms_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("Operad")).is_some());
        assert!(env.get(&Name::str("OperadAlgebra")).is_some());
        assert!(env.get(&Name::str("CyclicOperad")).is_some());
        assert!(env.get(&Name::str("Associahedron")).is_some());
    }
    #[test]
    fn test_derived_category_koszul_axioms_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("BoundedDerivedCategory")).is_some());
        assert!(env.get(&Name::str("TStructure")).is_some());
        assert!(env.get(&Name::str("KoszulDuality")).is_some());
        assert!(env.get(&Name::str("KoszulAlgebra")).is_some());
        assert!(env.get(&Name::str("KoszulResolution")).is_some());
        assert!(env.get(&Name::str("DerivedFunctor")).is_some());
    }
    #[test]
    fn test_vertex_algebra_axioms_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("VertexAlgebra")).is_some());
        assert!(env.get(&Name::str("ConformalVertex")).is_some());
    }
    #[test]
    fn test_prime_spectrum_axioms_registered() {
        let env = registered_env();
        assert!(env.get(&Name::str("PrimeSpectrum")).is_some());
        assert!(env.get(&Name::str("MaximalSpectrum")).is_some());
        assert!(env.get(&Name::str("ZariskiTopology")).is_some());
        assert!(env.get(&Name::str("StructureSheaf")).is_some());
    }
    #[test]
    fn test_hopf_algebra_data_group_like() {
        let mut h = HopfAlgebraData::new("k[Z/2]");
        h.add_group_like("1", "1");
        h.add_group_like("g", "g");
        assert_eq!(h.dimension(), 2);
        assert!(h.check_counit_group_like("1"));
        assert!(h.check_counit_group_like("g"));
        assert!(h.is_cocommutative());
    }
    #[test]
    fn test_hopf_algebra_data_primitive() {
        let mut h = HopfAlgebraData::new("k[x]/x^2");
        h.add_group_like("1", "1");
        h.add_primitive("x", "1");
        assert_eq!(h.dimension(), 2);
        assert_eq!(h.counit.get("x").copied(), Some(0));
        assert_eq!(h.antipode.get("x").map(|s| s.as_str()), Some("-x"));
    }
    #[test]
    fn test_galois_extension_fundamental_theorem() {
        let mut ext = GaloisExtensionData::new(
            "Q",
            "Q(sqrt2,sqrt3)",
            4,
            vec!["sqrt2".to_string(), "sqrt3".to_string()],
        );
        ext.add_automorphism("sigma", vec!["-sqrt2".to_string(), "sqrt3".to_string()]);
        ext.add_automorphism("tau", vec!["sqrt2".to_string(), "-sqrt3".to_string()]);
        ext.add_automorphism(
            "sigma_tau",
            vec!["-sqrt2".to_string(), "-sqrt3".to_string()],
        );
        ext.add_automorphism("id", vec!["sqrt2".to_string(), "sqrt3".to_string()]);
        assert_eq!(ext.galois_group_order(), 4);
        assert!(ext.satisfies_fundamental_theorem());
    }
    #[test]
    fn test_galois_extension_fixed_generators() {
        let mut ext = GaloisExtensionData::new(
            "Q",
            "Q(sqrt2,sqrt3)",
            4,
            vec!["sqrt2".to_string(), "sqrt3".to_string()],
        );
        ext.add_automorphism("sigma", vec!["-sqrt2".to_string(), "sqrt3".to_string()]);
        let fixed = ext.fixed_generators(&[0]);
        assert_eq!(fixed, vec!["sqrt3".to_string()]);
    }
    #[test]
    fn test_dg_algebra_boundary_zero() {
        let mut dga = DGAlgebra::new("Omega*(pt)");
        dga.add_basis("1", 0);
        dga.set_differential("1", vec![]);
        assert!(dga.check_d_squared_zero("1"));
    }
    #[test]
    fn test_dg_algebra_boundary_nontrivial() {
        let mut dga = DGAlgebra::new("Omega*(S1)");
        dga.add_basis("1", 0);
        dga.add_basis("dt", 1);
        dga.set_differential("1", vec![]);
        dga.set_differential("dt", vec![]);
        assert!(dga.check_d_squared_zero("1"));
        assert!(dga.check_d_squared_zero("dt"));
        assert_eq!(dga.basis_in_degree(0).len(), 1);
        assert_eq!(dga.basis_in_degree(1).len(), 1);
    }
    #[test]
    fn test_koszul_complex_ranks() {
        let kc =
            KoszulComplex::new(vec!["x".to_string(), "y".to_string()]).with_regular_sequence(true);
        assert_eq!(kc.length(), 2);
        assert_eq!(kc.rank_at(0), 1);
        assert_eq!(kc.rank_at(1), 2);
        assert_eq!(kc.rank_at(2), 1);
        assert_eq!(kc.rank_at(3), 0);
        assert_eq!(kc.euler_characteristic(), 0);
    }
    #[test]
    fn test_koszul_complex_acyclic() {
        let kc = KoszulComplex::new(vec!["x".to_string(), "y".to_string(), "z".to_string()])
            .with_regular_sequence(true);
        assert_eq!(kc.is_acyclic(), Some(true));
        assert_eq!(kc.length(), 3);
        assert_eq!(kc.rank_at(1), 3);
        assert_eq!(kc.rank_at(2), 3);
        assert_eq!(kc.rank_at(3), 1);
        assert_eq!(kc.euler_characteristic(), 0);
    }
    #[test]
    fn test_koszul_complex_betti_numbers() {
        let kc = KoszulComplex::new(vec!["f1".to_string(), "f2".to_string()]);
        let betti = kc.betti_numbers();
        assert_eq!(betti, vec![(0, 1), (1, 2), (2, 1)]);
    }
    #[test]
    fn test_koszul_complex_empty() {
        let kc = KoszulComplex::default();
        assert_eq!(kc.length(), 0);
        assert_eq!(kc.euler_characteristic(), 1);
        assert_eq!(kc.rank_at(0), 1);
    }
}