Lean formalization
Each Math STEM unit declares a Lean status. full means the proof is checked end-to-end. partial means statements compile but Mathlib gaps gate the proofs. none means Mathlib coverage is too thin to state the theorem formally; the unit ships with a named human reviewer.
8
full
131
partial
174
none
203
Mathlib gaps
Precalculus foundations
7 units · full: 1 · partial: 6 · none: 0 · stub: 0
| id | title | status | module |
|---|---|---|---|
00.01.01 | Real numbers, integers, rationals | partial | Codex.Precalc.Numbers.Reals |
00.01.02 | Absolute value and the triangle inequality | partial | Codex.Precalc.Numbers.AbsoluteValue |
00.01.03 | Polynomials and rational expressions | partial | Codex.Precalc.Numbers.Polynomials |
00.02.05 | Function | full | Codex.Precalc.SetAndFunction.Function |
00.03.01 | Linear equations and the line | partial | Codex.Precalc.Equations.LinesPlane |
00.03.02 | Quadratic equations and the quadratic formula | partial | Codex.Precalc.Equations.QuadraticFormula |
00.04.01 | Inequalities (linear and quadratic) | partial | Codex.Precalc.Inequalities.Basic |
Algebra & linear algebra
10 units · full: 2 · partial: 7 · none: 1 · stub: 0
| id | title | status | module |
|---|---|---|---|
01.01.01 | Field | full | Codex.Foundations.LinearAlgebra.Field |
01.01.03 | Vector space | full | Codex.Foundations.LinearAlgebra.VectorSpace |
01.01.04 | Subspace, basis, dimension | partial | Codex.Foundations.LinearAlgebra.Basis |
01.01.05 | Linear transformation: kernel, image, rank-nullity | partial | Codex.Foundations.LinearAlgebra.RankNullity |
01.01.07 | Determinant: axiomatic + expansion + properties | partial | Codex.Foundations.LinearAlgebra.Determinant |
01.01.08 | Eigenvalue, eigenvector, characteristic polynomial | partial | Codex.Foundations.LinearAlgebra.Eigen |
01.01.11 | Jordan canonical form and minimal polynomial | partial | Codex.Foundations.LinearAlgebra.JordanForm |
01.01.12 | Singular value decomposition (finite-dim) | partial | Codex.Foundations.LinearAlgebra.SVD |
01.01.15 | Bilinear form / quadratic form | partial | Codex.Foundations.LinearAlgebra.BilinearQuadraticForm |
01.02.01 | Group | none | — |
Analysis
20 units · full: 2 · partial: 10 · none: 8 · stub: 0
| id | title | status | module |
|---|---|---|---|
02.01.01 | Topological space | full | Codex.Analysis.Topology.TopologicalSpace |
02.01.02 | Continuous map | none | — |
02.01.05 | Metric space | full | Codex.Analysis.Topology.MetricSpace |
02.01.06 | Quotient and identification topology | none | — |
02.01.07 | Fibration (Hurewicz and Serre) | none | — |
02.01.08 | Cofibration and homotopy extension property | none | — |
02.01.09 | Compact-open topology and function spaces | none | — |
02.02.01 | Real-number axioms (ordered field) | partial | Codex.Analysis.RealNumbers.Axioms |
02.03.02 | Cauchy sequences and Bolzano-Weierstrass | partial | Codex.Analysis.Sequences.CauchyBolzanoWeierstrass |
02.05.01 | Multi-variable limit and continuity | partial | Codex.Analysis.MultiVariable.LimitContinuity |
02.05.03 | Chain rule for multi-variable functions | partial | Codex.Analysis.MultiVariable.ChainRule |
02.05.04 | Implicit and inverse function theorems | partial | Codex.Analysis.MultiVariable.ImplicitInverse |
02.05.05 | Taylor's theorem and extrema in several variables | partial | Codex.Analysis.MultiVariable.TaylorExtrema |
02.11.01 | Bounded linear operators | partial | Codex.Analysis.FunctionalAnalysis.BoundedOperators |
02.11.03 | Unbounded self-adjoint operators | none | — |
02.11.04 | Banach space fundamentals | partial | Codex.Analysis.FunctionalAnalysis.BanachSpaces |
02.11.05 | Compact operators | partial | Codex.Analysis.FunctionalAnalysis.CompactOperators |
02.11.06 | Normed vector space | none | — |
02.11.07 | Inner product space | none | — |
02.11.08 | Hilbert space | partial | Codex.Analysis.FunctionalAnalysis.HilbertSpace |
Modern geometry
97 units · full: 3 · partial: 34 · none: 60 · stub: 0
| id | title | status | module |
|---|---|---|---|
03.01.01 | Tensor product | full | Codex.ModernGeometry.TensorAlgebra.TensorProduct |
03.01.02 | Associative algebra | full | Codex.ModernGeometry.TensorAlgebra.AssociativeAlgebra |
03.01.03 | Ideal in an algebra | full | Codex.ModernGeometry.TensorAlgebra.Ideal |
03.01.04 | Tensor algebra | none | — |
03.01.05 | Quotient algebra | none | — |
03.02.01 | Smooth manifold | partial | Codex.ModernGeometry.Manifolds.SmoothManifold |
03.03.01 | Lie group | partial | Codex.ModernGeometry.Lie.LieGroup |
03.03.02 | Group action | none | — |
03.03.03 | Orthogonal group | none | — |
03.04.01 | Lie algebra | partial | Codex.ModernGeometry.DifferentialForms.LieAlgebra |
03.04.02 | Differential forms | partial | Codex.ModernGeometry.DifferentialForms.DifferentialForms |
03.04.03 | Integration on manifolds | none | — |
03.04.04 | Exterior derivative | partial | Codex.ModernGeometry.DifferentialForms.ExteriorDerivative |
03.04.05 | Stokes' theorem | partial | Codex.ModernGeometry.DifferentialForms.StokesTheorem |
03.04.06 | De Rham cohomology | partial | Codex.ModernGeometry.DifferentialForms.DeRhamCohomology |
03.04.07 | Mayer-Vietoris sequence for de Rham cohomology | partial | Codex.ModernGeometry.DifferentialForms.MayerVietoris |
03.04.08 | Variational calculus on manifolds | none | — |
03.04.09 | Compactly-supported cohomology, integration along the fiber, and the de Rham Thom isomorphism | partial | Codex.ModernGeometry.DifferentialForms.ThomGlobalAngularForm |
03.04.10 | Good covers, finite-dimensionality of de Rham cohomology, and the Mayer-Vietoris induction | partial | Codex.ModernGeometry.DifferentialForms.GoodCover |
03.04.11 | Čech-de Rham double complex and the tic-tac-toe principle | partial | Codex.ModernGeometry.DifferentialForms.CechDeRham |
03.04.12 | Künneth formula for de Rham cohomology — two proofs | partial | Codex.DifferentialForms.Kunneth |
03.04.13 | Singular cohomology and the de Rham theorem (with $\mathbb{Z}$ coefficients) | partial | Codex.DifferentialForms.SingularCohomology |
03.04.E1 | Mayer-Vietoris and degree-theory exercise pack (Bott-Tu Ch. I supplement) | none | — |
03.05.01 | Principal bundle | none | — |
03.05.02 | Vector bundle | none | — |
03.05.03 | Orthogonal frame bundle | none | — |
03.05.04 | Connection on a vector bundle | none | — |
03.05.05 | Double cover | none | — |
03.05.07 | Principal bundle with connection | none | — |
03.05.08 | Complex vector bundle | none | — |
03.05.09 | Curvature of a connection | none | — |
03.05.10 | Sphere bundle, the global angular form, and the Hopf index theorem | partial | Codex.Bundles.SphereBundle |
03.06.03 | Stiefel-Whitney classes | none | — |
03.06.04 | Pontryagin and Chern classes | none | — |
03.06.05 | Invariant polynomial on a Lie algebra | none | — |
03.06.06 | Chern-Weil homomorphism | none | — |
03.07.05 | Yang-Mills action | none | — |
03.08.01 | Topological K-theory | none | — |
03.08.04 | Classifying space | none | — |
03.08.05 | Universal bundle, $H^*(BU(k))$, and the Borel presentation of flag-manifold cohomology | partial | Codex.KTheory.UniversalBundle |
03.08.06 | Stable homotopy | none | — |
03.08.07 | Bott periodicity | none | — |
03.09.02 | Clifford algebra | partial | Codex.SpinGeometry.CliffordAlgebra |
03.09.03 | Spin group | none | — |
03.09.04 | Spin structure on an oriented Riemannian manifold | none | — |
03.09.05 | Spinor bundle | none | — |
03.09.06 | Fredholm operators | none | — |
03.09.07 | Symbol of a differential operator | none | — |
03.09.08 | Dirac operator | none | — |
03.09.09 | Elliptic operators on a manifold | none | — |
03.09.10 | Atiyah-Singer index theorem | none | — |
03.09.11 | Clifford algebra classification — the 8×8 chessboard | partial | Codex.SpinGeometry.CliffordChessboard |
03.09.12 | KR-theory and the (1,1)-periodicity theorem | partial | Codex.SpinGeometry.KRTheory |
03.09.13 | Triality on Spin(8) and exceptional Lie groups via spinors | partial | Codex.SpinGeometry.Triality |
03.09.14 | Generalised Dirac bundles and the Bochner-Weitzenböck identity | partial | Codex.SpinGeometry.DiracBundle |
03.09.15 | Cl_k-linear Dirac operators and the KO-valued index | partial | Codex.SpinGeometry.ClkDirac |
03.09.16 | Positive scalar curvature obstruction theory | partial | Codex.SpinGeometry.PSCObstruction |
03.09.17 | Witten positive-mass theorem via spinors | partial | Codex.SpinGeometry.WittenPositiveMass |
03.09.18 | Berger holonomy classification and parallel spinors | partial | Codex.SpinGeometry.BergerHolonomy |
03.09.19 | Calibrated geometries — Special Lagrangian, associative, coassociative, Cayley | partial | Codex.SpinGeometry.CalibratedGeometries |
03.09.20 | Heat-kernel proof of the Atiyah-Singer index theorem | none | — |
03.09.21 | Family, equivariant, and Lefschetz fixed-point index theorems | none | — |
03.09.22 | Sobolev spaces, pseudodifferential operators, and elliptic parametrices | partial | Codex.SpinGeometry.Pseudodifferential |
03.09.E1 | Clifford and spin algebra exercise pack (Lawson-Michelsohn Ch. I supplement) | none | — |
03.09.E2 | Chapter IV applications exercise pack (Lawson-Michelsohn Ch. IV supplement) | none | — |
03.10.02 | CFT basics | none | — |
03.11.01 | Central extension of a Lie algebra | none | — |
03.11.02 | Infinite-dimensional Lie algebra representations | none | — |
03.11.03 | Virasoro algebra | none | — |
03.12.00 | Fundamental group | none | — |
03.12.01 | Homotopy and homotopy group | partial | Codex.ModernGeometry.Homotopy.Homotopy |
03.12.02 | Covering space | partial | Codex.ModernGeometry.Homotopy.CoveringSpace |
03.12.03 | Suspension | partial | Codex.ModernGeometry.Homotopy.Suspension |
03.12.04 | Spectrum | none | — |
03.12.05 | Eilenberg-MacLane space | none | — |
03.12.06 | Sullivan minimal models and rational homotopy theory | partial | Codex.Homotopy.SullivanMinimalModels |
03.12.07 | Whitehead tower, rational Hurewicz theorem, and Serre's finiteness | partial | Codex.Homotopy.WhiteheadTower |
03.12.08 | Fundamental groupoid | none | — |
03.12.09 | Seifert-van Kampen theorem | none | — |
03.12.10 | CW complex | none | — |
03.12.11 | Singular homology | none | — |
03.12.12 | Simplicial and $\Delta$-complex homology | none | — |
03.12.13 | Cellular homology and cellular approximation | none | — |
03.12.14 | Excision theorem | none | — |
03.12.15 | Eilenberg-Steenrod axioms | none | — |
03.12.16 | Poincaré duality | none | — |
03.12.17 | Cap product | none | — |
03.12.18 | Universal coefficient theorem | none | — |
03.12.19 | Hurewicz theorem | none | — |
03.12.20 | Whitehead's theorem | none | — |
03.12.21 | Blakers-Massey theorem | none | — |
03.12.23 | Euler characteristic | none | — |
03.12.E1 | Rational homotopy and Sullivan minimal-model exercise pack (Bott-Tu Ch. III §19 supplement) | none | — |
03.13.01 | Spectral sequences — exact couples, filtered complexes, double complexes | partial | Codex.SpectralSequences.SpectralSequence |
03.13.02 | Leray-Serre spectral sequence and the Gysin sequence | partial | Codex.SpectralSequences.LeraySerre |
03.13.03 | Leray-Hirsch theorem and the splitting principle for vector bundles | partial | Codex.SpectralSequences.LerayHirschSplitting |
03.13.E1 | Spectral-sequence computation exercise pack (Bott-Tu Ch. III supplement) | none | — |
Algebraic geometry
37 units · full: 0 · partial: 26 · none: 11 · stub: 0
| id | title | status | module |
|---|---|---|---|
04.01.01 | Sheaf | partial | Codex.AlgebraicGeometry.Sheaves.Sheaf |
04.01.02 | Stalk of a sheaf | partial | Codex.AlgebraicGeometry.Sheaves.Stalk |
04.01.03 | Sheafification | partial | Codex.AlgebraicGeometry.Sheaves.Sheafification |
04.01.04 | Direct and inverse image of sheaves | partial | Codex.AlgebraicGeometry.Sheaves.DirectInverseImage |
04.02.01 | Scheme | partial | Codex.AlgebraicGeometry.Schemes.Scheme |
04.02.02 | Affine scheme | partial | Codex.AlgebraicGeometry.Schemes.AffineScheme |
04.02.03 | Projective scheme | partial | Codex.AlgebraicGeometry.Schemes.ProjectiveScheme |
04.02.04 | Morphism of schemes | partial | Codex.AlgebraicGeometry.Schemes.Morphism |
04.02.05 | Smooth, étale, and unramified morphisms | none | — |
04.02.07 | Nullstellensatz and dimension theory | none | — |
04.03.01 | Sheaf cohomology | partial | Codex.AlgebraicGeometry.Cohomology.SheafCohomology |
04.03.02 | Local systems, monodromy, and twisted cohomology | none | — |
04.03.03 | Čech cohomology of sheaves on schemes | none | — |
04.03.04 | Cohomology of line bundles on projective space | none | — |
04.03.05 | Serre's vanishing and finiteness theorems | none | — |
04.04.01 | Riemann-Roch theorem for curves | partial | Codex.AlgebraicGeometry.RiemannRoch.Curves |
04.04.02 | Hurwitz formula | none | — |
04.04.03 | Elliptic curves | none | — |
04.05.01 | Weil divisor | partial | Codex.AlgebraicGeometry.Divisors.WeilDivisor |
04.05.02 | Picard group | partial | Codex.AlgebraicGeometry.Divisors.PicardGroup |
04.05.03 | Line bundle on a scheme | partial | Codex.AlgebraicGeometry.Divisors.LineBundle |
04.05.04 | Cartier divisor | partial | Codex.AlgebraicGeometry.Divisors.CartierDivisor |
04.05.05 | Ample and very ample line bundle | partial | Codex.AlgebraicGeometry.Divisors.Ample |
04.05.06 | Intersection pairing on a surface | none | — |
04.05.07 | Adjunction formula on a surface | none | — |
04.05.08 | Riemann-Roch theorem for surfaces | none | — |
04.06.01 | Quasi-coherent sheaf | partial | Codex.AlgebraicGeometry.Coherent.QuasiCoherent |
04.06.02 | Coherent sheaf | partial | Codex.AlgebraicGeometry.Coherent.Coherent |
04.07.01 | Projective space | partial | Codex.AlgebraicGeometry.Projective.ProjectiveSpace |
04.07.02 | Blowup | partial | Codex.AlgebraicGeometry.Projective.Blowup |
04.08.01 | Sheaf of differentials | partial | Codex.AlgebraicGeometry.Differentials.Differentials |
04.08.02 | Canonical sheaf | partial | Codex.AlgebraicGeometry.Differentials.CanonicalSheaf |
04.08.03 | Serre duality | partial | Codex.AlgebraicGeometry.Differentials.SerreDuality |
04.09.01 | Hodge decomposition | partial | Codex.AlgebraicGeometry.Hodge.HodgeDecomposition |
04.09.02 | Kodaira vanishing theorem | partial | Codex.AlgebraicGeometry.Hodge.KodairaVanishing |
04.10.01 | Moduli of curves | partial | Codex.AlgebraicGeometry.Moduli.ModuliOfCurves |
04.10.02 | Geometric invariant theory | partial | Codex.AlgebraicGeometry.Moduli.GIT |
Symplectic geometry
49 units · full: 0 · partial: 0 · none: 49 · stub: 0
| id | title | status | module |
|---|---|---|---|
05.00.01 | Lagrangian mechanics on the tangent bundle | none | — |
05.00.02 | Hamilton's principle of least action | none | — |
05.00.03 | Legendre transform | none | — |
05.00.04 | Noether's theorem | none | — |
05.00.06 | Galilean group and Newtonian mechanics | none | — |
05.01.01 | Symplectic vector space | none | — |
05.01.02 | Symplectic manifold | none | — |
05.01.03 | Symplectic group | none | — |
05.01.04 | Darboux's theorem | none | — |
05.01.05 | Moser's trick | none | — |
05.02.01 | Hamiltonian vector field | none | — |
05.02.02 | Poisson bracket and Poisson manifold | none | — |
05.02.03 | Integrable system | none | — |
05.02.04 | Action-angle coordinates | none | — |
05.02.05 | Cotangent bundle as canonical symplectic manifold | none | — |
05.02.06 | Geodesic flow as a Hamiltonian flow | none | — |
05.02.07 | Liouville's volume theorem | none | — |
05.02.08 | Poincaré recurrence theorem | none | — |
05.02.09 | Poincaré-Cartan integral invariants | none | — |
05.03.01 | Coadjoint orbit | none | — |
05.04.01 | Moment map | none | — |
05.04.02 | Marsden-Weinstein symplectic reduction | none | — |
05.04.03 | Atiyah-Guillemin-Sternberg convexity theorem | none | — |
05.04.04 | Delzant theorem (symplectic toric classification) | none | — |
05.04.05 | Duistermaat-Heckman theorem | none | — |
05.04.06 | Symplectic blow-up and symplectic cut | none | — |
05.05.01 | Lagrangian submanifold | none | — |
05.05.02 | Weinstein Lagrangian neighbourhood theorem | none | — |
05.05.03 | Generating functions for symplectomorphisms | none | — |
05.05.04 | Hamilton-Jacobi equation | none | — |
05.06.01 | Almost-complex structure on a symplectic manifold | none | — |
05.06.02 | Pseudoholomorphic curve | none | — |
05.06.03 | Newlander-Nirenberg integrability theorem | none | — |
05.07.01 | Gromov non-squeezing theorem | none | — |
05.07.02 | Symplectic capacity | none | — |
05.08.01 | Arnold conjecture and Floer homology setup | none | — |
05.08.02 | Floer homology | none | — |
05.08.03 | Maslov index | none | — |
05.08.04 | Conley-Zehnder index | none | — |
05.09.01 | Kolmogorov-Arnold-Moser theorem | none | — |
05.09.02 | Adiabatic invariants | none | — |
05.09.03 | Birkhoff normal form | none | — |
05.09.04 | Williamson normal form for quadratic Hamiltonians | none | — |
05.09.05 | Euler-Arnold equations | none | — |
05.09.06 | Nekhoroshev estimates | none | — |
05.10.01 | Contact manifold | none | — |
05.10.02 | Symplectisation of a contact manifold | none | — |
05.10.03 | Gray's stability theorem | none | — |
05.10.04 | Contact topology and Reeb dynamics | none | — |
Statistical field theory
22 units · full: 0 · partial: 0 · none: 22 · stub: 0
| id | title | status | module |
|---|---|---|---|
08.01.01 | Partition function (statistical mechanics) | none | — |
08.01.02 | Ising model | none | — |
08.01.03 | Boltzmann distribution and canonical ensemble | none | — |
08.01.04 | Free energy | none | — |
08.02.01 | Mean-field theory and Curie-Weiss model | none | — |
08.02.02 | Spontaneous symmetry breaking | none | — |
08.02.03 | Mermin-Wagner theorem | none | — |
08.03.01 | Onsager solution of the 2D Ising model (transfer matrix) | none | — |
08.03.02 | Transfer matrix | none | — |
08.04.01 | Renormalisation group (real-space block decimation) | none | — |
08.04.02 | Wilson-Fisher fixed point and universality | none | — |
08.04.03 | Beta function (renormalisation group) | none | — |
08.04.04 | Block-spin decimation | none | — |
08.05.01 | Critical exponents and scaling laws | none | — |
08.05.02 | Correlation functions (statistical mechanics) | none | — |
08.06.01 | Gaussian field theory and free boson | none | — |
08.06.02 | Conformal symmetry at criticality | none | — |
08.07.01 | Path integral formulation of statistical mechanics | none | — |
08.08.01 | Wilson's lattice gauge theory | none | — |
08.08.02 | Wilson action | none | — |
08.08.03 | Effective field theory | none | — |
08.09.01 | Quantum-classical correspondence (Wick rotation) | none | — |
Riemann surfaces
45 units · full: 0 · partial: 22 · none: 23 · stub: 0
| id | title | status | module |
|---|---|---|---|
06.01.01 | Holomorphic function | partial | Codex.RiemannSurfaces.ComplexAnalysis.Holomorphic |
06.01.02 | Cauchy integral formula | partial | Codex.RiemannSurfaces.ComplexAnalysis.CauchyIntegralFormula |
06.01.03 | Residue theorem | partial | Codex.RiemannSurfaces.ComplexAnalysis.ResidueTheorem |
06.01.04 | Analytic continuation | partial | Codex.RiemannSurfaces.ComplexAnalysis.AnalyticContinuation |
06.01.05 | Meromorphic function | partial | Codex.RiemannSurfaces.ComplexAnalysis.MeromorphicFunction |
06.01.06 | Riemann mapping theorem | partial | Codex.RiemannSurfaces.ComplexAnalysis.RiemannMappingTheorem |
06.01.07 | Riemann sphere | none | — |
06.01.08 | Möbius (linear-fractional) transformations | none | — |
06.01.10 | Cauchy-Riemann equations and harmonic conjugate | partial | Codex.RiemannSurfaces.ComplexAnalysis.CauchyRiemann |
06.01.11 | Harmonic functions on the plane | none | — |
06.01.12 | Maximum modulus + Schwarz lemma | none | — |
06.01.13 | Argument principle and Rouché's theorem | none | — |
06.02.01 | Branch point and ramification | partial | Codex.RiemannSurfaces.BranchPoints.BranchPointRamification |
06.02.02 | Branched coverings of Riemann surfaces | none | — |
06.02.03 | Riemann's existence theorem for algebraic curves | none | — |
06.03.01 | Riemann surface | partial | Codex.RiemannSurfaces.Surfaces.RiemannSurface |
06.03.02 | Genus of a Riemann surface | partial | Codex.RiemannSurfaces.Surfaces.GenusRiemannSurface |
06.03.03 | Uniformization theorem | partial | Codex.RiemannSurfaces.Surfaces.UniformizationTheorem |
06.04.01 | Riemann-Roch theorem for compact Riemann surfaces | partial | Codex.RiemannSurfaces.RiemannRoch.CompactSurface |
06.04.02 | Čech cohomology of holomorphic line bundles | none | — |
06.04.03 | Hodge decomposition on a compact Riemann surface | none | — |
06.04.04 | Serre duality on a curve | none | — |
06.04.05 | Hilbert-space PDE for $\bar\partial$ | none | — |
06.04.07 | Survey of sheaf cohomology on Riemann surfaces | none | — |
06.05.01 | Divisor on a Riemann surface | partial | Codex.RiemannSurfaces.DivisorsBundles.DivisorRiemannSurface |
06.05.02 | Holomorphic line bundle on a Riemann surface | partial | Codex.RiemannSurfaces.DivisorsBundles.HolomorphicLineBundle |
06.05.03 | Riemann-Hurwitz formula | partial | Codex.RiemannSurfaces.DivisorsBundles.RiemannHurwitzFormula |
06.06.01 | Holomorphic 1-form / abelian differential | partial | Codex.RiemannSurfaces.Jacobians.HolomorphicOneForm |
06.06.02 | Period matrix | partial | Codex.RiemannSurfaces.Jacobians.PeriodMatrix |
06.06.03 | Jacobian variety | partial | Codex.RiemannSurfaces.Jacobians.JacobianVariety |
06.06.04 | Abel-Jacobi map | partial | Codex.RiemannSurfaces.Jacobians.AbelJacobiMap |
06.06.05 | Theta function | partial | Codex.RiemannSurfaces.Jacobians.ThetaFunction |
06.06.06 | Jacobi inversion theorem | none | — |
06.06.07 | Riemann's bilinear relations | none | — |
06.06.08 | Schottky problem | none | — |
06.07.01 | Holomorphic functions of several variables | partial | Codex.RiemannSurfaces.SeveralVariables.HolomorphicSeveralVariables |
06.07.02 | Hartogs phenomenon | partial | Codex.RiemannSurfaces.SeveralVariables.HartogsPhenomenon |
06.08.01 | Gauss-Manin connection | none | — |
06.08.02 | Variation of Hodge structure on the Jacobian | none | — |
06.08.03 | Moduli of Riemann surfaces | none | — |
06.09.01 | Stein Riemann surfaces | none | — |
06.09.02 | Cartan's Theorems A and B for Stein Riemann surfaces | none | — |
06.09.03 | Behnke-Stein theorem | none | — |
06.09.04 | Cousin I (additive) | none | — |
06.09.05 | Cousin II (multiplicative) | none | — |
Representation theory
26 units · full: 0 · partial: 26 · none: 0 · stub: 0
| id | title | status | module |
|---|---|---|---|
07.01.01 | Group representation | partial | Codex.RepresentationTheory.Foundations.GroupRepresentation |
07.01.02 | Schur's lemma | partial | Codex.RepresentationTheory.Foundations.SchurLemma |
07.01.03 | Character of a representation | partial | Codex.RepresentationTheory.Foundations.Character |
07.01.04 | Character orthogonality | partial | Codex.RepresentationTheory.Foundations.CharacterOrthogonality |
07.01.05 | Regular representation | partial | Codex.RepresentationTheory.Foundations.RegularRepresentation |
07.01.06 | Tensor product of representations | partial | Codex.RepresentationTheory.Foundations.TensorProduct |
07.01.07 | Induced representation | partial | Codex.RepresentationTheory.Foundations.InducedRepresentation |
07.01.08 | Frobenius reciprocity | partial | Codex.RepresentationTheory.Foundations.FrobeniusReciprocity |
07.02.01 | Maschke's theorem | partial | Codex.RepresentationTheory.Character.Maschke |
07.03.01 | Highest weight representation | partial | Codex.RepresentationTheory.HighestWeight.HighestWeight |
07.04.01 | Cartan-Weyl classification | partial | Codex.RepresentationTheory.Classification.CartanWeyl |
07.05.01 | Symmetric group representation | partial | Codex.RepresentationTheory.Symmetric.SymmetricGroupRepresentation |
07.05.02 | Young diagram and tableau | partial | Codex.RepresentationTheory.Symmetric.YoungDiagram |
07.05.03 | Specht module | partial | Codex.RepresentationTheory.Symmetric.SpechtModule |
07.06.01 | Lie algebra representation | partial | Codex.RepresentationTheory.LieAlgebraic.LieAlgebraRepresentation |
07.06.02 | Universal enveloping algebra | partial | Codex.RepresentationTheory.LieAlgebraic.UniversalEnvelopingAlgebra |
07.06.03 | Root system | partial | Codex.RepresentationTheory.LieAlgebraic.RootSystem |
07.06.04 | Weyl group | partial | Codex.RepresentationTheory.LieAlgebraic.WeylGroup |
07.06.05 | Dynkin diagram | partial | Codex.RepresentationTheory.LieAlgebraic.DynkinDiagram |
07.06.06 | Verma module | partial | Codex.RepresentationTheory.LieAlgebraic.VermaModule |
07.06.07 | Weyl character formula | partial | Codex.RepresentationTheory.LieAlgebraic.WeylCharacterFormula |
07.06.08 | Weyl dimension formula | partial | Codex.RepresentationTheory.LieAlgebraic.WeylDimensionFormula |
07.06.09 | Borel-Weil theorem | partial | Codex.RepresentationTheory.LieAlgebraic.BorelWeilTheorem |
07.07.01 | Compact Lie group representation | partial | Codex.RepresentationTheory.CompactLie.CompactLieGroupRepresentation |
07.07.02 | Peter-Weyl theorem | partial | Codex.RepresentationTheory.CompactLie.PeterWeylTheorem |
07.07.03 | Haar measure | partial | Codex.RepresentationTheory.CompactLie.HaarMeasure |