def IsPullbackSquare
(alpha1 : G ⟶ H1) (alpha2 : G ⟶ H2)
(beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H) : Prop :=
alpha1 ≫ beta1 = alpha2 ≫ beta2 ∧
∀ ⦃K : ProCGrp ProC⦄ (phi1 : K ⟶ H1) (phi2 : K ⟶ H2),
phi1 ≫ beta1 = phi2 ≫ beta2 →
∃! phi : K ⟶ G, phi ≫ alpha1 = phi1 ∧ phi ≫ alpha2 = phi2A pullback square in the bundled category pro-\(C\) groups.
noncomputable def pullbackLift
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}
{K : ProCGrp ProC}
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)
(phi1 : K ⟶ H1) (phi2 : K ⟶ H2)
(hphi : phi1 ≫ beta1 = phi2 ≫ beta2) : K ⟶ G :=
Classical.choose (ExistsUnique.exists (hpb.2 phi1 phi2 hphi))The pro-\(C\) pullback universal property supplies the induced morphism.
theorem pullbackLift_spec
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}
{K : ProCGrp ProC}
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)
(phi1 : K ⟶ H1) (phi2 : K ⟶ H2)
(hphi : phi1 ≫ beta1 = phi2 ≫ beta2) :
pullbackLift hpb phi1 phi2 hphi ≫ alpha1 = phi1 ∧
pullbackLift hpb phi1 phi2 hphi ≫ alpha2 = phi2The chosen pullback lift has the prescribed composites.
Show proof
Classical.choose_spec (ExistsUnique.exists (hpb.2 phi1 phi2 hphi))Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□@[simp] theorem pullbackLift_left
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}
{K : ProCGrp ProC}
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)
(phi1 : K ⟶ H1) (phi2 : K ⟶ H2)
(hphi : phi1 ≫ beta1 = phi2 ≫ beta2) :
pullbackLift hpb phi1 phi2 hphi ≫ alpha1 = phi1The pullback lift has the prescribed left projection.
Show proof
(pullbackLift_spec hpb phi1 phi2 hphi).1Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□@[simp] theorem pullbackLift_right
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}
{K : ProCGrp ProC}
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)
(phi1 : K ⟶ H1) (phi2 : K ⟶ H2)
(hphi : phi1 ≫ beta1 = phi2 ≫ beta2) :
pullbackLift hpb phi1 phi2 hphi ≫ alpha2 = phi2The pullback lift has the prescribed right projection.
Show proof
(pullbackLift_spec hpb phi1 phi2 hphi).2Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem pullbackLift_unique
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}
{K : ProCGrp ProC}
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)
(phi1 : K ⟶ H1) (phi2 : K ⟶ H2)
(hphi : phi1 ≫ beta1 = phi2 ≫ beta2)
{psi : K ⟶ G}
(hpsi : psi ≫ alpha1 = phi1 ∧ psi ≫ alpha2 = phi2) :
psi = pullbackLift hpb phi1 phi2 hphiUniqueness of the chosen pullback lift.
Show proof
by
rcases hpb.2 phi1 phi2 hphi with ⟨u, hu, huniq⟩
have hpsi' : psi = u := huniq _ hpsi
have hchosen : pullbackLift hpb phi1 phi2 hphi = u :=
huniq _ (pullbackLift_spec hpb phi1 phi2 hphi)
exact hpsi'.trans hchosen.symmProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□@[simp] theorem pullbackLift_self
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2) :
pullbackLift hpb alpha1 alpha2 hpb.1 = 𝟙 GThe self-lift of a pullback object is the identity morphism.
Show proof
by
symm
exact pullbackLift_unique hpb alpha1 alpha2 hpb.1 (psi := 𝟙 G) (by simp only [Category.id_comp, and_self])Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem pullback_hom_ext
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}
{K : ProCGrp ProC}
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)
{psi psi' : K ⟶ G}
(h1 : psi ≫ alpha1 = psi' ≫ alpha1)
(h2 : psi ≫ alpha2 = psi' ≫ alpha2) :
psi = psi'Extensionality of morphisms into a pro-\(C\) pullback object.
Show proof
by
have hphi : (psi ≫ alpha1) ≫ beta1 = (psi ≫ alpha2) ≫ beta2 := by
calc
(psi ≫ alpha1) ≫ beta1 = psi ≫ (alpha1 ≫ beta1) := by simp only [Category.assoc]
_ = psi ≫ (alpha2 ≫ beta2) := by rw [hpb.1]
_ = (psi ≫ alpha2) ≫ beta2 := by simp only [Category.assoc]
have hpsi :
psi = pullbackLift hpb (psi ≫ alpha1) (psi ≫ alpha2) hphi := by
exact pullbackLift_unique hpb (psi ≫ alpha1) (psi ≫ alpha2) hphi
(psi := psi) ⟨rfl, rfl⟩
have hpsi' :
psi' = pullbackLift hpb (psi ≫ alpha1) (psi ≫ alpha2) hphi := by
exact pullbackLift_unique hpb (psi ≫ alpha1) (psi ≫ alpha2) hphi
(psi := psi') ⟨h1.symm, h2.symm⟩
exact hpsi.trans hpsi'.symmProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□noncomputable def pullbackMapOfIsPullback
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{alpha1' : G' ⟶ H1} {alpha2' : G' ⟶ H2}
(beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H)
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)
(hpb' : IsPullbackSquare alpha1' alpha2' beta1 beta2) :
G' ⟶ G :=
pullbackLift hpb alpha1' alpha2' hpb'.1The canonical comparison map from one pro-\(C\) pullback object to another.
@[simp] theorem pullbackMapOfIsPullback_self
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
(beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H)
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2) :
pullbackMapOfIsPullback beta1 beta2 hpb hpb = 𝟙 GThe comparison map from a pullback object to itself is the identity.
Show proof
by
exact pullbackLift_self (hpb := hpb)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□@[simp] theorem pullbackMapOfIsPullback_left
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{alpha1' : G' ⟶ H1} {alpha2' : G' ⟶ H2}
(beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H)
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)
(hpb' : IsPullbackSquare alpha1' alpha2' beta1 beta2) :
pullbackMapOfIsPullback beta1 beta2 hpb hpb' ≫ alpha1 = alpha1'The comparison map between pullback objects respects the left projection.
Show proof
pullbackLift_left hpb alpha1' alpha2' hpb'.1Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□@[simp] theorem pullbackMapOfIsPullback_right
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{alpha1' : G' ⟶ H1} {alpha2' : G' ⟶ H2}
(beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H)
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)
(hpb' : IsPullbackSquare alpha1' alpha2' beta1 beta2) :
pullbackMapOfIsPullback beta1 beta2 hpb hpb' ≫ alpha2 = alpha2'The comparison map between pullback objects respects the right projection.
Show proof
pullbackLift_right hpb alpha1' alpha2' hpb'.1Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□noncomputable def pullbackIsoOfIsPullback
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{alpha1' : G' ⟶ H1} {alpha2' : G' ⟶ H2}
(beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H)
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)
(hpb' : IsPullbackSquare alpha1' alpha2' beta1 beta2) :
G ≅ G' where
hom := pullbackMapOfIsPullback beta1 beta2 hpb' hpb
inv := pullbackMapOfIsPullback beta1 beta2 hpb hpb'
hom_inv_id := by
apply pullback_hom_ext hpb
· calc
(pullbackMapOfIsPullback beta1 beta2 hpb' hpb ≫
pullbackMapOfIsPullback beta1 beta2 hpb hpb') ≫ alpha1 =
pullbackMapOfIsPullback beta1 beta2 hpb' hpb ≫ alpha1' := by
rw [Category.assoc, pullbackMapOfIsPullback_left]
_ = alpha1 := pullbackMapOfIsPullback_left beta1 beta2 hpb' hpb
· calc
(pullbackMapOfIsPullback beta1 beta2 hpb' hpb ≫
pullbackMapOfIsPullback beta1 beta2 hpb hpb') ≫ alpha2 =
pullbackMapOfIsPullback beta1 beta2 hpb' hpb ≫ alpha2' := by
rw [Category.assoc, pullbackMapOfIsPullback_right]
_ = alpha2 := pullbackMapOfIsPullback_right beta1 beta2 hpb' hpb
inv_hom_id := by
apply pullback_hom_ext hpb'
· calc
(pullbackMapOfIsPullback beta1 beta2 hpb hpb' ≫
pullbackMapOfIsPullback beta1 beta2 hpb' hpb) ≫ alpha1' =
pullbackMapOfIsPullback beta1 beta2 hpb hpb' ≫ alpha1 := by
rw [Category.assoc, pullbackMapOfIsPullback_left]
_ = alpha1' := pullbackMapOfIsPullback_left beta1 beta2 hpb hpb'
· calc
(pullbackMapOfIsPullback beta1 beta2 hpb hpb' ≫
pullbackMapOfIsPullback beta1 beta2 hpb' hpb) ≫ alpha2' =
pullbackMapOfIsPullback beta1 beta2 hpb hpb' ≫ alpha2 := by
rw [Category.assoc, pullbackMapOfIsPullback_right]
_ = alpha2' := pullbackMapOfIsPullback_right beta1 beta2 hpb hpb'Any two pro-\(C\) pullback objects of the same cospan are canonically isomorphic.
@[simp] theorem pullbackIsoOfIsPullback_hom_left
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{alpha1' : G' ⟶ H1} {alpha2' : G' ⟶ H2}
(beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H)
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)
(hpb' : IsPullbackSquare alpha1' alpha2' beta1 beta2) :
(pullbackIsoOfIsPullback beta1 beta2 hpb hpb').hom ≫ alpha1' = alpha1The canonical pullback isomorphism respects the left projection.
Show proof
pullbackMapOfIsPullback_left beta1 beta2 hpb' hpbProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. For equivalence and homeomorphism statements, the two comparison maps are composed in both orders and evaluated on the coordinates that determine the source. Each composite reduces to the identity transition or to the chosen representative identity on finite stages, so the algebraic inverse laws and the topological inverse laws follow simultaneously.
□@[simp] theorem pullbackIsoOfIsPullback_hom_right
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{alpha1' : G' ⟶ H1} {alpha2' : G' ⟶ H2}
(beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H)
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)
(hpb' : IsPullbackSquare alpha1' alpha2' beta1 beta2) :
(pullbackIsoOfIsPullback beta1 beta2 hpb hpb').hom ≫ alpha2' = alpha2The canonical pullback isomorphism respects the right projection.
Show proof
pullbackMapOfIsPullback_right beta1 beta2 hpb' hpbProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. For equivalence and homeomorphism statements, the two comparison maps are composed in both orders and evaluated on the coordinates that determine the source. Each composite reduces to the identity transition or to the chosen representative identity on finite stages, so the algebraic inverse laws and the topological inverse laws follow simultaneously.
□theorem isPullbackSquare_of_hasProfiniteTestPullbackProperty
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}
(hpb : ProCGroups.Categorical.HasProfiniteTestPullbackProperty
alpha1.hom alpha2.hom beta1.hom beta2.hom) :
IsPullbackSquare alpha1 alpha2 beta1 beta2A concrete continuous profinite pullback square is a pullback in ProCGrp.
Show proof
by
refine ⟨?_, ?_⟩
· apply hom_ext
change beta1.hom.comp alpha1.hom = beta2.hom.comp alpha2.hom
exact hpb.1
· intro K phi1 phi2 hphi
have hK : ProCGroups.IsProfiniteGroup K :=
ProCGroups.ProC.ProCGroup.profiniteGroup ProC K
have hphi' : beta1.hom.comp phi1.hom = beta2.hom.comp phi2.hom := by
simpa using congrArg (fun f : K ⟶ H => f.hom) hphi
rcases hpb.2 (K := K) hK phi1.hom phi2.hom hphi' with ⟨psi, hpsi, huniq⟩
let psi' : K ⟶ G := ConcreteCategory.ofHom (C := ProCGrp ProC) psi
refine ⟨psi', ?_, ?_⟩
· constructor
· apply hom_ext
change alpha1.hom.comp psi = phi1.hom
exact hpsi.1
· apply hom_ext
change alpha2.hom.comp psi = phi2.hom
exact hpsi.2
· intro theta htheta
apply hom_ext
change theta.hom = psi
apply huniq
constructor
· simpa using congrArg (fun f : K ⟶ H1 => f.hom) htheta.1
· simpa using congrArg (fun f : K ⟶ H2 => f.hom) htheta.2Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem hasProfiniteTestPullbackProperty_of_isPullbackSquare_allFinite
{G H H1 H2 : ProCGrp ProCGroups.ProC.allFiniteProC}
{alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
{beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}
(hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2) :
ProCGroups.Categorical.HasProfiniteTestPullbackProperty
alpha1.hom alpha2.hom beta1.hom beta2.homShow proof
by
refine ⟨?_, ?_⟩
· change (alpha1 ≫ beta1).hom = (alpha2 ≫ beta2).hom
exact congrArg (fun f : G ⟶ H => f.hom) hpb.1
· intro K _ _ _ hK phi1 phi2 hphi
letI : ProCGroups.ProC.ProCGroup ProCGroups.ProC.allFiniteProC K :=
ProCGroups.ProC.ProCGroup.of_isProCGroup ProCGroups.ProC.allFiniteProC K
(ProCGroups.ProC.allFiniteProC_isProCGroup_of_profinite hK)
let Kc : ProCGrp ProCGroups.ProC.allFiniteProC :=
ProCGrp.of ProCGroups.ProC.allFiniteProC K
let phi1' : Kc ⟶ H1 := ConcreteCategory.ofHom (C := ProCGrp ProCGroups.ProC.allFiniteProC) phi1
let phi2' : Kc ⟶ H2 := ConcreteCategory.ofHom (C := ProCGrp ProCGroups.ProC.allFiniteProC) phi2
have hphi' : phi1' ≫ beta1 = phi2' ≫ beta2 := by
apply hom_ext
exact hphi
rcases hpb.2 phi1' phi2' hphi' with ⟨psi, hpsi, huniq⟩
refine ⟨psi.hom, ?_, ?_⟩
· constructor
· simpa using congrArg (fun f : Kc ⟶ H1 => f.hom) hpsi.1
· simpa using congrArg (fun f : Kc ⟶ H2 => f.hom) hpsi.2
· intro theta htheta
let theta' : Kc ⟶ G :=
ConcreteCategory.ofHom (C := ProCGrp ProCGroups.ProC.allFiniteProC) theta
have htheta' : theta' ≫ alpha1 = phi1' ∧ theta' ≫ alpha2 = phi2' := by
constructor
· apply hom_ext
exact htheta.1
· apply hom_ext
exact htheta.2
have hthetaEq : theta' = psi := huniq theta' htheta'
simpa using congrArg (fun f : Kc ⟶ G => f.hom) hthetaEqProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For equivalence and homeomorphism statements, the two comparison maps are composed in both orders and evaluated on the coordinates that determine the source. Each composite reduces to the identity transition or to the chosen representative identity on finite stages, so the algebraic inverse laws and the topological inverse laws follow simultaneously.
□