The Moore-path replacement of a map

For a continuous map p : E → B, the Moore-path replacement is the space E' = MooreReplacement p of pairs (e, γ) of a point e ∈ E and a Moore path γ in B starting at p e, with the endpoint map p' (e, γ) = γ.target.

• p' has a transitive lifting function, given by concatenation: a path δ starting at γ.target lifts to s ↦ (e, γ · δ|[0, s]). So p' is a Hurewicz fibration, whatever p is (TauCeti.MooreReplacement.isHurewiczFibration_endpoint).
• The inclusion E → E', e ↦ (e, const), is a map over B and a homotopy equivalence, with homotopy inverse the projection (e, γ) ↦ e: a path shrinks to its start (TauCeti.MooreReplacement.homotopyEquiv).
• The fibre F' of p' over b carries the strict right action (e, γ) · ω = (e, γ · ω) of the Moore loops at b, continuous in both variables. No choice of lifting function for p is involved.

When p itself has a lifting function Φ, transport F' → F, (e, γ) ↦ Φ (e, γ)(end), to the fibre F of p over b is a homotopy equivalence, with homotopy inverse f ↦ (f, const) (TauCeti.MooreLiftingFunction.transportHomotopyEquiv). When Φ is transitive, the Moore loops act strictly on F by f · ω = Φ (f, ω)(end), and transport is strictly equivariant (TauCeti.MooreLiftingFunction.IsTransitive.transport_act).

Main definitions

• TauCeti.MooreReplacement.endpoint p: the endpoint map p' : E' → B.
• TauCeti.MooreReplacement.endpointLiftingFunction p: the transitive lifting function of p'.
• TauCeti.MooreReplacement.Fiber p b: the fibre F' of p' over b, with its right action of MooreLoopSpace B b.
• TauCeti.MooreReplacement.Fiber.map h hh: the equivariant map of fibres induced by a map h over B.
• TauCeti.MooreLiftingFunction.transport: transport F' → F along a lifting function.

Main results

• TauCeti.MooreReplacement.isHurewiczFibration_endpoint: p' is a Hurewicz fibration.
• TauCeti.MooreReplacement.homotopyEquiv: E ≃ₕ E', by the inclusion over B.
• TauCeti.MooreLiftingFunction.transportHomotopyEquiv: transport is a homotopy equivalence.
• TauCeti.MooreLiftingFunction.IsTransitive.transport_act: transport is strictly equivariant.

References

• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Morse homology with differential graded coefficients, Progress in Mathematics 360, Birkhäuser, 2025, §7.1 (after Dold and Kamps).

The endpoint map and its lifting function

