Revision #3342 → #3390 · back to history
modifiedAdjunction via hom-setse5d3a80ad887
| Field | From #3342 | To #3390 |
|---|
| anchors | [{"section":"Definition via hom-sets","snippet":"can be defined as consisting of two functors"},{"type":"math_alttext","value":"{\\displaystyle \\Phi :\\mathrm {Hom} _{\\mathcal {C}}(F-,-)\\to \\mathrm {Hom} _{\\mathcal {D}}(-,G-).}"},{"type":"math_alttext","value":"{\\displaystyle \\Phi _{Y,X}:\\mathrm {Hom} _{\\mathcal {C}}(FY,X)\\to \\mathrm {Hom} _{\\mathcal {D}}(Y,GX)}"}] | — |
modifiedAdjunction via counit–unit8f88821afb2f
| Field | From #3342 | To #3390 |
|---|
| anchors | [{"section":"Definition via counit–unit","snippet":"A third way of defining an adjunction between two categories"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\varepsilon &:FG\\to 1_{\\mathcal {C}}\\\\\\eta &:1_{\\mathcal {D}}\\to GF\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle F\\xrightarrow {\\overset {}{\\;F\\eta \\;}} FGF\\xrightarrow {\\overset {}{\\;\\varepsilon F\\,}} F}"},{"type":"math_alttext","value":"{\\displaystyle G\\xrightarrow {\\overset {}{\\;\\eta G\\;}} GFG\\xrightarrow {\\overset {}{\\;G\\varepsilon \\,}} G}"}] | — |
modifiedPolynomial rings0290d6df8786
| Field | From #3342 | To #3390 |
|---|
| mathlib.module | Mathlib.Algebra.Polynomial.Eval | Mathlib.Algebra.Polynomial.AlgebraMap |
| note | The universal property of `R[x]` (evaluation) is formalized, but the adjunction with a category of pointed rings is not. | The universal property of `R[x]` (evaluation via `Polynomial.aeval`) is formalized, but the adjunction with a category of pointed rings is not. |
modifiedEquivalence yields adjoint paira9402d9006c3
| Field | From #3342 | To #3390 |
|---|
| anchors | [{"section":"Category theory","snippet":"the two functors F and G form an adjoint pair"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\varepsilon '&=\\varepsilon \\circ (F\\eta ^{-1}G)\\circ (FG\\varepsilon ^{-1})\\\\\\eta '&=(GF\\eta ^{-1})\\circ (G\\varepsilon ^{-1}F)\\circ \\eta \\end{aligned}}}"}] | — |
modifiedConnected components functor869db1727bb4
| Field | From #3342 | To #3390 |
|---|
| anchors | [{"section":"Category theory","snippet":"which assigns to a category its set of connected components is left-adjoint"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\varepsilon '&=\\varepsilon \\circ (F\\eta ^{-1}G)\\circ (FG\\varepsilon ^{-1})\\\\\\eta '&=(GF\\eta ^{-1})\\circ (G\\varepsilon ^{-1}F)\\circ \\eta \\end{aligned}}}"}] | — |
modifiedCurrying in cartesian closed categorye22336f295b6
| Field | From #3342 | To #3390 |
|---|
| anchors | [{"section":"Category theory","snippet":"This pair is often referred to as currying and uncurrying"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\varepsilon '&=\\varepsilon \\circ (F\\eta ^{-1}G)\\circ (FG\\varepsilon ^{-1})\\\\\\eta '&=(GF\\eta ^{-1})\\circ (G\\varepsilon ^{-1}F)\\circ \\eta \\end{aligned}}}"}] | — |
modifiedQuantifiers as adjoints to pullback85c9ed0bf918
| Field | From #3342 | To #3390 |
|---|
| anchors | [{"section":"Categorical logic","snippet":"quantifiers are identified with adjoints to the pullback functor"},{"type":"math_alttext","value":"{\\displaystyle \\{y\\in Y\\mid \\exists x.\\,\\psi _{f}(x,y)\\land \\phi _{S}(x)\\}}"},{"type":"math_alttext","value":"{\\displaystyle f^{*}:{\\text{Sub}}(Y)\\longrightarrow {\\text{Sub}}(X)}"},{"type":"math_alttext","value":"{\\displaystyle {\\operatorname {Hom} }(\\exists _{f}S,T)\\cong {\\operatorname {Hom} }(S,f^{*}T),}"},{"type":"math_alttext","value":"{\\displaystyle \\exists _{f}S\\subseteq T\\leftrightarrow S\\subseteq f^{-1}[T].}"},{"type":"math_alttext","value":"{\\displaystyle \\exists _{f}S=\\{y\\in Y\\mid \\exists (x\\in f^{-1}[\\{y\\}]).\\,x\\in S\\;\\}=f[S].}"},{"type":"math_alttext","value":"{\\displaystyle \\forall _{f}S=\\{y\\in Y\\mid \\forall (x\\in f^{-1}[\\{y\\}]).\\,x\\in S\\;\\}.}"}] | — |
modifiedDirect image as left adjoint in Set9eece214aefe
| Field | From #3342 | To #3390 |
|---|
| anchors | [{"section":"Categorical logic","snippet":"the category of sets and functions"},{"type":"math_alttext","value":"{\\displaystyle \\{y\\in Y\\mid \\exists x.\\,\\psi _{f}(x,y)\\land \\phi _{S}(x)\\}}"},{"type":"math_alttext","value":"{\\displaystyle f^{*}:{\\text{Sub}}(Y)\\longrightarrow {\\text{Sub}}(X)}"},{"type":"math_alttext","value":"{\\displaystyle {\\operatorname {Hom} }(\\exists _{f}S,T)\\cong {\\operatorname {Hom} }(S,f^{*}T),}"},{"type":"math_alttext","value":"{\\displaystyle \\exists _{f}S\\subseteq T\\leftrightarrow S\\subseteq f^{-1}[T].}"},{"type":"math_alttext","value":"{\\displaystyle \\exists _{f}S=\\{y\\in Y\\mid \\exists (x\\in f^{-1}[\\{y\\}]).\\,x\\in S\\;\\}=f[S].}"},{"type":"math_alttext","value":"{\\displaystyle \\forall _{f}S=\\{y\\in Y\\mid \\forall (x\\in f^{-1}[\\{y\\}]).\\,x\\in S\\;\\}.}"}] | — |
modifiedCounit–unit induces hom-set adjunction5b8be172d359
| Field | From #3342 | To #3390 |
|---|
| anchors | [{"section":"counit–unit adjunction induces hom-set adjunction","snippet":"we can construct a hom-set adjunction by finding the natural transformation"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\Phi _{Y,X}(f)=G(f)\\circ \\eta _{Y}\\\\\\Psi _{Y,X}(g)=\\varepsilon _{X}\\circ F(g)\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\Psi \\Phi f&=\\varepsilon _{X}\\circ FG(f)\\circ F(\\eta _{Y})\\\\&=f\\circ \\varepsilon _{FY}\\circ F(\\eta _{Y})\\\\&=f\\circ 1_{FY}=f\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\Phi \\Psi g&=G(\\varepsilon _{X})\\circ GF(g)\\circ \\eta _{Y}\\\\&=G(\\varepsilon _{X})\\circ \\eta _{GX}\\circ g\\\\&=1_{GX}\\circ g=g\\end{aligned}}}"}] | — |
modifiedHom-set adjunction induces counit–unit602df092fcf1
| Field | From #3342 | To #3390 |
|---|
| anchors | [{"section":"Hom-set adjunction induces all of the above","snippet":"which defines families of initial and terminal morphisms"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\Phi _{Y,X}(f)=G(f)\\circ \\eta _{Y}\\\\\\Phi _{Y,X}^{-1}(g)=\\varepsilon _{X}\\circ F(g)\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle 1_{FY}=\\varepsilon _{FY}\\circ F(\\eta _{Y}),}"},{"type":"math_alttext","value":"{\\displaystyle 1_{GX}=G(\\varepsilon _{X})\\circ \\eta _{GX}.}"}] | — |
modifiedAdjointness preserved under natural isomorphismac2f4e69e63d
| Field | From #3342 | To #3390 |
|---|
| anchors | [{"section":"Uniqueness","snippet":"then F is also left adjoint to G ′"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\eta '&=(\\tau \\ast \\sigma )\\circ \\eta \\\\\\varepsilon '&=\\varepsilon \\circ (\\sigma ^{-1}\\ast \\tau ^{-1}).\\end{aligned}}}"}] | — |
modifiedComposition of adjunctionseb88f2f49277
| Field | From #3342 | To #3390 |
|---|
| anchors | [{"section":"Composition","snippet":"Adjunctions can be composed in a natural fashion."},{"type":"math_alttext","value":"{\\displaystyle F\\circ F':E\\rightarrow C}"},{"type":"math_alttext","value":"{\\displaystyle G'\\circ G:C\\to E.}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}&1_{\\mathcal {E}}{\\xrightarrow {\\eta '}}G'F'{\\xrightarrow {G'\\eta F'}}G'GFF'\\\\&FF'G'G{\\xrightarrow {F\\varepsilon 'G}}FG{\\xrightarrow {\\varepsilon }}1_{\\mathcal {C}}.\\end{aligned}}}"}] | — |
modifiedAdjunction gives rise to a monad9f3882b8dc2b
| Field | From #3342 | To #3390 |
|---|
| anchors | [{"section":"Monads","snippet":"gives rise to an associated monad"},{"type":"math_alttext","value":"{\\displaystyle T:{\\mathcal {D}}\\to {\\mathcal {D}}}"},{"type":"math_alttext","value":"{\\displaystyle \\eta :1_{\\mathcal {D}}\\to T}"},{"type":"math_alttext","value":"{\\displaystyle \\mu :T^{2}\\to T\\,}"}] | — |
addedCounit and unit of an adjunctioncaec0c87cb44
addedEilenberg–Moore and Kleisli adjunctions200858b1c721
addedFree monoid functora2a107d6165e