ProCGroups.InverseSystems.Basic
This module studies basic for pro cgroups. An inverse system of topological spaces indexed by a preorder. The transition map along \(i \le i\) is the identity on points.
import
- Mathlib.Topology.Algebra.Ring.Basic
- Mathlib.Algebra.Module.Pi
structure InverseSystem where
X : I → Type v
topologicalSpace : ∀ i, TopologicalSpace (X i)
map : ∀ {i j : I}, i ≤ j → X j → X i
continuous_map : ∀ {i j : I} (hij : i ≤ j), Continuous (map hij)
map_id : ∀ i, map (le_rfl : i ≤ i) = id
map_comp : ∀ {i j k : I} (hij : i ≤ j) (hjk : j ≤ k),
map hij ∘ map hjk = map (hij.trans hjk)An inverse system of topological spaces indexed by a preorder.
@[simp] theorem map_id_apply (i : I) (x : S.X i) :
S.map (le_rfl : i ≤ i) x = xThe transition map along \(i \le i\) is the identity on points.
Show proof
by
simpa using congrFun (S.map_id i) xProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□@[simp] theorem map_comp_apply {i j k : I} (hij : i ≤ j) (hjk : j ≤ k) (x : S.X k) :
S.map hij (S.map hjk x) = S.map (hij.trans hjk) xThe composite map is computed pointwise by applying the constituent coordinate formulas in succession.
Show proof
by
simpa [Function.comp] using congrFun (S.map_comp hij hjk) xProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□def Compatible (x : ∀ i, S.X i) : Prop :=
∀ i j, ∀ hij : i ≤ j, S.map hij (x j) = x iCompatibility of a family of points in the product.
def CompatibleMaps {Y : Type w} (ψ : ∀ i, Y → S.X i) : Prop :=
∀ i j, ∀ hij : i ≤ j, S.map hij ∘ ψ j = ψ iCompatibility of a family of maps into an inverse system.
abbrev inverseLimit : Type _ := {x : ∀ i, S.X i // S.Compatible x}The inverse limit realized as a subtype of the product.
def projection (i : I) : S.inverseLimit → S.X i := fun x => x.1 iThe canonical projection from the inverse limit to the \(i\)-th component.
def IsLinearSystem {R : Type w} [Semiring R] (S : InverseSystem (I := I))
[∀ i, AddCommMonoid (S.X i)] [∀ i, Module R (S.X i)]
[AddCommMonoid S.inverseLimit] [Module R S.inverseLimit] : Prop :=
(∀ {i j : I} (hij : i ≤ j) (r : R) (x : S.X j),
S.map hij (r • x) = r • S.map hij x) ∧
(∀ i (r : R) (x : S.inverseLimit), S.projection i (r • x) = r • S.projection i x)Linearity data for an inverse system and its concrete inverse-limit cone. This companion predicate packages the scalar-compatibility facts used by Hom-comparison formulations, without installing them as global typeclass instances.
theorem map_smul {R : Type w} [Semiring R] {S : InverseSystem (I := I)}
[∀ i, AddCommMonoid (S.X i)] [∀ i, Module R (S.X i)]
[AddCommMonoid S.inverseLimit] [Module R S.inverseLimit]
(hS : IsLinearSystem (R := R) S) {i j : I} (hij : i ≤ j) (r : R) (x : S.X j) :
S.map hij (r • x) = r • S.map hij xMaps in a linear inverse system commute with scalar multiplication.
Show proof
hS.1 hij r xProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem projection_smul {R : Type w} [Semiring R] {S : InverseSystem (I := I)}
[∀ i, AddCommMonoid (S.X i)] [∀ i, Module R (S.X i)]
[AddCommMonoid S.inverseLimit] [Module R S.inverseLimit]
(hS : IsLinearSystem (R := R) S) (i : I) (r : R) (x : S.inverseLimit) :
S.projection i (r • x) = r • S.projection i xThe finite-stage projection commutes with scalar multiplication by coefficients.
Show proof
hS.2 i r xProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□@[simp] theorem projection_apply (i : I) (x : S.inverseLimit) :
S.projection i x = x.1 iApplying a projection to an inverse-limit element returns its corresponding stage coordinate.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem projection_compatible (x : S.inverseLimit) (i j : I) (hij : i ≤ j) :
S.map hij (S.projection j x) = S.projection i xProjections from the inverse limit are compatible with the transition maps.
Show proof
by
exact x.2 i j hijProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem projection_compatibleMaps : S.CompatibleMaps S.projectionThe canonical projections form a compatible family of maps.
Show proof
by
intro i j hij
funext x
exact S.projection_compatible x i j hijProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem continuous_projection (i : I) : Continuous (S.projection i)Each canonical projection from an inverse limit is continuous.
Show proof
(continuous_apply i).comp continuous_subtype_valProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□@[ext] theorem ext {x y : S.inverseLimit}
(h : ∀ i, S.projection i x = S.projection i y) : x = yTwo inverse-limit points are equal when all their projections are equal.
Show proof
by
apply Subtype.ext
funext i
exact h iProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□def inverseLimitLift {Y : Type w} (ψ : ∀ i, Y → S.X i)
(hcompat : S.CompatibleMaps ψ) :
Y → S.inverseLimit := fun y =>
⟨fun i => ψ i y, by
intro i j hij
exact congrFun (hcompat i j hij) y⟩The concrete map induced by a compatible family of maps into the subtype inverse limit.
@[simp] theorem projection_comp_inverseLimitLift {Y : Type w} (ψ : ∀ i, Y → S.X i)
(hcompat : S.CompatibleMaps ψ) (i : I) :
S.projection i ∘ S.inverseLimitLift ψ hcompat = ψ iComposing a canonical projection with the lift recovers the corresponding compatible map.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□@[simp] theorem projection_inverseLimitLift_apply {Y : Type w} (ψ : ∀ i, Y → S.X i)
(hcompat : S.CompatibleMaps ψ) (i : I) (y : Y) :
S.projection i (S.inverseLimitLift ψ hcompat y) = ψ i yApplying a projection to an inverse-limit lift returns the corresponding stage map value.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem inverseLimitLift_unique {Y : Type w} (ψ : ∀ i, Y → S.X i)
(hcompat : S.CompatibleMaps ψ) {f : Y → S.inverseLimit}
(hf : ∀ i, S.projection i ∘ f = ψ i) :
f = S.inverseLimitLift ψ hcompatA map into the subtype inverse limit is uniquely determined by its projections.
Show proof
by
funext y
apply S.ext
intro i
simpa [Function.comp] using congrFun (hf i) yProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem continuous_inverseLimitLift {Y : Type w} [TopologicalSpace Y] (ψ : ∀ i, Y → S.X i)
(hψ : ∀ i, Continuous (ψ i))
(hcompat : S.CompatibleMaps ψ) :
Continuous (S.inverseLimitLift ψ hcompat)A lift from a topological space is continuous when all of its component maps are continuous.
Show proof
by
exact Continuous.subtype_mk (continuous_pi fun i => hψ i) fun y => by
intro i j hij
exact congrFun (hcompat i j hij) yProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□structure IsInverseLimit {L : Type w} [TopologicalSpace L] (π : ∀ i, L → S.X i) : Prop where
continuous_proj : ∀ i, Continuous (π i)
compatible : S.CompatibleMaps π
existsUnique_lift :
∀ {Y : Type w} [TopologicalSpace Y] (ψ : ∀ i, Y → S.X i)
(_hψ : ∀ i, Continuous (ψ i)) (_hcompat : S.CompatibleMaps ψ),
∃! f : Y → L, Continuous f ∧ ∀ i, π i ∘ f = ψ iThe universal property of an inverse limit.
noncomputable def lift (hπ : S.IsInverseLimit π) {Y : Type w} [TopologicalSpace Y]
(ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ) :
Y → L :=
Classical.choose (ExistsUnique.exists (hπ.existsUnique_lift ψ hψ hcompat))A compatible family of maps to the stages lifts uniquely to a map into the inverse limit.
theorem lift_spec (hπ : S.IsInverseLimit π) {Y : Type w} [TopologicalSpace Y]
(ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ) :
Continuous (hπ.lift ψ hψ hcompat) ∧
∀ i, π i ∘ hπ.lift ψ hψ hcompat = ψ iThe universal-property lift is continuous and has the prescribed projections.
Show proof
Classical.choose_spec (ExistsUnique.exists (hπ.existsUnique_lift ψ hψ hcompat))Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem continuous_lift (hπ : S.IsInverseLimit π) {Y : Type w} [TopologicalSpace Y]
(ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ) :
Continuous (hπ.lift ψ hψ hcompat)The lift into the inverse limit is continuous when all coordinate maps are continuous.
Show proof
(hπ.lift_spec ψ hψ hcompat).1Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem fac (hπ : S.IsInverseLimit π) {Y : Type w} [TopologicalSpace Y]
(ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ)
(i : I) :
π i ∘ hπ.lift ψ hψ hcompat = ψ iThe universal-property lift has the prescribed i-th projection.
Show proof
(hπ.lift_spec ψ hψ hcompat).2 iProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem uniq (hπ : S.IsInverseLimit π) {Y : Type w} [TopologicalSpace Y]
(ψ : ∀ i, Y → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ)
{f : Y → L} (hf : Continuous f) (hfac : ∀ i, π i ∘ f = ψ i) :
f = hπ.lift ψ hψ hcompatThe universal-property lift is the unique continuous map with the prescribed projections.
Show proof
by
rcases hπ.existsUnique_lift ψ hψ hcompat with ⟨g, hg, huniq⟩
have hchosen : hπ.lift ψ hψ hcompat = g := huniq _ (hπ.lift_spec ψ hψ hcompat)
exact (huniq _ ⟨hf, hfac⟩).trans hchosen.symmProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem lift_self (hπ : S.IsInverseLimit π) :
hπ.lift (Y := L) π hπ.continuous_proj hπ.compatible = idLifting the projection family of an inverse limit gives the identity map.
Show proof
by
symm
exact hπ.uniq (Y := L) π hπ.continuous_proj hπ.compatible continuous_id fun _ => rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□noncomputable def homeomorph {L' : Type w} [TopologicalSpace L'] {π' : ∀ i, L' → S.X i}
(hπ : S.IsInverseLimit π) (hπ' : S.IsInverseLimit π') :
L ≃ₜ L' where
toFun := hπ'.lift (Y := L) π hπ.continuous_proj hπ.compatible
invFun := hπ.lift (Y := L') π' hπ'.continuous_proj hπ'.compatible
left_inv := by
intro x
let f : L → L' := hπ'.lift (Y := L) π hπ.continuous_proj hπ.compatible
let g : L' → L := hπ.lift (Y := L') π' hπ'.continuous_proj hπ'.compatible
have hgf : g ∘ f = hπ.lift (Y := L) π hπ.continuous_proj hπ.compatible := by
exact hπ.uniq (Y := L) π hπ.continuous_proj hπ.compatible
((hπ.continuous_lift (Y := L') π' hπ'.continuous_proj hπ'.compatible).comp
(hπ'.continuous_lift (Y := L) π hπ.continuous_proj hπ.compatible))
(by
intro i
calc
π i ∘ (g ∘ f) = (π i ∘ g) ∘ f := by rfl
_ = π' i ∘ f := by
rw [hπ.fac (Y := L') π' hπ'.continuous_proj hπ'.compatible i]
_ = π i := by
simpa [Function.comp] using
hπ'.fac (Y := L) π hπ.continuous_proj hπ.compatible i)
calc
g (f x) = hπ.lift (Y := L) π hπ.continuous_proj hπ.compatible x := congrFun hgf x
_ = x := by
simpa using congrFun hπ.lift_self x
right_inv := by
intro x
let f : L → L' := hπ'.lift (Y := L) π hπ.continuous_proj hπ.compatible
let g : L' → L := hπ.lift (Y := L') π' hπ'.continuous_proj hπ'.compatible
have hfg : f ∘ g = hπ'.lift (Y := L') π' hπ'.continuous_proj hπ'.compatible := by
exact hπ'.uniq (Y := L') π' hπ'.continuous_proj hπ'.compatible
((hπ'.continuous_lift (Y := L) π hπ.continuous_proj hπ.compatible).comp
(hπ.continuous_lift (Y := L') π' hπ'.continuous_proj hπ'.compatible))
(by
intro i
calc
π' i ∘ (f ∘ g) = (π' i ∘ f) ∘ g := by rfl
_ = π i ∘ g := by
rw [hπ'.fac (Y := L) π hπ.continuous_proj hπ.compatible i]
_ = π' i := by
simpa [Function.comp] using
hπ.fac (Y := L') π' hπ'.continuous_proj hπ'.compatible i)
calc
f (g x) = hπ'.lift (Y := L') π' hπ'.continuous_proj hπ'.compatible x := congrFun hfg x
_ = x := by
simpa using congrFun hπ'.lift_self x
continuous_toFun := hπ'.continuous_lift (Y := L) π hπ.continuous_proj hπ.compatible
continuous_invFun := hπ.continuous_lift (Y := L') π' hπ'.continuous_proj hπ'.compatibleInverse limits are unique up to unique homeomorphism.
theorem isInverseLimit_projection : S.IsInverseLimit S.projectionThe subtype model carries the inverse-limit universal property.
Show proof
by
refine ⟨S.continuous_projection, S.projection_compatibleMaps, ?_⟩
intro Y _ ψ hψ hcompat
refine ⟨S.inverseLimitLift ψ hcompat, ?_, ?_⟩
· exact ⟨S.continuous_inverseLimitLift ψ hψ hcompat,
fun i => S.projection_comp_inverseLimitLift ψ hcompat i⟩
· intro f hf
exact S.inverseLimitLift_unique ψ hcompat hf.2Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem isClosed_setOf_compatible [∀ i, T2Space (S.X i)] :
IsClosed {x : ∀ i, S.X i | S.Compatible x}The inverse limit is a closed subspace of the product.
Show proof
by
simp only [Compatible, setOf_forall]
refine isClosed_iInter fun i => isClosed_iInter fun j => isClosed_iInter fun hij => ?_
exact isClosed_eq ((S.continuous_map hij).comp (continuous_apply j)) (continuous_apply i)Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□instance instCompactSpaceInverseLimit [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)] :
CompactSpace S.inverseLimit := by
let hs : IsClosed {x : ∀ i, S.X i | S.Compatible x} := S.isClosed_setOf_compatible
simpa [InverseSystem.inverseLimit] using hs.isClosedEmbedding_subtypeVal.compactSpaceThe constructed object carries the compact space structure inherited from its profinite construction.
theorem t2Space_inverseLimit [∀ i, T2Space (S.X i)] :
T2Space S.inverseLimitInverse limits of Hausdorff spaces are Hausdorff.
Show proof
inferInstanceProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem totallyDisconnectedSpace_inverseLimit [∀ i, TotallyDisconnectedSpace (S.X i)] :
TotallyDisconnectedSpace S.inverseLimitInverse limits of totally disconnected spaces are totally disconnected.
Show proof
inferInstanceProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem isQuotientMap_projection_of_surjective [∀ i, CompactSpace (S.X i)]
[∀ i, T2Space (S.X i)] {i : I} (hsurj : Function.Surjective (S.projection i)) :
Topology.IsQuotientMap (S.projection i)A surjective projection from a compact inverse limit to a Hausdorff stage is a quotient map.
Show proof
IsQuotientMap.of_surjective_continuous hsurj (S.continuous_projection i)Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□class IsGroupSystem (S : InverseSystem (I := I)) [∀ i, Group (S.X i)] : Prop where
map_one : ∀ {i j : I} (hij : i ≤ j), S.map hij 1 = 1
map_mul : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
S.map hij (x * y) = S.map hij x * S.map hij y
map_inv : ∀ {i j : I} (hij : i ≤ j) (x : S.X j),
S.map hij x⁻¹ = (S.map hij x)⁻¹A group-valued inverse system whose transition maps are group homomorphisms.
instance instOneInverseLimit : One S.inverseLimit where
one := ⟨fun i => 1, by
intro i j hij
simpa using IsGroupSystem.map_one (S := S) hij⟩The unit of the inverse limit is the compatible family of units at all stages.
instance instMulInverseLimit : Mul S.inverseLimit where
mul x y := ⟨fun i => S.projection i x * S.projection i y, by
intro i j hij
calc
S.map hij (S.projection j x * S.projection j y)
= S.map hij (S.projection j x) * S.map hij (S.projection j y) := by
simpa using IsGroupSystem.map_mul (S := S) hij (S.projection j x)
(S.projection j y)
_ = S.projection i x * S.projection i y := by
rw [S.projection_compatible x i j hij, S.projection_compatible y i j hij]⟩Multiplication on the inverse limit is defined coordinatewise through the stage multiplications.
instance instInvInverseLimit : Inv S.inverseLimit where
inv x := ⟨fun i => (S.projection i x)⁻¹, by
intro i j hij
calc
S.map hij ((S.projection j x)⁻¹) = (S.map hij (S.projection j x))⁻¹ := by
simpa using IsGroupSystem.map_inv (S := S) hij (S.projection j x)
_ = (S.projection i x)⁻¹ := by rw [S.projection_compatible x i j hij]⟩The inverse-limit object carries the structure induced coordinatewise from the finite stages.
@[simp] theorem projection_one (i : I) : S.projection i (1 : S.inverseLimit) = 1The projection of the identity element is the identity at each stage.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□@[simp] theorem projection_mul (i : I) (x y : S.inverseLimit) :
S.projection i (x * y) = S.projection i x * S.projection i yProjection commutes with multiplication in a group-valued inverse system.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□@[simp] theorem projection_inv (i : I) (x : S.inverseLimit) :
S.projection i x⁻¹ = (S.projection i x)⁻¹Projection commutes with inversion in a group-valued inverse system.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□instance instGroupInverseLimit : Group S.inverseLimit where
one := 1
mul := (· * ·)
inv := Inv.inv
mul_assoc x y z := by
apply S.ext
intro i
change ((x.1 i * y.1 i) * z.1 i) = (x.1 i * (y.1 i * z.1 i))
simp only [mul_assoc]
one_mul x := by
apply S.ext
intro i
change 1 * x.1 i = x.1 i
simp only [one_mul]
mul_one x := by
apply S.ext
intro i
change x.1 i * 1 = x.1 i
simp only [mul_one]
inv_mul_cancel x := by
apply S.ext
intro i
change (x.1 i)⁻¹ * x.1 i = 1
simp only [inv_mul_cancel]The constructed carrier inherits its group structure from the coordinatewise group structure of the construction.
instance instIsTopologicalGroupInverseLimit [∀ i, IsTopologicalGroup (S.X i)] :
IsTopologicalGroup S.inverseLimit where
continuous_mul := by
exact Continuous.subtype_mk
(continuous_pi fun i =>
((S.continuous_projection i).comp continuous_fst).mul
((S.continuous_projection i).comp continuous_snd))
(fun xy => by
intro i j hij
change S.map hij (S.projection j xy.1 * S.projection j xy.2) =
S.projection i xy.1 * S.projection i xy.2
rw [IsGroupSystem.map_mul (S := S) hij,
S.projection_compatible xy.1 i j hij, S.projection_compatible xy.2 i j hij])
continuous_inv := by
exact Continuous.subtype_mk
(continuous_pi fun i => continuous_inv.comp (S.continuous_projection i))
(fun x => by
intro i j hij
change S.map hij ((S.projection j x)⁻¹) = (S.projection i x)⁻¹
rw [IsGroupSystem.map_inv (S := S) hij, S.projection_compatible x i j hij])The object is a topological group with the induced group operations and topology.
def projectionHom (i : I) : S.inverseLimit →* S.X i where
toFun := S.projection i
map_one' := projection_one (S := S) i
map_mul' := by
intro x y
exact projection_mul (S := S) i x yThe canonical projections from a group-valued inverse limit are homomorphisms.
@[simp] theorem projectionHom_apply (i : I) (x : S.inverseLimit) :
projectionHom (S := S) i x = S.projection i xApplying a homomorphic projection to an inverse-limit element returns its corresponding stage coordinate.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□class IsAddGroupSystem (S : InverseSystem (I := I)) [∀ i, AddCommGroup (S.X i)] : Prop where
map_zero : ∀ {i j : I} (hij : i ≤ j), S.map hij 0 = 0
map_add : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
S.map hij (x + y) = S.map hij x + S.map hij y
map_neg : ∀ {i j : I} (hij : i ≤ j) (x : S.X j),
S.map hij (-x) = -S.map hij xAn additive-group-valued inverse system whose transition maps are additive homomorphisms.
class IsModuleSystem (R : Type w) [Semiring R] (S : InverseSystem (I := I))
[∀ i, AddCommGroup (S.X i)] [∀ i, Module R (S.X i)] : Prop where
map_smul : ∀ {i j : I} (hij : i ≤ j) (r : R) (x : S.X j),
S.map hij (r • x) = r • S.map hij xA module-valued inverse system whose transition maps are linear over a fixed semiring.
instance instZeroAddInverseLimit : Zero S.inverseLimit where
zero := ⟨fun i => 0, by
intro i j hij
simpa using IsAddGroupSystem.map_zero (S := S) hij⟩The zero element of the inverse limit is the compatible family of zero elements at all stages.
instance instAddAddInverseLimit : Add S.inverseLimit where
add x y := ⟨fun i => S.projection i x + S.projection i y, by
intro i j hij
calc
S.map hij (S.projection j x + S.projection j y)
= S.map hij (S.projection j x) + S.map hij (S.projection j y) := by
simpa using IsAddGroupSystem.map_add (S := S) hij (S.projection j x)
(S.projection j y)
_ = S.projection i x + S.projection i y := by
rw [S.projection_compatible x i j hij, S.projection_compatible y i j hij]⟩Addition in the additive inverse limit is defined coordinatewise.
instance instNegAddInverseLimit : Neg S.inverseLimit where
neg x := ⟨fun i => -S.projection i x, by
intro i j hij
calc
S.map hij (-S.projection j x) = -S.map hij (S.projection j x) := by
simpa using IsAddGroupSystem.map_neg (S := S) hij (S.projection j x)
_ = -S.projection i x := by rw [S.projection_compatible x i j hij]⟩Negation on an additive inverse limit is defined coordinatewise through the stage negations.
instance instSubAddInverseLimit : Sub S.inverseLimit where
sub x y := ⟨fun i => S.projection i x - S.projection i y, by
intro i j hij
change S.map hij (S.projection j x - S.projection j y) =
S.projection i x - S.projection i y
rw [sub_eq_add_neg, IsAddGroupSystem.map_add, IsAddGroupSystem.map_neg,
S.projection_compatible x i j hij, S.projection_compatible y i j hij, sub_eq_add_neg]⟩Subtraction in the inverse limit is defined coordinatewise through the stage subtractions.
instance instSMulNatAddInverseLimit : SMul ℕ S.inverseLimit where
smul n x := ⟨fun i => n • S.projection i x, by
intro i j hij
change S.map hij (n • S.projection j x) = n • S.projection i x
induction n with
| zero =>
simp only [InverseSystem.projection_apply, zero_nsmul, IsAddGroupSystem.map_zero]
| succ n ihn =>
rw [succ_nsmul, succ_nsmul]
calc
S.map hij (n • S.projection j x + S.projection j x)
= S.map hij (n • S.projection j x) + S.map hij (S.projection j x) := by
exact IsAddGroupSystem.map_add (S := S) hij (n • S.projection j x)
(S.projection j x)
_ = n • S.projection i x + S.projection i x := by
rw [ihn, S.projection_compatible x i j hij]⟩An additive inverse limit carries natural-number scalar multiplication coordinatewise.
instance instSMulIntAddInverseLimit : SMul ℤ S.inverseLimit where
smul n x := ⟨fun i => n • S.projection i x, by
intro i j hij
change S.map hij (n • S.projection j x) = n • S.projection i x
let f : S.X j →+ S.X i :=
{ toFun := S.map hij
map_zero' := IsAddGroupSystem.map_zero (S := S) hij
map_add' := IsAddGroupSystem.map_add (S := S) hij }
calc
S.map hij (n • S.projection j x) = f (n • S.projection j x) := rfl
_ = n • f (S.projection j x) := f.map_zsmul (S.projection j x) n
_ = n • S.projection i x := by
change n • S.map hij (S.projection j x) = n • S.projection i x
rw [S.projection_compatible x i j hij]⟩An additive inverse limit carries integer scalar multiplication coordinatewise.
@[simp] theorem projection_zero (i : I) : S.projection i (0 : S.inverseLimit) = 0Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□@[simp] theorem projection_add (i : I) (x y : S.inverseLimit) :
S.projection i (x + y) = S.projection i x + S.projection i yProjection commutes with addition in an additive inverse system.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□@[simp] theorem projection_neg (i : I) (x : S.inverseLimit) :
S.projection i (-x) = -S.projection i xProjection commutes with negation in an additive inverse system.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□@[simp] theorem projection_sub (i : I) (x y : S.inverseLimit) :
S.projection i (x - y) = S.projection i x - S.projection i yProjection commutes with subtraction in an additive inverse system.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□instance instAddCommGroupAddInverseLimit : AddCommGroup S.inverseLimit := by
let f : S.inverseLimit → ∀ i, S.X i := Subtype.val
apply Subtype.val_injective.addCommGroup f rfl (fun _ _ => rfl) (fun _ => rfl)
(fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)Addition in the additive inverse limit is defined coordinatewise.
instance instSMulInverseLimitOfIsModuleSystem : SMul R S.inverseLimit where
smul r x := ⟨fun i => r • S.projection i x, by
intro i j hij
change S.map hij (r • S.projection j x) = r • S.projection i x
rw [IsModuleSystem.map_smul (S := S) hij, S.projection_compatible x i j hij]⟩An inverse-limit module carries scalar multiplication by applying the scalar action at every stage.
@[simp] theorem projection_smul_of_isModuleSystem (i : I) (r : R) (x : S.inverseLimit) :
S.projection i (r • x) = r • S.projection i xProjection commutes with scalar multiplication in a module-valued inverse system.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□instance instModuleInverseLimitOfIsModuleSystem : Module R S.inverseLimit := by
let f : S.inverseLimit →+ ∀ i, S.X i :=
{ toFun := Subtype.val
map_zero' := rfl
map_add' := fun _ _ => rfl }
exact Function.Injective.module R f Subtype.val_injective (fun _ _ => rfl)The inverse limit is a module when all stages form a compatible module system.
instance instContinuousSMulInverseLimitOfIsModuleSystem
[TopologicalSpace R] [∀ i, ContinuousSMul R (S.X i)] :
ContinuousSMul R S.inverseLimit where
continuous_smul := by
exact Continuous.subtype_mk
(continuous_pi fun i =>
continuous_fst.smul ((S.continuous_projection i).comp continuous_snd))
(fun p => by
intro i j hij
change S.map hij (p.1 • S.projection j p.2) = p.1 • S.projection i p.2
rw [IsModuleSystem.map_smul (S := S) hij, S.projection_compatible p.2 i j hij])Scalar multiplication is continuous for the relevant inverse-limit topology.
instance instIsTopologicalAddGroupAddInverseLimit [∀ i, IsTopologicalAddGroup (S.X i)] :
IsTopologicalAddGroup S.inverseLimit where
continuous_add := by
exact Continuous.subtype_mk
(continuous_pi fun i =>
((S.continuous_projection i).comp continuous_fst).add
((S.continuous_projection i).comp continuous_snd))
(fun xy => by
intro i j hij
change S.map hij (S.projection j xy.1 + S.projection j xy.2) =
S.projection i xy.1 + S.projection i xy.2
rw [IsAddGroupSystem.map_add (S := S) hij,
S.projection_compatible xy.1 i j hij, S.projection_compatible xy.2 i j hij])
continuous_neg := by
exact Continuous.subtype_mk
(continuous_pi fun i => continuous_neg.comp (S.continuous_projection i))
(fun x => by
intro i j hij
change S.map hij (-S.projection j x) = -S.projection i x
rw [IsAddGroupSystem.map_neg (S := S) hij, S.projection_compatible x i j hij])The additive inverse-limit object has addition defined coordinatewise on compatible families.
def projectionAddHom (i : I) : S.inverseLimit →+ S.X i where
toFun := S.projection i
map_zero' := projection_zero (S := S) i
map_add' := by
intro x y
exact projection_add (S := S) i x yThe canonical projections from an additive inverse limit are additive homomorphisms.
@[simp] theorem projectionAddHom_apply (i : I) (x : S.inverseLimit) :
projectionAddHom (S := S) i x = S.projection i xApplying an additive projection to an inverse-limit element returns its corresponding stage coordinate.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□class IsRingSystem (S : InverseSystem (I := I)) [∀ i, Ring (S.X i)] : Prop where
map_zero : ∀ {i j : I} (hij : i ≤ j), S.map hij 0 = 0
map_one : ∀ {i j : I} (hij : i ≤ j), S.map hij 1 = 1
map_add : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
S.map hij (x + y) = S.map hij x + S.map hij y
map_mul : ∀ {i j : I} (hij : i ≤ j) (x y : S.X j),
S.map hij (x * y) = S.map hij x * S.map hij yA ring-valued inverse system whose transition maps are ring homomorphisms.
def mapRingHom {i j : I} (hij : i ≤ j) : S.X j →+* S.X i where
toFun := S.map hij
map_zero' := IsRingSystem.map_zero (S := S) hij
map_one' := IsRingSystem.map_one (S := S) hij
map_add' := IsRingSystem.map_add (S := S) hij
map_mul' := IsRingSystem.map_mul (S := S) hij
@[simp]A transition map in a ring-valued inverse system is bundled as a ring homomorphism.
theorem mapRingHom_apply {i j : I} (hij : i ≤ j) (x : S.X j) :
mapRingHom (S := S) hij x = S.map hij xThe bundled ring homomorphism has the same underlying function as the coordinatewise construction.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□instance instIsAddGroupSystemOfIsRingSystem : IsAddGroupSystem S where
map_zero := IsRingSystem.map_zero (S := S)
map_add := IsRingSystem.map_add (S := S)
map_neg := by
intro i j hij x
exact (mapRingHom (S := S) hij).map_neg xThe additive inverse-limit object has addition defined coordinatewise on compatible families.
instance instMulRingInverseLimit : Mul S.inverseLimit where
mul x y := ⟨fun i => S.projection i x * S.projection i y, by
intro i j hij
calc
S.map hij (S.projection j x * S.projection j y)
= S.map hij (S.projection j x) * S.map hij (S.projection j y) := by
exact IsRingSystem.map_mul (S := S) hij (S.projection j x)
(S.projection j y)
_ = S.projection i x * S.projection i y := by
rw [S.projection_compatible x i j hij, S.projection_compatible y i j hij]⟩Ring multiplication on the inverse limit is defined coordinatewise through the stage ring multiplications.
instance instOneRingInverseLimit : One S.inverseLimit where
one := ⟨fun i => 1, by
intro i j hij
exact IsRingSystem.map_one (S := S) hij⟩The unit of the ring inverse limit is the compatible family of units at all stages.
instance instPowNatRingInverseLimit : Pow S.inverseLimit ℕ where
pow x n := ⟨fun i => S.projection i x ^ n, by
intro i j hij
change S.map hij (S.projection j x ^ n) = S.projection i x ^ n
rw [← mapRingHom_apply (S := S) hij, map_pow, mapRingHom_apply,
S.projection_compatible x i j hij]⟩Powers in the inverse-limit ring are computed at every stage coordinate.
instance instNatCastRingInverseLimit : NatCast S.inverseLimit where
natCast n := ⟨fun _ => n, by
intro i j hij
change S.map hij (Nat.cast n) = Nat.cast n
exact map_natCast (mapRingHom (S := S) hij) n⟩Natural number casts in a ring inverse limit are computed coordinatewise from finite-stage natural number casts.
instance instIntCastRingInverseLimit : IntCast S.inverseLimit where
intCast n := ⟨fun _ => n, by
intro i j hij
change S.map hij (Int.cast n) = Int.cast n
exact map_intCast (mapRingHom (S := S) hij) n⟩
@[simp]Integer casts in a ring inverse limit are computed coordinatewise from finite-stage integer casts.
theorem projection_ring_one (i : I) : S.projection i (1 : S.inverseLimit) = 1The inverse-limit projection preserves \(1\).
Show proof
rfl
@[simp]Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem projection_ring_mul (i : I) (x y : S.inverseLimit) :
S.projection i (x * y) = S.projection i x * S.projection i yThe inverse-limit projection preserves multiplication.
Show proof
rfl
@[simp]Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem projection_ring_pow (i : I) (x : S.inverseLimit) (n : ℕ) :
S.projection i (x ^ n) = S.projection i x ^ nThe inverse-limit projection preserves powers.
Show proof
rfl
@[simp]Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem projection_ring_natCast (i : I) (n : ℕ) :
S.projection i (Nat.cast n : S.inverseLimit) = Nat.cast nThe inverse-limit projection preserves natural number casts.
Show proof
rfl
@[simp]Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem projection_ring_intCast (i : I) (n : ℤ) :
S.projection i (Int.cast n : S.inverseLimit) = Int.cast nThe inverse-limit projection preserves integer casts.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□instance instRingInverseLimit : Ring S.inverseLimit :=
Function.Injective.ring
(fun x : S.inverseLimit => (x : ∀ i, S.X i))
Subtype.val_injective
(by funext i; rfl)
(by funext i; rfl)
(by intro x y; funext i; rfl)
(by intro x y; funext i; rfl)
(by intro x; funext i; rfl)
(by intro x y; funext i; rfl)
(by intro n x; funext i; rfl)
(by intro n x; funext i; rfl)
(by intro x n; funext i; rfl)
(by intro n; funext i; rfl)
(by intro n; funext i; rfl)A ring inverse limit is a ring because all operations and axioms are inherited coordinatewise from the stage rings.
instance instContinuousMulRingInverseLimit [∀ i, ContinuousMul (S.X i)] :
ContinuousMul S.inverseLimit where
continuous_mul := by
exact Continuous.subtype_mk
(continuous_pi fun i =>
((S.continuous_projection i).comp continuous_fst).mul
((S.continuous_projection i).comp continuous_snd))
(fun xy => by
intro i j hij
change S.map hij (S.projection j xy.1 * S.projection j xy.2) =
S.projection i xy.1 * S.projection i xy.2
rw [IsRingSystem.map_mul (S := S) hij,
S.projection_compatible xy.1 i j hij, S.projection_compatible xy.2 i j hij])Multiplication in a ring inverse limit is continuous for the inverse-limit topology.
instance instIsTopologicalRingRingInverseLimit [∀ i, IsTopologicalRing (S.X i)] :
IsTopologicalRing S.inverseLimit := by
letI : IsTopologicalAddGroup S.inverseLimit :=
instIsTopologicalAddGroupAddInverseLimit S
letI : ContinuousMul S.inverseLimit := instContinuousMulRingInverseLimit S
letI : IsTopologicalSemiring S.inverseLimit := IsTopologicalSemiring.mk
exact IsTopologicalRing.mkA ring inverse limit inherits a topological-ring structure from the compatible stage topological rings.
def projectionRingHom (i : I) : S.inverseLimit →+* S.X i where
toFun := S.projection i
map_zero' := projection_zero (S := S) i
map_one' := projection_ring_one (S := S) i
map_add' := by
intro x y
exact projection_add (S := S) i x y
map_mul' := by
intro x y
exact projection_ring_mul (S := S) i x y
@[simp]The canonical projection from a ring-valued inverse limit is bundled as a ring homomorphism.
theorem projectionRingHom_apply (i : I) (x : S.inverseLimit) :
projectionRingHom (S := S) i x = S.projection i xThe ring-homomorphism projection has the same underlying coordinate map as the finite-stage projection.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□theorem mapRingHom_comp_projectionRingHom {i j : I} (hij : i ≤ j) :
(mapRingHom (S := S) hij).comp (projectionRingHom (S := S) j) =
projectionRingHom (S := S) iComposing the ring-valued transition from \(j\) to \(i\) with the projection at \(j\) gives the projection at \(i\).
Show proof
by
apply RingHom.ext
intro x
exact S.projection_compatible x i j hijProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□