LeanPool.WhiteheadTheorem.Exponential #

Imported Lean Pool material for LeanPool.WhiteheadTheorem.Exponential.

theorem ContinuousMap.uncurry_curry {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace Y] (f : C(X × Y, Z)) :

f = f.curry.uncurry

uncurry_curry

source

theorem ContinuousMap.curry_uncurry {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace Y] (f : C(X, C(Y, Z))) :

f = f.uncurry.curry

curry_uncurry

source

theorem TopCat.exp_homEquiv_naturality_right {X : Type u_1} {Y : Type u_2} {Y' : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Y'] [TopologicalSpace Z] [LocallyCompactSpace X] (f : C(Y', Y)) (g : C(Y, C(X, Z))) :

(g.comp f).uncurry = g.uncurry.comp (f.prodMap (ContinuousMap.id X))

An auxiliary lemma only used for showing the naturality of topBinProdRightAdjExp

source

@[reducible, inline]

abbrev TopCat.topBinProdRight (X : TopCat) :

CategoryTheory.Functor TopCat TopCat

The functor TopCat.of (· × X) (taking the topological binary product, with X on the right) from TopCat to TopCat

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev TopCat.exp (X : TopCat) :

CategoryTheory.Functor TopCat TopCat

The exponentiation functor C(X, ·) from TopCat to TopCat

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def TopCat.topBinProdRightAdjExp (X : TopCat) [LocallyCompactSpace ↑X] :

X.topBinProdRight ⊣ X.exp

topBinProdRightAdjExp

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev TopCat.topBinProdRight' (X : Type u) [TopologicalSpace X] :

CategoryTheory.Functor TopCat TopCat

Same as topBinProdRight, except that X is not an object in TopCat, but simply a topological space

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev TopCat.topBinProdLeft' (X : Type u) [TopologicalSpace X] :

CategoryTheory.Functor TopCat TopCat

topBinProdLeft'

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev TopCat.exp' (X : Type u) [TopologicalSpace X] :

CategoryTheory.Functor TopCat TopCat

Same as exp, except that X is not an object in TopCat, but simply a topological space

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def TopCat.topBinProdRightAdjExp' (X : Type u) [TopologicalSpace X] [LocallyCompactSpace X] :

topBinProdRight' X ⊣ exp' X

Same as topBinProdRightAdjExp, except that X is not an object in TopCat, but simply a topological space

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def TopCat.topBinProdLeftAdjExp' (X : Type u) [TopologicalSpace X] [LocallyCompactSpace X] :

topBinProdLeft' X ⊣ exp' X

topBinProdLeftAdjExp'

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def ContinuousMap.argSwap {A : Type u_5} {B : Type u_6} {Y : Type u_7} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace Y] :

C(C(A × B, Y), C(B × A, Y))

argSwap

Equations

ContinuousMap.argSwap = { toFun := fun (f : C(A × B, Y)) => f.comp ContinuousMap.prodSwap, continuous_toFun := ⋯ }

Instances For

source

def ContinuousMap.curriedArgSwap {A : Type u_5} {B : Type u_6} {Y : Type u_7} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace Y] [LocallyCompactSpace A] [LocallyCompactSpace B] :

C(C(A, C(B, Y)), C(B, C(A, Y)))

curriedArgSwap

Equations

ContinuousMap.curriedArgSwap = { toFun := fun (f : C(A, C(B, Y))) => (ContinuousMap.argSwap f.uncurry).curry, continuous_toFun := ⋯ }

Instances For

source

theorem ContinuousMap.curriedArgSwap_curriedArgSwap {A : Type u_5} {B : Type u_6} {Y : Type u_7} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace Y] [LocallyCompactSpace A] [LocallyCompactSpace B] :

⇑curriedArgSwap ∘ ⇑curriedArgSwap = id

source

def ContinuousMap.curryLeft {A : Type u_5} {B : Type u_6} {Y : Type u_7} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace Y] (f : C(A × B, Y)) (b : B) :

C(A, Y)

curryLeft

Equations

f.curryLeft b = { toFun := fun (a : A) => f (a, b), continuous_toFun := ⋯ }

Instances For

source

def ContinuousMap.curryRight {A : Type u_5} {B : Type u_6} {Y : Type u_7} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace Y] (f : C(A × B, Y)) (a : A) :

C(B, Y)

curryRight

Equations

f.curryRight a = { toFun := fun (b : B) => f (a, b), continuous_toFun := ⋯ }

Instances For

source

theorem ContinuousMap.eq_of_curry_eq {A : Type u_5} {B : Type u_6} {Y : Type u_7} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace Y] {f g : C(A × B, Y)} (e : f.curry = g.curry) :

f = g

source

theorem ContinuousMap.eq_of_argSwap_curry_eq {A : Type u_5} {B : Type u_6} {Y : Type u_7} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace Y] {f g : C(A × B, Y)} (e : (argSwap f).curry = (argSwap g).curry) :

f = g

source

theorem TopCat.hom_eq_of_curry_eq {A : Type u_5} {B : Type u_6} [TopologicalSpace A] [TopologicalSpace B] {Y : TopCat} {f g : of (A × B) ⟶ Y} (e : (Hom.hom f).curry = (Hom.hom g).curry) :

f = g

source

theorem TopCat.hom_eq_of_argSwap_curry_eq {A : Type u_5} {B : Type u_6} [TopologicalSpace A] [TopologicalSpace B] {Y : TopCat} {f g : of (A × B) ⟶ Y} (e : (ContinuousMap.argSwap (Hom.hom f)).curry = (ContinuousMap.argSwap (Hom.hom g)).curry) :

f = g