Headline results
Quoted from the headline results in README.md of FormalFrontier/fundamental-groupoids at commit ce38a38f, Apache-2.0.
Evaluation and target refinement of compact-open mapping spaces. For
UCompactlyGeneratedSpace.{u} A and arbitrary Y, the spaces
κ_u C(A, κ_u Y) and κ_u C(A, Y) are canonically homeomorphic, with independent
probe and carrier universes. The forward map is refined counit postcomposition,
the inverse retains each function, and both maps are natural in the target;
no local compactness of A or separation or generatedness of Y is assumed.
For arbitrary A and Y, point evaluation κ_u (C(A, Y) × A) → Y is continuous,
with ordinary compact-open and product topologies inside the refinement.
See evaluation and the mapping-space comparison.
DefinitionCompactly generated compact-open currying#
For original UCompactlyGeneratedSpace.{u} spaces P and A and any
topological space Y, currying is a homeomorphism
κ_u C_co(κ_u (P × A), Y) ≃ₜ κ_u C_co(P, κ_u C_co(A, Y)).
Here C_co has the ordinary compact-open topology and κ_u denotes refinement
by compact Hausdorff probes in universe u. The product uses the original
factor topologies, and the right-hand compact-open space uses the refined
inner mapping space as target. The probe and all three carrier universes are
independent, with no local compactness or separation hypotheses. Its whole
underlying equivalence is
ContinuousMap.compactlyGeneratedCurryEquiv.
Quoted from the headline results in README.md of FormalFrontier/fundamental-groupoids at commit ce38a38f, Apache-2.0.
Lean
Homeomorph.compactlyGeneratedCurry(def), declared in FundamentalGroupoids/Topology/CompactOpen/CompactlyGeneratedCurryHomeomorph.lean, line 70.
Read from the source at commit ce38a38f, without running Lean.
Sources
The ordinary based loop functor and based homotopy. The compact-open loop
space Path x x, based at its constant loop, is functorial for strict based maps.
A homotopy relative to the selected point induces a jointly continuous homotopy
of loop maps fixing the whole constant loop, with no local compactness or
separation assumptions on the original spaces. The loop functor descends uniquely
to the category of based-homotopy classes, with a strict commuting triangle.
Based homotopy inverses give an isomorphism there whose two arrows are the classes
of the corresponding loop maps. See
Based.Loop.
Generated-by subspaces. For any family of generating spaces and any subset of an arbitrary space, the generated-by refinement of the original subspace is canonically homeomorphic to the generated-by refinement of the counit-preimage inside the refined ambient space. The comparison is natural for continuous ambient maps preserving the subsets. For a closed subset, the outer refinement can be omitted when closed subspaces of the generating spaces are generated by the same family. The compact Hausdorff family recovers the existing fixed-universe compactly generated topology, with independent probe and carrier universes. See the subspace comparison and the compact Hausdorff bridges.
Components of a covering homotopy fiber. For a covering map f : C(E, B)
and b : B, ContinuousMap.HomotopyFiber.zerothHomotopyHomeomorphFiber identifies
ZerothHomotopy (HomotopyFiber f b), with its quotient topology, homeomorphically
with the strict subtype fiber {e : E // f e = b}. The comparison evaluates
point classes using the fiber retraction, and its inverse takes the class of the
constant-path inclusion. It is natural in continuous commuting squares between
coverings, including empty fibers, with independent universes and no covering
assumptions on the horizontal maps. See path components of covering fibers.
Homotopy invariance of ordinary homotopy fibers. For topological spaces E and
B, continuous maps f g : C(E, B), a specified homotopy
H : ContinuousMap.Homotopy f g, and any b : B,
ContinuousMap.HomotopyFiber.homotopyEquiv H b constructs an unbased
homotopy equivalence HomotopyFiber f b ≃ₕ HomotopyFiber g b. The forward map
retains the E-point and appends the path traced by H after the whole supplied
path; the inverse appends its reverse. The named inverse homotopies retain the
E-point at every time. No separation or local-compactness assumptions on E or
B are required. See homotopy invariance.
Strict fibers of covering maps (Fiber.Covering).
For f : C(E, B) with cov : IsCoveringMap f and any b : B,
HomotopyFiber.fiberHomotopyEquiv cov is the canonical homotopy equivalence
from {e : E // f e = b} to HomotopyFiber f b. Its forward map uses the
constant path, its inverse lifts the reversed retained path, and the homotopy
fixes every included strict-fiber point throughout. The source and target
universes are independent; no separation, local compactness or surjectivity
assumption is required.
The naturality module
intertwines the original inclusion, whole reverse-path lift, retraction and
whole fixing deformation under continuous commuting squares, preserving the
strict subtype fibers and the complete retained paths. Inclusion and reversed-path
family naturality need no covering hypotheses; lift, retraction and deformation
naturality require only that the two vertical maps are coverings, not the horizontal
maps. The four space universes are independent, with no connectedness, local
compactness, separation or nonempty-fiber assumptions. The independent
homotopy-lift naturality module
gives postcomposition naturality of Mathlib's canonical lift for any topological
parameter space, in a fifth independent universe, under the same covering floor.
Point-wide-pushout coproducts up to based homotopy (Based.Coproducts).
A family D : J → BasedTopCat.{max u w}, indexed by J : Type w, has a
point-wide-pushout cofan with explicit descent and uniqueness, both in based
spaces and after quotienting based maps by homotopies fixing the point at
every time. Two based maps from this wedge represent the same class exactly
when all factor restrictions do. The colimit data retain the mapped composite
diagram; the binary specialization uses its explicit comparison isomorphism.
Empty families give initial objects. No separation, local compactness of the
spaces, finiteness of the index, or condition on the basepoints is required.
Strict ordered finite-wedge comparisons (Based.FiniteWedge).
For D : Fin 2 → BasedTopCat.{u}, the finite wedge is isomorphic in based
spaces to the binary wedge, sending 0 to the left and 1 to the right.
For D : Fin 3 → BasedTopCat.{u}, both nested binary wedges flatten
isomorphically to the three-factor wedge, preserving leaf order 0, 1, 2.
Forward and inverse leg equations and common-point preservation characterize
the comparisons. The factors may differ in an arbitrary common universe,
without separation, connectedness, local compactness or basepoint conditions.
The existing homotopyQuotient.mapIso gives their based-homotopy images.
Chosen finite products in the opposite based-homotopy category (Based.Cartesian).
The ordinary opposite of BasedTopCat.HomotopyCategory has explicit terminal
and binary limit cones, given by the opposite empty and ordered two-factor
based wedges. The named cartesian monoidal structure uses these choices;
its unit, tensor, two projections and map to the unit have characteristic
equations. The projections preserve the left/right order of the wedge
inclusions. For D : Fin 3 → BasedTopCat.{u}, the unop of the associator
followed by the quotient image of left-nested flattening equals the quotient
image of right-nested flattening, preserving the ordered leaves 0, 1, 2.
No global cartesian or monoidal instance is installed.
Point-family maps and universe lifting (WidePushout.PointMap,
WidePushout.ULift,
Based.ULift).
Point-preserving maps between independently sized families on the same index
type descend through their point-wide-pushouts, preserving identities and
composition. For J : Type w and X : J → TopCat.{max u w} with chosen points,
the universe lift of its point-wide-pushout is homeomorphic to the
point-wide-pushout of its lifted factors, with head, factor and inverse
evaluation laws. Based at the
lifted head, this gives an isomorphism with the based wedge of the lifted
pointed factors. Empty families retain the head. No separation or local
compactness is needed; the point-family and homeomorphism modules are
independent of based-homotopy constructions.
Wide-pushout continuity and homotopy descent (Limits.Products,
Limits.WidePushout,
Homotopy.WidePushout).
A supplied topological colimit has its characteristic continuity criterion after
product with P for maps to Y under LocallyCompactPair P Y, with independent
indexing-object, indexing-morphism, diagram, parameter and target universes.
Wide pushouts of arbitrary continuous attaching maps have a quotient comparison
and continuous descent to independently universed targets, with head, factor and
uniqueness equations. Compatible jointly continuous families and HomotopyLike
data descend with their prescribed restrictions at every time. For a point head,
chosen-point-relative factor homotopies and explicit equality of endpoint maps
at the head give a unique head-relative homotopy. Empty index families are
included; no separation or local compactness of the factors or target is required.
Unpointed disk attachments (DiskAttachment).
Arbitrary families of circle maps attach closed complex unit disks, with no
connectedness or separation assumptions. The continuous-map universal property
allows independent universes. Continuity on an open or closed subset is tested
on its preimages in the original space and each disk, without continuity elsewhere.
Compatible functions have a unique descent to any target type, without a
continuity requirement; continuous descent has the same underlying function.
Empty attachments recover the original space; attaching along the identity of the
boundary recovers the disk. The original inclusion is a closed embedding, and the
open-disk characteristic maps are open embeddings with mutually disjoint images
avoiding the original space. Every attaching
boundary circle induces a trivial fundamental-group homomorphism at every basepoint.
Punctured disk attachments (Punctured,
PuncturedRetraction).
For any topological space and arbitrary unbased attaching maps, the disk centres
form a closed set. Their complement strongly deformation retracts onto the
original-space image, fixing that image throughout. On each punctured disk,
the retraction follows its unit direction and the deformation is radial.
Space and disk-index universes are independent; no connectivity, separation
or finiteness assumptions are needed.
The punctured part of an attachment path component
retracts to the corresponding original-space component through a relative
deformation. Its fundamental group
is isomorphic to that of the original space, with forward map induced by
retraction followed by component inclusion. The inverse lifts to the
original-space component and then includes it into the punctured component.
Neither component is assumed open.
For a selected attaching map taking 1 to the chosen point, its
thickened chart
is path connected, with a contractible open-disk piece and punctured-open-disk
overlap with the core. The positive radial-whiskered half-radius loop maps to
the positive attaching loop class under the retraction isomorphism
(generator comparison).
Restriction to the core
identifies homomorphisms from the chart fundamental group with core
homomorphisms killing that selected generator, for an arbitrary target group
in an independent universe. Both directions restrict along the same inclusion
at the component basepoint.
When every attaching map takes 1 to the chosen point, the core and charts
give an Option-indexed open cover
of the attachment component, with common core intersection, path-connected
members and pairwise intersections. This includes the empty disk family.
Homomorphisms from the attachment fundamental group
correspond to homomorphisms from the original fundamental group killing all
positive attaching loop classes, for any target group in an independent universe.
The forward map restricts along the original-space inclusion, and the inverse
restricts back to the supplied homomorphism along that same inclusion.
The inclusion-induced homomorphism
is surjective, with kernel the normal closure of the positive attaching loop
classes. Its induced quotient isomorphism commutes with the inclusion-induced
homomorphism and the quotient projection in both directions.
Endomorphism transport (Conjugation).
In any category, transports along α β : X ≅ Y agree iff
α.hom ≫ β.inv is central in End X. Commutativity makes transport independent;
in a groupoid the converse holds for a fixed explicitly isomorphic target.
Loop transport agrees with Mathlib's MulAut.conj.
Chosen vertex group (SingleObj).
For a chosen object x in a preconnected groupoid,
SingleObj.functor (MonoidHom.id (End x)) is an equivalence; it is full and
faithful in every category, without preconnectedness.
Categorical monodromy and preconnectedness (Covering).
A quiver-covering functor E ⥤ B between categories gives a canonical left
Aut b-action on its fiber. It is pretransitive if E is a preconnected
groupoid. Conversely, for preconnected groupoid base B, pretransitivity on
one specified fiber implies preconnectedness of the total category E.
All four universes are independent; no nonempty fiber or surjectivity is needed.
Categories of elements (Elements).
For a type-valued functor on any category, strict object fibers recover its
values. Given a covering proof, lift targets and monodromy agree with the
functor action; for a groupoid base the projection is a quiver covering.
The three universes are independent, with no nonemptiness or connectedness.
Components as type colimits (ConnectedComponents).
For any X : C ⥤ Type w, ConnectedComponents X.Elements ≃ X.ColimitType,
naturally and on representatives, with independent object, morphism and value
universes and no smallness, nonemptiness or connectivity assumptions. An individual
HasColimit X instance gives the comparison with Limits.colimit X instead.
Path connectedness (Connected).
A space is path connected iff its fundamental groupoid is connected, including
nonemptiness on both sides; no local path connectedness or separation is needed.
Pointlike path components (FundamentalGroupoid.Discrete,
Connected.ZerothHomotopy).
If every path component is a subsingleton, the fundamental groupoid is canonically
equivalent to the discrete category on the same points, and evaluation identifies
ZerothHomotopy X homeomorphically with X in its original topology. The inverse
maps are the point inclusion and continuous class map. Both comparisons commute
with continuous maps and specialize to totally disconnected spaces, including
discrete spaces. No basepoint or nonemptiness assumption is required; categorical
discreteness does not assert that the topology on X is discrete.
Maps on path components (PathConnected).
Every continuous map induces ZerothHomotopy.map, preserving representatives,
identity and composition; homotopic maps induce equal functions. Space universes
are independent, with no separation or connectedness assumptions.
Cube boundaries (Cube).
For any index type N with at least two elements, the coordinate-face boundary of
N → I is path connected, even for infinite N. The zero vertex lies in the
boundary whenever N is nonempty. For finite N, the boundary is closed,
including the empty-index cube.
Real coordinates on cube-boundary complements (Cube.Coordinates).
For every index type N in any universe, Cube.boundaryComplHomeomorphPi N
identifies the boundary complement, with its subtype topology, with the product
N → ℝ. Each coordinate is increasing, using t ↦ 2 * t - 1 followed by the
inverse of Mathlib's orderIsoIooNegOneOne ℝ; forward and inverse evaluation
laws are public. A theorem supplies local compactness for finite N.
Empty and infinite indices are allowed; for infinite cubes this is not an
ambient-interior description.
Open-subspace collapse (OnePoint.Collapse).
For a Hausdorff space K and any open subspace s, OnePoint.collapse s
continuously retains the points of s and sends its complement to infinity
in OnePoint s, without local compactness of K. The extension
OnePoint.collapseWithPoint s from K ⊕ PUnit is surjective even when s is
the whole space; for compact K it is a quotient map, giving continuous descent
through Mathlib's quotient-map API to arbitrary topological targets. Neither
nonemptiness nor properness of s is required.
Based compact-open collapse comparison (OnePoint.ContinuousMap).
For a compact Hausdorff space K, any open s and any topological space X
with a chosen x : X, OnePoint.collapsePullbackHomeomorph s x identifies
{F : C(OnePoint s, X) // F ∞ = x} homeomorphically with continuous maps
K → X equal to x outside s. The forward map precomposes with
OnePoint.collapse s; the inverse is OnePoint.rec x applied to restriction
to s. Both spaces carry the ordinary compact-open/subtype topology.
Ambient and target universes are independent; s may be empty or all of K,
and X needs neither separation nor local compactness. The construction uses
GroupTheory's compact-covering precomposition embedding API.
Ordinary compact-open paths and homotopy fibers (RelativePathSpace,
Fiber,
Fiber.Const,
Fiber.Contractible,
Fiber.Homeomorph,
Fiber.PathComponent,
Fiber.Prod,
RelativePathSpace.Contractible).
ContinuousMap.RelativePathSpace b A consists of paths from an arbitrary b
to any point of A; the paths need not stay in A, and b need not lie in A.
ContinuousMap.HomotopyFiber f b retains both a source point e and a path
from b to f e, with the ordinary product/subtype compact-open topology.
It is homeomorphic to the pullback of f along terminal evaluation. For an
embedding, forgetting e identifies it with paths ending in Set.range f;
for the original subspace inclusion, the endpoint lies in A itself.
Maps act on both point and path, with identity, composition, constant and
naturality laws. A commuting square of source and target homeomorphisms
induces HomotopyFiber.homeomorph eX eY w hy at specified points satisfying
hy : eY y = y'. Its inverse uses the inverse coordinate homeomorphisms;
its forward map sends the retained point through eX and postcomposes the
whole path by eY, with identity, composition and projection laws.
All four space universes are independent, without embedding, separation or
nonemptiness assumptions.
HomotopyFiber.prodHomeomorph f g y z splits the fiber of a product map
over (y, z) into the product of the two fibers, retaining both source points
and entire paths. Its inverse pairs paths at the same original time. The
comparison commutes with both projections and is natural for two arbitrary
continuous squares, with eight independent universes and no separation or
ambient local-compactness assumptions.
HomotopyFiber.compFstHomeomorph (Z := Z) f b identifies the fiber of
f.comp (ContinuousMap.fst : C(X × Z, X)) over b with
HomotopyFiber f b × Z. It preserves both source coordinates and the full
original path, with forward and inverse same-time evaluation and constructor
laws. Whole continuous-map diagrams describe the first-fiber, free-coordinate,
point and path projections. Naturality permits any continuous commuting square
and any continuous map of the free factor, with six independent universes;
the comparison itself uses three independent universes and arbitrary topologies.
Empty spaces are allowed. For f = id, the full identity-fiber factor remains;
this is not a homeomorphism from the projection's fiber to Z alone.
A constant fiber point needs a specified e with f e = b;
being outside the image does not force the homotopy fiber to be empty.
For arbitrary f, nonemptiness is equivalent to ∃ e, Joined b (f e), or
to membership of ZerothHomotopy.mk b in the range of ZerothHomotopy.map f.
The induced path-component map is therefore surjective exactly when every
homotopy fiber is nonempty. Source and target universes are independent,
without connectivity assumptions. The retained-point projection has path-component
image equal to the preimage of {ZerothHomotopy.mk b} under
ZerothHomotopy.map f; no injectivity of the component projection is asserted.
For a constant map with value c, HomotopyFiber.constHomeomorph E b c
identifies its fiber with E × Path b c, retaining the point and every path
value, naturally in continuous source maps. The fiber is nonempty exactly when
both factors are nonempty; an empty source and the full loop factor for b = c
are included, with independent source and target universes.
For every topological space X and chosen b : X,
RelativePathSpace.contraction b sends γ to t ↦ γ ((1 - s) * t) at time
s, fixes the constant path throughout, and gives a ContractibleSpace
instance on RelativePathSpace b Set.univ. Its endpoint is free to move.
HomotopyFiber.idContraction b transports this to the identity map's homotopy
fiber, giving a ContractibleSpace instance and fixing its constant-path point.
At time s, the retained source point is γ (1 - s) and the whole path is
t ↦ γ ((1 - s) * t), with its original direction and starting point.
No target separation or local compactness is required. These are ordinary,
non-kified spaces, not an identification with May's category U; this contracts
neither loop spaces nor X.
Homotopy-fiber exactness (Based.HomotopyFiber.Exact,
Fiber.Exact).
For f : C(E, B), e₀ : E, b : B and h : f e₀ = b, base
HF = ContinuousMap.HomotopyFiber f b at its constant-path point, and let
p retain the source point.
For any original based source (Z, z₀), write
[Z, X]_* for the whole hom-set in BasedTopCat.HomotopyCategory:
Under(TopCat.of PUnit) modulo homotopy relative to {z₀}, not the under
category of an unbased homotopy category. Put ΩE = Path e₀ e₀ and
ΩB = Path b b, based at their constant loops; let J : ΩB → HF retain
e₀ and the whole forward loop, and let Ωf : ΩE → ΩB apply f pointwise.
With k_* denoting based postcomposition and c_X the constant class in
[Z, X]_*, the three identities are
range p_* = f_* ⁻¹' {c_B} in [Z, E]_*,
range J_* = p_* ⁻¹' {c_E} in [Z, HF]_*,
range (Ωf)_* = J_* ⁻¹' {c_HF} in [Z, ΩB]_*.
They are
BasedTopCat.range_homotopyFiberProjection,
BasedTopCat.range_homotopyFiberLoopInclusion, and
BasedTopCat.range_homotopyFiberLoopMap.
The original carriers Z, E, B have independent universes. Ordinary
ULift puts the original source, fiber and loop-space models in the common
universe max uZ uE uB, with their ordinary product/subtype/compact-open
topologies transported unchanged. In Based.Universe,
BasedTopCat.exists_homotopyQuotient_map_ofHomULift_eq supplies original-space
representatives for every lifted quotient morphism, and
BasedTopCat.homotopyQuotient_map_ofHomULift_eq_iff characterizes equality by
homotopy relative to {z₀}. No commutation of lifting with fibers or loops
is used.
No local compactness, separation, closed-basepoint or fibration hypotheses
are imposed. The displayed Ωf is unsigned, distinct from May's signed arrow.
These are pointed-set identities, not identifications with components of
arbitrary mapping spaces or a signed, kified or group-valued long exact sequence.
For every cube index N,
HomotopyGroup.range_mapFun_homotopyFiber_point gives
range (π_N p) = (π_N f) ⁻¹' {constant class}, where π_N denotes
HomotopyGroup.mapFun with these point equations. No index instances are
needed. With [DecidableEq N] [Nonempty N],
HomotopyGroup.range_map_homotopyFiber_point gives the range–kernel form
for the existing groups and homomorphisms. These instances supply operation
data, not geometric assumptions. Index and space universes are independent,
and all topologies are arbitrary.
For the adjacent cubical position, J : C(Path b b, HF) is the continuous
composite through HomotopyFiber.constHomeomorph Unit b b and
HomotopyFiber.map, retaining e₀ and the whole forward loop γ.
It sends Path.refl b to HomotopyFiber.const e₀ h; only the pointwise
equation h is required, not constancy of f.
HomotopyGroup.range_mapFun_homotopyFiber_loop gives
range (π_N J) = (π_N p) ⁻¹' {constant class} for every N, again without
index instances. This is exactness at
HomotopyGroup N HF (HomotopyFiber.const e₀ h).
With [DecidableEq N] [Nonempty N],
HomotopyGroup.range_map_homotopyFiber_loop gives the subgroup range–kernel
form for the same maps. The empty-index consequence
ZerothHomotopy.range_map_homotopyFiber_loop is
range (π₀ J) = (π₀ p) ⁻¹' {ZerothHomotopy.mk e₀} on all path components
of the ordinary topological loop space Path b b, not just the component
of Path.refl b. The unpointed zeroth projection formula also allows
empty E, without choosing e₀ or h.
At the base-space position, HomotopyGroup.Fiber
identifies the image of π_(N ⊕ Unit) f with the preimage of the constant
class under inverse loop iteration, the singleton-loop homeomorphism and π_N J.
This holds for every N, with the subgroup range–kernel form for
[DecidableEq N] [Nonempty N]; the sum order is N followed by Unit,
and the whole forward path is retained without reversal.
For continuous g : C(E', B) and u : C(E', E) with f (u x) = g x,
the induced fiber map K over id B satisfies
range (π₀ K) = (π₀ p) ⁻¹' range (π₀ u); E' may be empty.
The loop-class map δ : π₁B → π₀HF retains the whole forward loop at e₀,
with image (π₀ p) ⁻¹' {ZerothHomotopy.mk e₀} and
δ ⁻¹' {δ 1} = Set.range (FundamentalGroup.mapOfEq f h).
These are the positions at π₀HF and π₁B, distinct from projection
exactness at HomotopyGroup N E e₀. No group structure on π₀HF is supplied.
The arbitrary-source based identities and finite-degree exactness formulas adapt
May, Chapter 8 §6, printed pp. 61–62; the all-index statements are ordinary-topology
cubical extensions, without a sphere-domain comparison or identification with
his signed degree-indexed sequence or category U. See the
exactness guide.
Pointed homotopy-fiber sequences and positive-degree exactness (HomotopyGroup.Fiber.Sequence,
Sequence.Exact).
For arbitrary topological spaces E, B, f : C(E, B), b : B, e₀ : E
and h : f e₀ = b, let HF = HomotopyFiber f b, based at
HomotopyFiber.const e₀ h. The construction
S = HomotopyGroup.homotopyFiberSequence f b e₀ h : ChainComplex Pointed ℕ
has terms identified with ULifts of πₙB, πₙE, πₙHF in degrees
3n, 3n + 1, 3n + 2, where πₙ uses HomotopyGroup (Fin n).
Only quotient carriers are lifted into a common ambient universe; the spaces
retain their independent universes. Zero morphisms are constant pointed maps.
The differentials are based postcomposition by f, fiber projection, and
the connecting function from πₙ₊₁B to πₙHF.
GenLoop.homotopyFiberConnecting n f b e₀ h p retains e₀ and the whole
forward path t ↦ p (Fin.snoc a t) at each outer coordinate a.
The term isomorphisms homotopyFiberSequenceBaseIso,
homotopyFiberSequenceTotalIso, homotopyFiberSequenceFiberIso and the
differential laws homotopyFiberSequence_d_base_apply,
homotopyFiberSequence_d_total_apply, homotopyFiberSequence_d_fiber_class
expose these descriptions without unfolding the complex; the first two
differentials also have _class laws on representatives.
HomotopyGroup.homotopyFiberSequence_exact states, for every n : ℕ,
Set.range (S.d (n + 2) (n + 1)).toFun =
(S.d (n + 1) n).toFun ⁻¹' {(S.X n).point}
This is pointed-set exactness at all positive chain degrees. The lemmas
homotopyFiberSequence_exact_total, homotopyFiberSequence_exact_fiber,
homotopyFiberSequence_exact_base give the positions 3n + 1, 3n + 2,
3n + 3, respectively. The incoming differential need not surject onto the
terminal term π₀B.
A strict continuous square preserving the specified points induces
HomotopyGroup.homotopyFiberSequenceMap, with four independent space
universes and a common ambient lift universe. Its _base_apply,
_total_apply, _fiber_apply laws describe the components, and _id,
_comp give identity and composition laws. The all-index connecting-map
naturality theorem is HomotopyGroup.mapFun_homotopyFiber_loop_naturality.
For an arbitrary index I with decidable equality and Nonempty I,
HomotopyGroup.homotopyFiberConnectingHom I f b e₀ h is the connecting
homomorphism from HomotopyGroup (I ⊕ Unit) B b to
HomotopyGroup I HF (HomotopyFiber.const e₀ h).
The underlying ContinuousMap.HomotopyFiber.loopInclusion retains the specified
point and whole forward loop; homotopyFiberConnectingHom_class_point_path
describes every point and time value of the connecting representative.
homotopyFiberConnectingHom_naturality gives equality of homomorphisms for
strict based squares, and range_map_eq_ker_homotopyFiberConnectingHom
identifies its kernel with the range of based postcomposition by f.
For I = Fin n with n ≥ 1, homotopyFiberConnectingHom_fin_class identifies
this homomorphism with the finite connecting representative after canonical
last-coordinate reindexing; no group structure on path components is used.
Function.range_eq_preimage_singleton_of_coordinates transports such
range–point-fiber equalities along commuting coordinates, requiring only
surjectivity in the first column and injectivity in the other two.
The ordinary compact-open model and finite-degree exactness adapt May,
Chapter 8 §§5–6, printed pp. 61–62; strict-square and all-index naturality
are structural extensions, not statements quoted from May. This is not a
signed long exact sequence of groups or a comparison with his category U:
π₀ remains a pointed set, and π₁ need not be abelian.
Finite generalized loops as based compact-open maps (GenLoop.OnePoint).
For every finite index type N ([Finite N]) and every topological space X
with chosen x, GenLoop.onePointHomeomorph N x identifies GenLoop N X x
with continuous maps from OnePoint ((Cube.boundary N)ᶜ) taking infinity to
x, with the ordinary compact-open/subtype topologies. It keeps the loop's
values on the coordinate-face boundary complement and assigns x at infinity;
its inverse precomposes with the boundary collapse. Underlying-map and
evaluation laws characterize both directions of this and the open-subspace
comparison. Index and target universes are independent; no Fintype, decidable
equality, index nonemptiness, target separation or target local compactness is
required. For empty N, the cube is a singleton with empty boundary, but the
added infinity is distinct from its cube point, so the based-map space need
not be a singleton.
Coverings on compact-open generalized-loop spaces (GenLoop).
For a covering p : E → X, a chosen e : E and any index type N with at least
two elements, hp.genLoopHomeomorph N e identifies GenLoop N E e with
GenLoop N X (p e) in their ordinary compact-open/subtype topologies. Its forward
map is GenLoop.map and its inverse is the unique chosen based lift hp.liftGenLoop e.
The lift is natural in commuting squares with arbitrary continuous horizontal maps;
the forward map agrees with HomotopyGroup.mapFun on representative classes.
Cube, total and base universes are independent, without finiteness, decidable equality,
connectedness, local path connectedness, local compactness, separation or global
surjectivity assumptions.
Coverings on positive homotopy groups (Covering.HomotopyGroup).
A covering induces an injection on the cubical homotopy quotient for every nonempty
index type, and a bijection when the index has at least two elements. Neither needs
decidable equality. With supplied decidable equality, the latter is a multiplicative
equivalence for the stock group structures: its forward map is HomotopyGroup.map,
and its inverse sends a class to the class of its chosen based lift. The cube, total
and base universes are independent, without connectedness, local path connectedness,
separation, finiteness or global surjectivity assumptions. For Fin n this gives
the covering isomorphism in degrees n ≥ 2; arbitrary indices use the coordinate-face
boundary, without a sphere-domain comparison.
Sheaves of representation sections (SectionsPresheaf).
For any topological space X, a representation FundamentalGroupoid X ⥤ Type w
determines a presheaf of transport-invariant families, functorially in the representation.
At an open U, its values are canonically equivalent to sections of the representation
pulled back along FundamentalGroupoid U → FundamentalGroupoid X; the comparison
preserves open restriction and natural transformations. Only paths in the open subspace
enter the transport condition. Space and fiber universes are independent, with no
smallness, connectedness, local connectedness or inhabited-fiber assumption.
This presheaf is a sheaf: compatible families on every open cover glue uniquely.
No semilocal simple connectivity is needed, and no covering realization is asserted.
The limits API
sends pointwise limit cones to limit cones. For coefficients in Type v,
[LocallySmall.{v} (FundamentalGroupoid X)] suffices for the sections-presheaf
functor to preserve every existing limit, with arbitrary indexing universes and
no shape-completeness assumption on Type v. This asserts sufficiency only,
not necessity or completeness. More generally, for any C : Type u
with Category.{a} C, the sections functor (C ⥤ Type v) ⥤ Type (max u v) is
corepresented by a constant singleton representation and preserves every existing
limit, without smallness or coefficient-completeness assumptions. The category,
coefficient and indexing universes remain independent.
Arbitrary coproducts and products (Coproduct,
Product).
The inclusion-induced comparison Σ i, FundamentalGroupoid (X i) →
FundamentalGroupoid (Σ i, X i) is an equivalence; the dependent-product
comparison is an isomorphism in Grpd, with coordinate projection and assembly.
Index and space universes are independent; no finiteness, connectedness, local
path connectedness or nonemptiness is needed. The product comparison agrees
with Mathlib's when its universes coincide.
Reindexing cube coordinates (HomotopyGroup.Congr).
An equivalence e : N ≃ M induces HomotopyGroup.congr x e on the existing
boundary-relative quotients, sending [p] to [t ↦ p (t ∘ e)].
The inverse uses e.symm; representative, constant, identity, composition
and based-postcomposition laws are public. Index and space universes are
independent, and the indices may be empty or infinite. For nonempty indices
with supplied decidable equality, HomotopyGroup.congrMulEquiv x e uses the
same function with Mathlib's existing group structures. It commutes with
concatenation along corresponding coordinates, without requiring the two
group structures to select corresponding axes. This is a cubical transport,
not a comparison with sphere-domain homotopy classes.
Coherent loop iteration (HomotopyGroup.Iteration).
The computed comparison HomotopyGroup.genLoopEquiv N M x flattens an
N-cube of M-loops to an (N ⊕ M)-loop using Mathlib's sum-flattening
homeomorphism on representatives. Its inverse, constant and based-map laws
are public. For nonempty N, with supplied decidable equality on N and
N ⊕ M, genLoopMulEquiv preserves the existing group operations; M may
be empty. Associativity uses the ordered sum associator, and the two empty
units retain all inner-loop components or evaluate the empty inner loop.
genLoopFinEquiv n m x orders the outer coordinates before the inner ones,
with associativity and zero-unit casts in every degree and a multiplicative
refinement when n is positive. Index and space universes are independent.
These are comparisons of the existing cubical homotopy quotients, not
sphere-domain or kified mapping-space identifications.
Generalized loops and homotopy quotients of dependent products (HomotopyGroup.Product,
FundamentalGroup.Product).
For arbitrary spaces X i, points p i and cube index N,
GenLoop.piHomeomorph N p is a homeomorphism from generalized loops in the
ordinary dependent product to the Pi product of coordinate generalized-loop
spaces, using their inherited compact-open topologies. Its inverse is the
existing assembler GenLoop.pi.
HomotopyGroup.piEquiv N p identifies HomotopyGroup N (∀ i, X i) p with
∀ i, HomotopyGroup N (X i) (p i). Its coordinates are induced by evaluation;
its inverse assembles loop representatives with GenLoop.pi, naturally in
based coordinate maps. Cube, family and space universes are independent;
either index may be empty or infinite, without finiteness or decidable-equality
assumptions. No connectedness, separation or local-compactness hypotheses on
the spaces are needed; the cube's local compactness is internal to the construction.
With [DecidableEq N] [Nonempty N],
HomotopyGroup.piMulEquiv N p is multiplicative for Mathlib's existing group
structures. Under pi1MulEquivFundamentalGroup, the degree-one equivalence
agrees with the existing FundamentalGroup.piMulEquiv p, identifying
π₁(∀ i, X i, p) multiplicatively with ∀ i, π₁(X i, p i).
That FundamentalGroup API is natural in continuous coordinate maps and arbitrary
reindexing. This generalizes May's binary finite-degree product statement
(Chapter 9 §4, printed p. 67), without a sphere-domain or U-topology comparison.
Categorical based products (Products,
Based.Products).
The fundamental-group functor preserves every existing indexed product,
including the empty product, with independent index and space universes.
This is preservation, not a blanket large-product existence assertion.
The stock comparison acts by the based projections; after the canonical based
product identification, its coordinate homomorphism is exactly piMulEquiv.
No connectedness, finiteness or index-smallness premise is needed.
Circle integer coordinates (Circle).
For every nonzero real period T, π₁(AddCircle T, 0) ≃* Multiplicative ℤ,
with the loop lifted from 0 to T * n assigned n, including negative periods.
The induced period-one homeomorphism gives π₁(Circle, 1) ≃* Multiplicative ℤ,
sending the counterclockwise full turn to +1. Signed-loop, inverse, endpoint,
nonidentity and homeomorphism-compatibility laws are public; zero-period loops
are constant. The coordinate core uses Mathlib alone.
Higher circle homotopy quotients (HomotopyGroup.Circle).
At every basepoint z and for every index type N with at least two elements,
HomotopyGroup N Circle z is a subsingleton, using the coordinate-face boundary
even for infinite N. For finite indices this gives πₙ(Circle, z) = 0 for
n ≥ 2; no decidable equality or group instance is required for the quotient result.
Fundamental groups and based homotopy (Based,
Functor).
Based spaces form the under category of the one-point space. The fundamental
group at the selected point and the induced homomorphism define a functor to
GrpCat. It factors uniquely through the category of based-homotopy classes,
with object, representative-map and loop-class characteristics. The quotient
identifies exactly the based-homotopic maps and has Mathlib's categorical
universal property and natural-transformation descent. Spaces and selected
points are arbitrary, without connectedness, separation or well-pointedness.
Based maps on homotopy groups (HomotopyGroup.Map).
A continuous map preserving supplied points acts on generalized loops and on
their homotopy quotient for every cube-index type, including an empty one.
For nonempty indices with decidable equality, the same function is a group
homomorphism. Representative, constant, identity, composition and based-homotopy
laws are public; in dimension one the map agrees with FundamentalGroup.mapOfEq
under Mathlib's multiplicative comparison. Cube and space universes are
independent, with no separation, connectedness or finiteness assumptions.
The module uses Mathlib alone.
Based-homotopy classes under refinement (Based.CompactlyGenerated).
For an original UCompactlyGeneratedSpace.{p} source Z and arbitrary target
Y, BasedTopCat.compactlyGeneratedCounitEquiv identifies the whole based
hom-sets [Z, κ_p Y]_* and [Z, Y]_*. Its forward map is postcomposition by
the continuous identity, and its inverse sends every original continuous based
representative to its unchanged-function lift into κ_p Y. Joint homotopy
relative to the source point is preserved and reflected. The forward comparison
is natural under arbitrary based source and target maps without generatedness;
inverse naturality requires generatedness only of the original source spaces.
The fixed probe universe and both original carrier universes are independent.
Refinement of the original target precedes ordinary ULift to a common carrier
universe; no commutation of refinement with ULift is assumed. There are no
separation, closed-basepoint or local-compactness hypotheses.
Locally compact products (CompactlyGeneratedSpace).
The ordinary product of two UCompactlyGeneratedSpace.{u} spaces is again
u-compactly generated when the first factor is locally compact. For such
a first factor P and an arbitrary topological A,
Homeomorph.compactlyGeneratedProd identifies k_u (P × A) with P × k_u A
by the identity function in both directions, compatibly with the counits.
The probe and both space universes are independent, without separation or
smallness assumptions. This is not an arbitrary-product formula.
Closed subspaces under refinement (CompactlyGeneratedSpace).
Let κ_u Y mean Y with Mathlib's compactlyGenerated.{u} Y topology,
with continuous identity ε_u : κ_u Y → Y. Closed subsets of a
UCompactlyGeneratedSpace.{u} space are u-compactly generated in their original
subtype topology. For any ambient space and closed s,
Homeomorph.compactlyGeneratedSubtype identifies κ_u s with the subtype s
of κ_u Y by unchanged functions in both directions. This homeomorphism and
preservation of closed embeddings require no ambient compact generation or
separation. The forward comparison and restricted counit exist for every subset;
no such inheritance or homeomorphism is asserted for arbitrary subspaces,
nor preservation of arbitrary embeddings.
Fixed-evaluation fibers under refinement (Homotopy.CompactlyGenerated).
For arbitrary spaces A, X and points a : A, x : X, assume only
IsClosed ({x} : Set X). Give M = C(A, X) its original compact-open topology,
P = {F : M // F a = x} its original subtype topology, and
Q = {F : κ_u M // (ε_u F) a = x} the subtype topology inside κ_u M.
Homeomorph.compactlyGeneratedEvalFiber gives κ_u P ≃ₜ Q, with unchanged
evaluations in both directions and counit laws. It is separately natural under
f : C(A', A) with f a' = a and g : C(X, Y) with g x = y.
The second homeomorphism for postcomposition needs {y} closed; these maps do not.
Probe and all space universes are independent. No compact generation, local
compactness, separation, countability or smallness of the spaces is required.
This refines the function space, not the codomain as in C(A, κ_u X);
it asserts no P ≃ₜ Q, exponential law, joint composition continuity or
arbitrary-product closure.
Path components under refinement (Homotopy.CompactlyGenerated).
ZerothHomotopy.bijective_map_compactlyGeneratedCounit gives a bijection on
path components for every topological space. Its subtype and fixed-evaluation-fiber
versions hold for every subset and every pole, even a nonclosed one, without
compact-generation or separation assumptions. Interval paths lift with unchanged
functions; this does not assert homeomorphisms or compact generation of arbitrary
subspaces.
Relative homotopies under refinement (Homotopy.CompactlyGenerated).
From any UCompactlyGeneratedSpace.{u} source, a supplied relative homotopy
lifts to the CompHaus-test refinement of its target with its entire joint
cylinder function unchanged. Endpoints and any fixed subset are preserved;
counit postcomposition is inverse to lifting, which is natural in target maps.
Source, target and probe universes are independent. The target needs no
separation or compact-generation assumption, and the source needs no local
compactness or first-countability assumption.
CompHaus-test topology comparisons (HomotopyGroup.CompactlyGenerated).
Refining the target topology to Mathlib's compactlyGenerated.{u} X leaves
every boundary-relative cubical homotopy quotient canonically equivalent to
the original-topology quotient. The forward function is the existing
HomotopyGroup.mapFun; for nonempty indices with decidable equality the
comparison is multiplicative for the existing group structures, naturally
in based maps. Probe, cube-index and target universes are independent, with
no target separation or compact-generation hypothesis. Empty indices retain
all path components; for infinite indices both quotients are subsingletons.
This compares two topologies in the same cubical model, not sphere-domain
classes or May's weak-Hausdorff category. The
continuous-map API
lifts unchanged functions from any UCompactlyGeneratedSpace.{u} source,
with evaluation, inverse-composition and refinement-naturality laws.
Basepoint transport of generalized homotopy classes (HomotopyGroup.BasepointEquiv).
A path γ : Path x y induces HomotopyGroup.equivOfPath γ for arbitrary
index types and topological targets, with independent universes. The
characteristic theorem HomotopyGroup.pathMap_mk_eq_iff identifies transport
of representatives with a homotopy having boundary trace exactly γ.
With the supplied [DecidableEq N] [Nonempty N], mulEquivOfPath γ preserves
the existing multiplication; transport is natural and agrees with the
fundamental-group construction in degree one. Empty indices preserve the
represented component of the target; infinite-index quotients are
subsingletons. No separation or local compactness of the target is required,
and no sphere or kification model comparison is asserted.
Generalized-loop spaces and components (HomotopyGroup.LoopSpace).
For a singleton index type J, genLoopHomeoOfUnique J x is a homeomorphism
from GenLoop J X x to the compact-open based path space Path x x, with
underlying equivalence genLoopEquivOfUnique J. It evaluates a generalized
loop on constant coordinates and its inverse evaluates a path at the unique
coordinate. Constant loops correspond to reflexive paths, and the comparison
commutes with based postcomposition, including endpoint casts. Index and target
universes are independent; no separation or local compactness of X is needed.
HomotopyGroup.equivZerothHomotopy N x identifies the raw quotient
HomotopyGroup N X x with ZerothHomotopy (GenLoop N X x) by the identity
on representatives in both directions, preserving the chosen constant class.
The compact-open/subtype topology is unchanged. Index and space universes are
independent; only a topology and chosen x are required, with no finiteness,
index nonemptiness, decidable equality or separation assumptions.
Naturality relates HomotopyGroup.mapFun to ZerothHomotopy.map of the same
continuous GenLoop.map. For empty indices, the square with
genLoopHomeoOfIsEmpty and homotopyGroupEquivZerothHomotopyOfIsEmpty
commutes, including arbitrary y : X, not just x. No group structure on
components is introduced. This is a raw cubical analogue of May, Chapter 8 §1's
based mapping-space observation; his sphere classes and kified weak-Hausdorff
category U use a different model. No sphere-domain, interval-quotient,
kification, U-category or finite iterated-loop comparison is asserted.
Boundaries mean coordinate faces; for infinite indices these are not interpreted
as ambient frontiers or infinite-dimensional spheres.
Fundamental-group actions on generalized homotopy quotients (HomotopyGroup.Action).
The existing fundamental group acts on every generalized homotopy quotient by
path-induced change of basepoint. Its reversed traversal product makes this a
left action. Representatives are related exactly by homotopies whose whole
cube boundary follows the chosen loop. Based maps are equivariant for their
induced fundamental-group maps. With the given nonempty index and decidable
equality, the same action preserves the existing group multiplication. Empty
indices fix every free path component; in degree one Mathlib's comparison
gives conjugation g * a * g⁻¹. Target and index universes are independent,
and no separation or local-connectivity hypothesis is required.
Point-local loop rigidity and totally disconnected targets (HomotopyGroup.Discrete).
At any chosen point with a subsingleton path component, every generalized loop
indexed by a nonempty type equals the constant loop, so its boundary-relative
homotopy quotient is a subsingleton. In particular this holds at every basepoint
of a totally disconnected space, including discrete spaces. Cube and target
universes are independent, and indices may be infinite. The nonempty-index
hypothesis is essential in general: the empty-index quotient records all
path components.
Relative affine homotopies and vector-space quotients (Affine,
HomotopyGroup.Affine).
Continuous maps from any space into a real vector space with continuous
addition and scalar multiplication admit an affine homotopy fixed on any
subset where they agree. Every generalized loop in such a vector space is
homotopic to the constant loop relative to its cube boundary, so
HomotopyGroup N E x is a subsingleton for every index type and every chosen
point. Cube and target universes are independent; empty and infinite indices
are allowed. No separation, norm, completeness or positive-degree group
structure is required.
Positive integer index in punctured complex balls (FundamentalGroup.ComplexPuncturedBall).
For 0 < a < r, positive scaling embeds Circle as the radius-a circle
inside the punctured radius-r ball, and normalization is z / ‖z‖.
The radial deformation fixes this circle pointwise. At the image of
1 : Circle, normalization induces a multiplicative equivalence of the
fundamental group with Multiplicative ℤ; its inverse scales circle classes.
Every scaled Circle.loop n has index n, so the positive loop is nontrivial
and has index one, including on the half-radius circle in the unit ball.
Radial deformation of punctured closed balls (Homotopy.Radial).
For every real normed space and positive radius, radial projection retracts
the closed ball with its centre removed onto its metric sphere. The scalar
interpolation from the identity to inclusion after projection is a
ContinuousMap.HomotopyRel fixing every boundary point. The projection and
inclusion give a ContinuousMap.HomotopyEquiv, with evaluation, endpoint,
boundary-fixing and retraction laws. No nontriviality, completeness or dimension
assumption is required; empty punctured balls and spheres are allowed.
For an open ball of radius r and 0 < a < r, the same construction
retracts onto the radius-a inner sphere, with the deformation fixing the
range of its inclusion. Projection onto a positive-radius sphere requires
only 0 < a, even when that sphere is not contained in the source ball.
Homotopy-retraction splittings (retractionOfHomotopy).
For g : C(X, Y), f : C(Y, X) and a homotopy from f.comp g to id X,
transport along its track at x gives an explicit left inverse of
π₁(X, x) → π₁(Y, g x), which is therefore injective. A nontrivial source
vertex group and a subsingleton target vertex group obstruct such a homotopy.
Space universes are independent; no connectedness or fixed-basepoint condition is needed.
Small-path generation (OpenCover).
For an indexed open cover, a composition-stable morphism property holding on
every local inclusion image holds globally. No separate identity/inverse
stability or connectedness is needed. Naturality on local images determines
a unique natural transformation between global functors into any category.
Strict open-cover descent (OpenCoverDescent).
For any indexed open cover, local functors into any category agreeing by
equality on every ordered pairwise intersection extend uniquely by equality.
No connectivity is assumed. Inclusion cocones are colimits in Grpd and Cat.
Full-inclusion open-cover colimits (OpenCoverInclusions).
For an indexed open cover with InfClosed (Set.range U), the diagram retaining
every index and every open inclusion has the ambient fundamental groupoid as
its colimit in both Grpd and Cat. Chart functors into any category agreeing
by equality along all inclusions extend uniquely by equality, with independent
space, index, target-object and target-morphism universes. No path connectedness,
common point, finiteness, injective indexing or member equal to the whole space
is required. This generalizes May's groupoid theorem on printed p. 17 by dropping
its path-connected-member hypothesis; the based theorem on p. 18 remains separate.
Indexed based van Kampen (isColimitOfIsOpenCover).
For an arbitrarily indexed open cover by path-connected neighborhoods of a
common basepoint with InfClosed (Set.range U), compatible homomorphisms to
any group extend uniquely from the local fundamental groups. Compatibility is
along every inclusion, including repeated opens. Space, index and target-group
universes are independent; the inclusion cocone is a colimit in GrpCat.{u}.
Binary intersection closure does not require the whole space in the range.
Common-overlap stars (CommonOverlap).
Let a based open core C lie in every chart U i, with C and the charts
path connected, U i ∩ U j = C for distinct indices, and the core together
with the charts covering the space. The core-to-chart inclusion star has the
ambient fundamental group as its colimit. Its raw group colimit is canonically
multiplicatively equivalent to that group, preserving every core and chart
leg in both directions. Space and index universes are independent; empty
chart families and a nontrivial core fundamental group are allowed.
Directed open-cover colimits (DirectedOpenCover).
For any topological space with a supplied basepoint and an arbitrarily indexed,
inclusion-directed open cover by its neighborhoods, compatible homomorphisms
from the local fundamental groups to any monoid extend uniquely to a
homomorphism from the ambient group. Compatibility is along every inclusion
between presented neighborhoods; the diagram uses inducedFunctor U.
The existing inclusion cocone is a colimit in GrpCat.{u}. All indices are
retained, including repeated opens, and all maps are inclusion-induced.
Space, index and target-monoid universes are independent; no path connectedness,
intersection closure, separation, local connectivity, finiteness, dimension or
separate index nonemptiness assumption is imposed.
Directed-preorder neighborhood-cover colimits (DirectedOpenCover).
Let X : Type u be any topological space, p : X, and J : Type v have
[Preorder J] [IsDirectedOrder J]. For a monotone open-neighborhood cover
U : J → OpenNhds p,
FundamentalGroup.existsUnique_hom_of_isOpenCover_of_monotone extends local
homomorphisms to any monoid G : Type w uniquely along the canonical inclusion
legs. Compatibility is required only for i ≤ j, not for every inclusion
U i ≤ U j. For hU : Monotone U, the noncomputable definition
FundamentalGroup.isColimitOfIsOpenCoverOfMonotone supplies
IsColimit ((openNhdsCocone p).whisker hU.functor) in GrpCat.{u}.
Its diagram uses the ordinary preorder category on J. The universes u, v
and w are independent; no path connectedness, intersection closure, separation,
local connectivity, smallness, injectivity, order reflection or separate
nonemptiness assumption on J is required.
Open-cover quotient presentations (OpenCoverPresentation).
An intersection-closed open cover by path-connected neighborhoods of a common
point presents the ambient fundamental group as the free product of the local
groups modulo the normal closure of all inclusion-arrow relators. The quotient
equivalence preserves the inclusion legs in both directions; the canonical
free-product map is surjective with exactly this kernel. Arbitrary indices,
repeated presentations and independent index/space universes are allowed.
Two-open based van Kampen (OpenCover).
For opens U, V with U ∪ V = X, all of U, V, U ∩ V path connected and a point
in the intersection, compatible homomorphisms to any group extend uniquely,
satisfying both restriction equations; target and space universes are independent.
The inclusion square is a pushout in GrpCat.{u}. These specialize indexed
van Kampen; neither formulation adds ambient or local path connectedness.
Infinite cyclic intersections (OpenCoverCyclicIntersection).
For a path-connected two-open cover with path-connected intersection, suppose
the second open has trivial fundamental group and the intersection group is
classified by Multiplicative ℤ. A homomorphism on the first open extends
uniquely exactly when it kills the inclusion image of the class corresponding
to Multiplicative.ofAdd (1 : ℤ). Restriction gives an equivalence with these
homomorphisms, with forward and inverse restriction laws. Restriction to the
first open also determines ambient homomorphisms without any cyclicity
assumption. Space and target-group universes are independent; no geometric
orientation is implicit in the supplied classification.
Path-component inclusion (pathComponentInclusionMulEquiv).
Inclusion of a path component induces an isomorphism on fundamental groups at
any point of the component. The inverse is represented by corestricting loops;
neither openness of the component nor connectedness of the ambient space is required.
Simple-connectivity criteria (FundamentalGroup,
OpenCover).
Simple connectivity is characterized by path connectedness and a
subsingleton fundamental group at a given point. Two simply connected opens
covering a space make it simply connected when their intersection
is path connected, including nonemptiness. A nonempty directed union of open simply
connected sets is simply connected. An arbitrarily indexed open cover also gives
simple connectivity when its members are simply connected, share one point, and
have path-connected pairwise intersections; connected triple intersections are not
required. These criteria add no ambient or local path connectedness or separation
assumption; overlaps need not be simply connected.
Semilocal simple connectivity (Basic,
Maps,
LocallyPathConnected).
At x, an open neighborhood's loops based at x contract in the ambient
space, not necessarily inside the neighborhood. The global class quantifies
separately over all centers and is vacuous on empty spaces. Simply connected
spaces satisfy it. Continuous maps with injective induced based fundamental-group
maps reflect it; local homeomorphisms preserve it pointwise. For every covering,
the pointwise properties are equivalent and the base property implies the total
property without surjectivity; global descent needs surjectivity, also for local
homeomorphisms. Only with local path connectedness do we obtain one open
path-connected neighborhood controlling loops at all its basepoints in the ambient
space, not an intrinsically simply connected neighborhood. Space universes are
independent; no separation or extra connectedness/nonemptiness is assumed.
Cancellation of covering maps (Composition).
If q ∘ g and q are covering maps, g is continuous, and the target of g is
locally connected, then g is a covering map. The three space universes are independent;
no surjectivity, nonempty-fiber, path-connectedness or separation assumption is needed.
Based lifting and equivalence of covers (Lifting,
Equivalence).
A continuous map from a path-connected, locally path-connected domain with
a prescribed lift of its basepoint has a unique based lift iff its induced
fundamental-group image lies in the covering image, compared by basepoint equality.
Two covers with path-connected totals and equal based images at specified points
over the same point are homeomorphic over the base, taking one point to the other;
only the source total must be locally path connected. No base connectedness or
global surjectivity is required.
Monodromy, cosets and path components (Monodromy,
Components).
Fiber-point stabilizers are the based fundamental-group images, and orbits are
joinedness classes, without connectivity or local path connectedness. Orbit
classes identify with the fiber of the induced path-component map. Over a
path-connected base they identify with all total-space components, allowing
empty total spaces and independent total/base universes; total path connectedness
is equivalent to nonemptiness and pretransitive monodromy. With path-connected total
and a chosen fiber point, the fiber is equivariantly equivalent to left cosets of the
induced based fundamental-group image, by [g] ↦ monodromy g; normality is not needed.
Commuting squares of continuous maps intertwine whole canonical path lifts and
monodromy across different bases; neither horizontal map need be a covering. Equivariant squares of quotient covers
intertwine the canonical homomorphisms to opposite acting groups, without simple
connectivity. All space and acting-group universes are independent.
Pullbacks and double cosets (Pullback,
PullbackDoubleCoset).
For a covering p : T → B and any continuous a : X → B, the second projection
p.Pullback a → X is a covering. Its fiber over x is homeomorphic to p ⁻¹' {b}
for every equality a x = b. The fiber homeomorphism itself works for arbitrary maps,
with topologies only on T and X, not on B. Both projections of a lifted path are
computed as whole continuous maps, and the fiber comparison intertwines all path-class
monodromy and the canonical left fundamental-group actions. The three space universes
are independent.
The pullback of two covers is a cover whose fiber is the product with diagonal
monodromy. Over a path-connected base, diagonal orbits give its components,
allowing empty/disconnected totals and independent universes. Alternatively,
with both totals path connected and specified fiber points, components are
H \ G / K for the based fundamental-group images; no base path connectedness is needed.
Fiber cardinalities and finiteness (Cardinality).
Point-fiber cardinality and the predicate of fiber finiteness are locally
constant, with independent universes. The finite-fiber locus is clopen:
empty fibers are included, infinite fibers excluded. No connectedness, local
path connectedness, finiteness, surjectivity or nonempty total is needed.
Proper covering maps (Proper).
For a covering map between arbitrary topological spaces, Mathlib's
IsProperMap holds iff every point fiber is finite. Total and base universes
are independent; no separation, local compactness, connectedness, surjectivity
or uniform degree is required. Over a preconnected base, finiteness of the
fiber at any given point suffices, without an extra nonemptiness premise.
For preconnected total and a supplied e0, properness instead means finiteness over
p e0. With path-connected total, it means finite index of the canonical based
fundamental-group image (FiniteIndex);
neither base connectedness nor surjectivity is required. Compact subsets have compact inverse images.
Maps of covers and deck centralizers (DeckMonodromy).
Over-maps restrict to equivariant maps on a chosen fiber without connectivity
assumptions. This is an equivalence of map spaces for path-connected base and
locally path-connected source, allowing empty/disconnected source and arbitrary target cover.
Alternatively a supplied source point and path-connected, locally path-connected
source suffice without base connectedness. Deck restriction is a homomorphism
into the monodromy centralizer in the fiber permutation group; it is injective
for path-connected base and a multiplicative equivalence if the total is also
locally path connected, even empty/disconnected. The supplied-point alternative
needs only path-connected, locally path-connected total, not base connectedness.
Normalizer quotients and regularity (NormalizerQuotient).
For a covering map with path-connected, locally path-connected total space
and a chosen point, the normalizer quotient of the based fundamental-group
image is canonically the deck group. A representative acts by monodromy of its inverse at the
chosen point. The existing deck action on that fiber is pretransitive iff
the image subgroup is normal, without base connectedness or surjectivity.
Deck fixed-point rigidity (DeckGroup).
Deck groups act on point fibers. For a separated, locally injective map with
preconnected total, evaluation at a supplied point is injective: fixing a point
forces identity. No codomain topology is needed; surjectivity is not asserted.
Generalized loops and homotopy fibers
For any cube index and based continuous map, generalized loops commute with its ordinary homotopy fiber. The comparison preserves the retained point functions, complete paths and both specified constant points, and is natural for based commuting squares.
See ContinuousMap.HomotopyFiber.genLoopHomeomorph and
ContinuousMap.HomotopyFiber.genLoopHomeomorph_naturality in
Topology/Homotopy/Fiber/GenLoop.lean.
Dependent products of homotopy fibers
For an arbitrary index type and topological families E k and B k, the
product-fiber module
constructs ContinuousMap.HomotopyFiber.piHomeomorph f b:
HomotopyFiber (ContinuousMap.piMap f) b ≃ₜ (∀ k, HomotopyFiber (f k) (b k)).
The comparison retains every original source point and the entire compact-open
path at the same time. Its inverse transposes the whole family of paths; only
the interval needs local compactness. The index, source and target universes are
independent, with no finiteness, nonemptiness or separation assumptions.
The original constant const e₀ (funext h) corresponds in both directions to
fun k => const (e₀ k) (h k).
piHomeomorph_naturality expresses naturality as equality of whole bundled
continuous maps for arbitrary families of commuting squares. For Fin 2,
piHomeomorph_finTwo identifies the composite homeomorphisms through
Homeomorph.piFinTwo, the homotopy-fiber homeomorph, and prodHomeomorph.
This common-universe family diagram leaves the binary comparison's four
independent ambient universes and its eight-universe naturality law unchanged.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.