def TauCeti.MooreReplacement.endpoint {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : C(MooreReplacement p, B)

The endpoint map p' : E' → B of the Moore-path replacement, (e, γ) ↦ γ.target.

@[simp]

theorem TauCeti.MooreReplacement.endpoint_apply {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (x : MooreReplacement p) : (endpoint p) x = x.path.target

noncomputable def TauCeti.MooreReplacement.liftPath {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (x : MooreReplacement p) (δ : MoorePath B) (h : δ.source = (endpoint p) x) : MoorePath (MooreReplacement p)

The lift of a path δ starting at the end point of (e, γ): the Moore path s ↦ (e, γ · δ|[0, s]) in the replacement, of the length of δ.

@[simp]

theorem TauCeti.MooreReplacement.liftPath_apply {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (x : MooreReplacement p) (δ : MoorePath B) (h : δ.source = (endpoint p) x) (s : NNReal) : (x.liftPath δ h).toContinuousMap s = mk x.point (x.path.trans (δ.truncate s) ⋯) ⋯

@[simp]

theorem TauCeti.MooreReplacement.length_liftPath {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (x : MooreReplacement p) (δ : MoorePath B) (h : δ.source = (endpoint p) x) : (x.liftPath δ h).length = δ.length

@[simp]

theorem TauCeti.MooreReplacement.source_liftPath {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (x : MooreReplacement p) (δ : MoorePath B) (h : δ.source = (endpoint p) x) : (x.liftPath δ h).source = x

@[simp]

theorem TauCeti.MooreReplacement.map_liftPath {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (x : MooreReplacement p) (δ : MoorePath B) (h : δ.source = (endpoint p) x) : MoorePath.map (endpoint p) (x.liftPath δ h) = δ

noncomputable def TauCeti.MooreReplacement.endpointLiftingFunction {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : MooreLiftingFunction (endpoint p)

The transitive lifting function of the endpoint map of the Moore-path replacement: concatenation, ((e, γ), δ) ↦ (s ↦ (e, γ · δ|[0, s])).

@[simp]

theorem TauCeti.MooreReplacement.endpointLiftingFunction_lift {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (x : MooreReplacement p) (δ : MoorePath B) (h : δ.source = (endpoint p) x) : (endpointLiftingFunction p).lift x δ h = x.liftPath δ h

theorem TauCeti.MooreReplacement.isTransitive_endpointLiftingFunction {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : (endpointLiftingFunction p).IsTransitive

The lifting function of the endpoint map is transitive.

theorem TauCeti.MooreReplacement.isHurewiczFibration_endpoint {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : IsHurewiczFibration ⇑(endpoint p)

The endpoint map of the Moore-path replacement is a Hurewicz fibration, whatever p is.

The inclusion and the projection

def TauCeti.MooreReplacement.incl {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : C(E, MooreReplacement p)

The inclusion E → E', e ↦ (e, const), a map over B.

@[simp]

theorem TauCeti.MooreReplacement.point_incl {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e : E) : ((incl p) e).point = e

@[simp]

theorem TauCeti.MooreReplacement.path_incl {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e : E) : ((incl p) e).path = MoorePath.refl (p e)

theorem TauCeti.MooreReplacement.endpoint_incl {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e : E) : (endpoint p) ((incl p) e) = p e

def TauCeti.MooreReplacement.proj {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : C(MooreReplacement p, E)

The projection E' → E, (e, γ) ↦ e.

@[simp]

theorem TauCeti.MooreReplacement.proj_apply {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (x : MooreReplacement p) : (proj p) x = x.point

@[simp]

theorem TauCeti.MooreReplacement.proj_comp_incl {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : (proj p).comp (incl p) = ContinuousMap.id E

def TauCeti.MooreReplacement.shrinkHomotopy {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : ((incl p).comp (proj p)).Homotopy (ContinuousMap.id (MooreReplacement p))

The homotopy from incl ∘ proj to the identity of E', shrinking each path to its start: (s, (e, γ)) ↦ (e, γ|[0, s · γ.length]).

@[simp]

theorem TauCeti.MooreReplacement.point_shrinkHomotopy {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) (y : ↑unitInterval × MooreReplacement p) : ((shrinkHomotopy p) y).point = y.2.point

@[simp]

theorem TauCeti.MooreReplacement.path_shrinkHomotopy {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) (y : ↑unitInterval × MooreReplacement p) : ((shrinkHomotopy p) y).path = y.2.path.truncate (unitInterval.toNNReal y.1 * y.2.path.length)

def TauCeti.MooreReplacement.homotopyEquiv {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : ContinuousMap.HomotopyEquiv E (MooreReplacement p)

The inclusion E → E' is a homotopy equivalence, with homotopy inverse the projection.

@[simp]

theorem TauCeti.MooreReplacement.coe_homotopyEquiv {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : ⇑(homotopyEquiv p).toFun = ⇑(incl p)

@[simp]

theorem TauCeti.MooreReplacement.coe_homotopyEquiv_symm {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : ⇑(homotopyEquiv p).symm.toFun = ⇑(proj p)

The fibre and the action of the Moore loops

def TauCeti.MooreReplacement.Fiber {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) (b : B) : Type (max u v)

The fibre F' of the endpoint map over b: the pairs (e, γ) with γ ending at b.

@[instance_reducible]

instance TauCeti.MooreReplacement.Fiber.instTopologicalSpace {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} : TopologicalSpace (Fiber p b)

def TauCeti.MooreReplacement.Fiber.val {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} (x : Fiber p b) : MooreReplacement p

The underlying pair of a point of the fibre.

theorem TauCeti.MooreReplacement.Fiber.val_eq_subtypeVal {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} (x : Fiber p b) : x.val = ↑x

The underlying pair of a point of the fibre is its value as an element of the subtype.

@[simp]

theorem TauCeti.MooreReplacement.Fiber.target_path_val {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} (x : Fiber p b) : x.val.path.target = b

theorem TauCeti.MooreReplacement.Fiber.ext {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} {x y : Fiber p b} (h : x.val = y.val) : x = y

theorem TauCeti.MooreReplacement.Fiber.ext_iff {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} {x y : Fiber p b} : x = y ↔ x.val = y.val

theorem TauCeti.MooreReplacement.Fiber.continuous_val {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} : Continuous val

def TauCeti.MooreReplacement.Fiber.mk' {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} (x : MooreReplacement p) (h : x.path.target = b) : Fiber p b

The point (e, γ) of the fibre, for a pair whose path ends at b.

@[simp]

theorem TauCeti.MooreReplacement.Fiber.val_mk' {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} (x : MooreReplacement p) (h : x.path.target = b) : (mk' x h).val = x

noncomputable def TauCeti.MooreReplacement.Fiber.act {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} (x : Fiber p b) (ω : MooreLoopSpace B b) : Fiber p b

The right action of a Moore loop ω at b on the fibre: (e, γ) · ω = (e, γ · ω).

@[simp]

theorem TauCeti.MooreReplacement.Fiber.point_act {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} (x : Fiber p b) (ω : MooreLoopSpace B b) : (x.act ω).val.point = x.val.point

@[simp]

theorem TauCeti.MooreReplacement.Fiber.path_act {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} (x : Fiber p b) (ω : MooreLoopSpace B b) : (x.act ω).val.path = x.val.path.trans ω.toMoorePath ⋯

@[simp]

theorem TauCeti.MooreReplacement.Fiber.act_one {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} (x : Fiber p b) : x.act 1 = x

The constant loop of length zero acts as the identity on the fibre.

@[simp]

theorem TauCeti.MooreReplacement.Fiber.act_mul {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} (x : Fiber p b) (ω ω' : MooreLoopSpace B b) : x.act (ω * ω') = (x.act ω).act ω'

The action is a right action: acting by ω * ω' is acting by ω, then by ω'.

theorem TauCeti.MooreReplacement.Fiber.continuous_act {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} : Continuous fun (q : Fiber p b × MooreLoopSpace B b) => q.1.act q.2

The action is continuous in both variables.

@[instance_reducible]

noncomputable instance TauCeti.MooreReplacement.Fiber.instMulActionMulOppositeMooreLoopSpace {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} : MulAction (MooreLoopSpace B b)ᵐᵒᵖ (Fiber p b)

The strict right action of the Moore loops at b on the fibre F', as a left action of the opposite monoid.

@[simp]

theorem TauCeti.MooreReplacement.Fiber.op_smul_eq_act {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} (x : Fiber p b) (ω : MooreLoopSpace B b) : MulOpposite.op ω • x = x.act ω

instance TauCeti.MooreReplacement.Fiber.instContinuousSMulMulOppositeMooreLoopSpace {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} : ContinuousSMul (MooreLoopSpace B b)ᵐᵒᵖ (Fiber p b)

Transport along a lifting function

def TauCeti.MooreLiftingFunction.fiberAct {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (b : B) (f : { e : E // p e = b }) (ω : MooreLoopSpace B b) : { e : E // p e = b }

The action of a Moore loop ω at b on the fibre of p over b through a lifting function: f · ω = Φ (f, ω)(end). It is a strict action when Φ is transitive.

@[simp]

theorem TauCeti.MooreLiftingFunction.coe_fiberAct {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (b : B) (f : { e : E // p e = b }) (ω : MooreLoopSpace B b) : ↑(Φ.fiberAct b f ω) = (Φ.lift (↑f) ω.toMoorePath ⋯).target

theorem TauCeti.MooreLiftingFunction.continuous_fiberAct {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (b : B) : Continuous fun (q : { e : E // p e = b } × MooreLoopSpace B b) => Φ.fiberAct b q.1 q.2

The action through a lifting function is continuous in both variables.

@[simp]

theorem TauCeti.MooreLiftingFunction.fiberAct_one {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (b : B) (f : { e : E // p e = b }) : Φ.fiberAct b f 1 = f

The unit loop acts trivially, for any lifting function: the lift of a path of length zero is constant.

theorem TauCeti.MooreLiftingFunction.IsTransitive.fiberAct_mul {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {Φ : MooreLiftingFunction p} (hΦ : Φ.IsTransitive) (b : B) (f : { e : E // p e = b }) (ω ω' : MooreLoopSpace B b) : Φ.fiberAct b f (ω * ω') = Φ.fiberAct b (Φ.fiberAct b f ω) ω'

For a transitive lifting function, the action of the Moore loops on the fibre is a right action: acting by ω * ω' is acting by ω, then by ω'.

@[reducible, inline]

abbrev TauCeti.MooreLiftingFunction.IsTransitive.mulAction {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {Φ : MooreLiftingFunction p} (hΦ : Φ.IsTransitive) (b : B) : MulAction (MooreLoopSpace B b)ᵐᵒᵖ { e : E // p e = b }

The strict right action of the Moore loops at b on the fibre of p over b, through a transitive lifting function.

theorem TauCeti.MooreLiftingFunction.IsTransitive.continuousSMul {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {Φ : MooreLiftingFunction p} (hΦ : Φ.IsTransitive) (b : B) : ContinuousSMul (MooreLoopSpace B b)ᵐᵒᵖ { e : E // p e = b }

The action through a transitive lifting function is continuous.

def TauCeti.MooreLiftingFunction.transport {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (b : B) : C(MooreReplacement.Fiber p b, { e : E // p e = b })

Transport along a lifting function, from the fibre F' of the Moore-path replacement to the fibre F of p over b: (e, γ) ↦ Φ (e, γ)(end).

@[simp]

theorem TauCeti.MooreLiftingFunction.coe_transport {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (b : B) (x : MooreReplacement.Fiber p b) : ↑((Φ.transport b) x) = (Φ.lift x.val.point x.val.path ⋯).target

theorem TauCeti.MooreLiftingFunction.IsTransitive.transport_act {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {Φ : MooreLiftingFunction p} (hΦ : Φ.IsTransitive) (b : B) (x : MooreReplacement.Fiber p b) (ω : MooreLoopSpace B b) : (Φ.transport b) (x.act ω) = Φ.fiberAct b ((Φ.transport b) x) ω

Transport is strictly equivariant for the actions of the Moore loops, when the lifting function is transitive.

def TauCeti.MooreLiftingFunction.fiberIncl {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) (b : B) : C({ e : E // p e = b }, MooreReplacement.Fiber p b)

The inclusion of the fibre of p into the fibre F', f ↦ (f, const).

@[simp]

theorem TauCeti.MooreLiftingFunction.val_fiberIncl {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (b : B) (f : { e : E // p e = b }) : ((fiberIncl p b) f).val = (MooreReplacement.incl p) ↑f

@[simp]

theorem TauCeti.MooreLiftingFunction.transport_comp_fiberIncl {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (b : B) : (Φ.transport b).comp (fiberIncl p b) = ContinuousMap.id { e : E // p e = b }

def TauCeti.MooreLiftingFunction.transportHomotopy {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (b : B) : (ContinuousMap.id (MooreReplacement.Fiber p b)).Homotopy ((fiberIncl p b).comp (Φ.transport b))

The homotopy from the identity of F' to fiberIncl ∘ transport: at time s, lift the first part γ|[0, u] of the path, u = s · γ.length, and keep the rest γ|[u, γ.length].

@[simp]

theorem TauCeti.MooreLiftingFunction.point_val_transportHomotopy {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (b : B) (y : ↑unitInterval × MooreReplacement.Fiber p b) : ((Φ.transportHomotopy b) y).val.point = (Φ.lift y.2.val.point (y.2.val.path.truncate (unitInterval.toNNReal y.1 * y.2.val.path.length)) ⋯).target

@[simp]

theorem TauCeti.MooreLiftingFunction.path_val_transportHomotopy {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (b : B) (y : ↑unitInterval × MooreReplacement.Fiber p b) : ((Φ.transportHomotopy b) y).val.path = y.2.val.path.drop (unitInterval.toNNReal y.1 * y.2.val.path.length)

def TauCeti.MooreLiftingFunction.transportHomotopyEquiv {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (b : B) : ContinuousMap.HomotopyEquiv (MooreReplacement.Fiber p b) { e : E // p e = b }

Transport is a homotopy equivalence from the fibre F' of the Moore-path replacement to the fibre of p, with homotopy inverse f ↦ (f, const).

@[simp]

theorem TauCeti.MooreLiftingFunction.coe_transportHomotopyEquiv {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (b : B) : ⇑(Φ.transportHomotopyEquiv b).toFun = ⇑(Φ.transport b)

@[simp]

theorem TauCeti.MooreLiftingFunction.coe_transportHomotopyEquiv_symm {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (b : B) : ⇑(Φ.transportHomotopyEquiv b).symm.toFun = ⇑(fiberIncl p b)

Naturality of the fibre in maps over the base

def TauCeti.MooreReplacement.Fiber.map {E : Type u_1} {E' : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {p' : C(E', B)} {b : B} (h : C(E, E')) (hh : p'.comp h = p) : C(Fiber p b, Fiber p' b)

The map of fibres of the Moore-path replacements induced by a map h : E → E' over B: (e, γ) ↦ (h e, γ).

@[simp]

theorem TauCeti.MooreReplacement.Fiber.point_map {E : Type u_1} {E' : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {p' : C(E', B)} {b : B} (h : C(E, E')) (hh : p'.comp h = p) (x : Fiber p b) : ((map h hh) x).val.point = h x.val.point

@[simp]

theorem TauCeti.MooreReplacement.Fiber.path_map {E : Type u_1} {E' : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {p' : C(E', B)} {b : B} (h : C(E, E')) (hh : p'.comp h = p) (x : Fiber p b) : ((map h hh) x).val.path = x.val.path

theorem TauCeti.MooreReplacement.Fiber.map_act {E : Type u_1} {E' : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {p' : C(E', B)} {b : B} (h : C(E, E')) (hh : p'.comp h = p) (x : Fiber p b) (ω : MooreLoopSpace B b) : (map h hh) (x.act ω) = ((map h hh) x).act ω

The induced map of fibres commutes with the action of the Moore loops.

@[simp]

theorem TauCeti.MooreReplacement.Fiber.map_id {E : Type u_1} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {b : B} : map (ContinuousMap.id E) ⋯ = ContinuousMap.id (Fiber p b)

The identity induces the identity of fibres.

theorem TauCeti.MooreReplacement.Fiber.map_comp {E : Type u_1} {E' : Type u_2} {E'' : Type u_3} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace E''] [TopologicalSpace B] {p : C(E, B)} {p' : C(E', B)} {p'' : C(E'', B)} {b : B} (h : C(E, E')) (h' : C(E', E'')) (hh : p'.comp h = p) (hh' : p''.comp h' = p') : map (h'.comp h) ⋯ = (map h' hh').comp (map h hh)

A composite of maps over B induces the composite of the maps of fibres.