General documentation

index
foundational types
tactics

Library

MBDVendor
Magnitude
Algebra
FiniteModuleDecomposition
IndecomposableLocalEnd
RightModuleAlmostSplit
RightModuleFactorCategory
RightModuleFactorLeftTau
RightModuleFactorRightTau
RightModuleFactorStrict
RightModuleFactorTauAssembly
RightModuleFiniteType
RightModuleIntrinsicArrowMultiplicity
RightModuleLeftAlmostSplit
RightModuleLeftTau
RightModulePrimitiveIdempotent
RightModuleProjectiveBoundary
RightModuleRadical
RightModuleRightTau
RightModuleTauAssembly
RightModuleTauData
RightModuleTranslation
RightModuleTranslationMultiplicity
CategoryTheory
AlgebraicallyClosedOccurrenceBasis
AlgebraicallyClosedResidue
AlmostSplitCokernel
AlmostSplitSummandIrreducible
CategoricalIrreducibleSpace
FiniteGeneratorRadicalNilpotence
FiniteIndecomposableDecomposition
FiniteKrullSchmidtMatrix
FiniteTauIrreducible
FiniteTauMatrix
FiniteTauTranslationMultiplicity
HomIdealComap
HomMeshInverse
HomUnitEquations
IndecomposableOfLocalEnd
IrreducibleAbelian
IrreducibleRadicalSquare
LinearBiproduct
MeshWeight
ModuleIrreducibleSpaceComparison
ModuleRadicalSquareComparison
PositiveWeightStrictness
ProjectiveCover
RadicalMinimality
ResidueDimension
TauExactDimension
Combinatorics
EulerSurplus
MeshMatrix
LinearAlgebra
LocalAlgebraResidue
QSE
CategoryTheory
CategoricalRadical
CategoricalRadicalIdeal
FiniteTauCategory
HomIdeal
HomIdealPowers
IdealQuotient
IdempotentLifting
IyamaFiniteLadderComparison
IyamaKrullSchmidtConormalForm
IyamaKrullSchmidtDirectFinite
IyamaKrullSchmidtNormalForm
IyamaKrullSchmidtWeight
IyamaLadderComparisonAssembly
IyamaLadderComparisonCertificate
IyamaLadderComparisonEndpoint
IyamaLadderRadical
IyamaLeftLadderBasic
IyamaLeftLadderIteration
IyamaLeftLadderNormalization
IyamaLeftLadderPropagation
IyamaLeftLadderRadicalLayer
IyamaLeftSuccessorSpecialness
IyamaMeshSplitLifting
IyamaMixedMeshSplitLifting
IyamaNakayamaBoundary
IyamaNakayamaExtraction
IyamaNakayamaPair
IyamaNakayamaWeight
IyamaReversedDomination
IyamaReversedRightPrefix
IyamaRightLadderConstruction
IyamaRightLadderIteration
IyamaRightLadderPropagation
IyamaRightLadderRadicalWitness
IyamaRightSuccessorSpecialness
IyamaSpecialMorphism
IyamaTauBiproduct
IyamaTauSequence
LinearGeneratedHomIdeal
MinimalMorphism
NilpotentCategoricalRadical
SplitMorphismComplement
ConvexGeometry
Basic
ClosedSets
Finite
LevelPolynomial
Relabeling
Foundation
RingTheory
KrullSchmidt
Indecomposable
LocalRing
Basic
RepresentationTheory
AdditiveSubcategory
AlmostSplitCofinite
AlmostSplitKernel
AlmostSplitUniqueness
AntiExchange
Biduality
Contragredient
ContragredientDuality
ContragredientFunctor
ContravariantTransport
DualityConsequences
EndomorphismRadical
FacSub
FiniteType
FiniteTypeAlmostSplit
IrreducibleCofinite
IrreducibleRadicalQuotient
LeftAROccurrenceBasis
LinearIrreducibleHomSpace
RightAROccurrenceBasis
SplitInjective
SplitProjective
SubmoduleAntiExchange
Trace
MultiplicativeBasisDeformations (file)
Foundations
A0Basis
A0Graded
A0Lift
A0Normed
A0RayTable
A0Rays
A0RepFinite
A0Table
AEven
AEvenChar2
APaths
ARBrick
ARBridge
ARInjData
ARMeshData
ARMeshExactness
ARMeshFinite
ARMeshWalk
ARPrime
ARQuiver
ARTranslationQuiver
AReflectChar2
ASort
ActiveZero
BarComplex
BaseChange
BasicCorner
BasicLabels
BasisExt
BinaryNormalization
Bockstein
BoundConfigs
BoundQuiverInfinite
BrickExclusion
CategoryAlgebra
CategoryAlgebraCorners
CentralizerAlgebra
CentralizerTable
Char2A0
Char2Basic
Char2Core
CharBasis
CharComplex
CharDecomp
CharSummands
ComponentGlue
ComponentSpan
ComponentTransfer
ConnectedCase
ConnectedChar2
ConnectedIdempotents
ConnectedWt
ContourTrees
Contours
CoordGrading
Cor105A0
Cor105Bridge
CornerAlgebra
CornerDeriv
CornerRadical
CornerRepFinite
CoverCategory
CoverPotential
CoverWeights
CoveringIdeals
CoveringMesh
Criterion
CrownRows
CyclicCorner
D4Return
DTopPaths
DeckCharacter
DeckCountable
DeckData
DeckGrading
DeckGroup
DeckInstance
DeckPi1
DegreeDeck
DeletionBrick
DeletionBrickAbstract
DeletionTransfer
Descent
DualRepresentables
DualWeight
DynkinConfigs
DynkinForm
E7Return
ECase
EndpointChains
EssentialSurjectivity
EvaluationCriterion
EvaluationCriterionStd
EvaluationDim
EvaluationEquivalence
EvenLineTop
Exchange
Exhaustion
ExtExtensions
ExtHigher
ExtOne
ExtProjective
ExtResolutions
ExtResolutionsA0
ExtUnique
FamilyCriterionA0
FamilyCriterionGen
FamilyNormalization
FibreRays
FilteredA
FilteredNormalForm
FiltrationDim
FiltrationRays
FinPoset
FinalBasis
FinalStandardness
FloorWeight
FormFunctor
FreeGroupoidVertex
FullIdempotent
FullSubquiver
GModLemmas
GaugeDescent
GaugeTransfer
GeneratingPaths
GlobalDimension
GradedBasis
GradedCover
GradedDecomp
GradedExt
GradedHomDimension
GradedLayers
GradedLocal
GradedPreproj
GradedRays
GradedRealization
GradedRealizationIso
HochschildCochains
HochschildMesh
HomBasis
HomIdeal
IndicatorCocycles
IndicatorRel
Induction
InitialFormProducts
InjectiveLabels
IntegralA0
IntegralCoker
IntegralCokerEquiv
IntegralCokerIso
IntegralCorner
IntegralHom
IntegralLifting
IntegralLifts
IntegralMesh
IntegralModuleLift
IntegralModules
IntegralPresentation
IntegralPsi
IntegralTable
IntegralTransport
IntegralWeightInstance
IntegralWeightLift
IntegralWeights
KrullSchmidtForm
KrullTrdeg
LayerComparison
LayerExactness
LayerExactnessDual
LiftedEvaluation
LiftedModules
LinCorners
LineTopPaths
LocalCorner
LocalMesh
MGrading
MeshCategory
MeshCokerWeights
MeshComplex
MeshCorrections
MeshDegreeTwo
MeshDerivativeRows
MeshExact
MeshGauge
MeshGrading
MeshRadical
MeshWeights
MeshWeightsConn
ModFourComparison
ModelDeck
MorseCollapse
NonbasicBasis
NormalFormAlgebra
NormalFormGeneral
NormalFormRetained
NormedBasis
NormedTransport
ObjectQuotients
ObjectValues
OddGauge
OddGaugeQ
OddQuotient
OppositeControls
OppositeControls2
OppositeControlsTwo
OppositeRepFinite
OrbitDim
OrbitReps
PathEval
PathGrading
PathGradingComp
PathMaps
PathShape
Peirce
PeriodicComponents
PeriodicDepth
PeriodicGauge
PeriodicGenerator
PeriodicIso
PeriodicLocalization
PeriodicModel
PosetRepBound
PosetRepInfinite
PosetWeights
PositiveDeformation
PreprojFunctionals
PreprojectiveDimension
PreprojectiveNilpotent
PrimeCoker
PrimeTable
PrimeWeight
PrimitiveCorners
PrimitiveDecomposition
ProjectiveEvaluation
ProjectiveIdempotents
Prop103
ProperProducts
PsiInjective
R5Span
RadicalFiltration
RayBasis
RayConfigs
RayDegree
RayOp
RayPres
RayProduct
RaySetting
RayStandard
RayTable
RayTransport
RayWeights
RayWeightsIso
Rays
ReRoot
ReductionMesh
RelativeHochschild
RepFinite
RepresentationTransfer
ResidualCorrection
ResidualDual
ResidualSpaces
RightModules
RootedGauge
RootedTrace
RowRotation
RowSpan
SameARQuiver
SameARTau
ScalDivisible
ScalSplit
ScalSplitSink
ScalarAutomorphism
ScalarFibres
ScalarNormalization
SectionalCover
SectionalDynkin
SectionalMesh
SectionalPaths
SectionalTree
SimpleTops
SkeletonExists
SplitTransfer
SquareFree
SquareZero
SquareZeroModules
SquareZeroWeight
StableTranslation
StandardConverse
StandardForm
StandardRay
StarArms
StarAut
StarCase
StarCorner
StarDSpan
StarESpan
StarGauge
StarGaugeQ
StarModel
StarRows
StarSpan
StarTrace
StarTree
StarTwo
StarTypes
StemProduct
StrictLayers
StrictLayersArtin
StrictLayersDual
StrictLayersModules
SubstarRestriction
Successor
SupportPoset
SupportedBockstein
SupportedBocksteinFree
TabSys
TableAlg
TableBound
TableConf
TableCover
TableInduction
TableOfBasis
TableRetract
TableSupport
TableTree
TableWeightLifting
ThinCategory
Thinness
TraceAlgebra
TraceAlgebraChar2
TraceAlgebraTwo
TraceDSpan
TraceE6
TraceE78
TraceE78Char2
TraceE78Integral
TraceEChar2
TraceTwoTorsion
TraceTypesAD
TransportFamily
TreeArms
TreeBFS
TreeEmbed
TreePoset
TreeRepetition
Twist
TwistedTrace
TwoSidedPaths
TwoTables
UBound
UnequalAction
UnitCoefficients
UnitNormalized
WeightCoker
WeightDivisibility
WeightEv
WeightExt
WeightExtGroup
WeightGrading
WeightHH
WeightLift
WeightTwist
ZCocycle
ZDeltaGauge
ZModFour
ZTransport
Independent
MeshComparison
Skeleton
StandardComparison
TheoremA
TheoremB
Translate
Refinements
CocycleLift
ConeLifting
FamilyArrows
FamilyLifts
FamilyNormalForm
FamilyPresentation
FamilyPsi
FamilySpan
FamilyTwist
FibreAlgebra
FilteredMaps
FlatPerturbation
FlatPerturbationDim
FlatPerturbationGr
FlatPerturbationRight
FullHochschild
GeneralLift
LiftTransport
LiftedCategory
LiftedCompleteness
LiftedCorner
LiftedLayers
LiftedMesh
LiftedMeshData
LiftedRadical
MeshFirstOrder
MeshNormalForm
ModuleLifting
Nonresonant
OneSidedPaths
PathRealize
PolyFamily
PolynomialFlatness
PolynomialMeshComparison
RegularLift
ResolutionForms
SameSupportForms
SameSupportResidual
SplitDeformation
SplitRelative
SplitSemisimple
Twist
TwistLifting
WeightCone
WeightedComparison
Statements
A0Basic
A0Instances
ClassicalMixtures
Cor105WP
FamilyCriterion
FamilyCriterionWP
HochschildDecomposition
IntegerWeights
IntegralCompanion
MainTheorems
ModFour
PartOne
PolynomialMesh
SanityChecks
Statement

Color scheme