def IsPushoutSquare
(β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
(α₁ : H₁ ⟶ G) (α₂ : H₂ ⟶ G) : Prop :=
β₁ ≫ α₁ = β₂ ≫ α₂ ∧
∀ ⦃K : ProCGrp ProC⦄ (φ₁ : H₁ ⟶ K) (φ₂ : H₂ ⟶ K),
β₁ ≫ φ₁ = β₂ ≫ φ₂ →
∃! φ : G ⟶ K, α₁ ≫ φ = φ₁ ∧ α₂ ≫ φ = φ₂A pushout square in the bundled category pro-\(C\) groups.
noncomputable def pushoutDesc
{β₁ : H ⟶ H₁} {β₂ : H ⟶ H₂}
{α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
{K : ProCGrp ProC}
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(φ₁ : H₁ ⟶ K) (φ₂ : H₂ ⟶ K)
(hφ : β₁ ≫ φ₁ = β₂ ≫ φ₂) : G ⟶ K :=
Classical.choose (ExistsUnique.exists (hpo.2 φ₁ φ₂ hφ))The pushout universal property supplies the induced morphism.
theorem pushoutDesc_spec
{β₁ : H ⟶ H₁} {β₂ : H ⟶ H₂}
{α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
{K : ProCGrp ProC}
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(φ₁ : H₁ ⟶ K) (φ₂ : H₂ ⟶ K)
(hφ : β₁ ≫ φ₁ = β₂ ≫ φ₂) :
α₁ ≫ pushoutDesc hpo φ₁ φ₂ hφ = φ₁ ∧
α₂ ≫ pushoutDesc hpo φ₁ φ₂ hφ = φ₂The chosen pushout descent map has the prescribed composites.
Show proof
Classical.choose_spec (ExistsUnique.exists (hpo.2 φ₁ φ₂ hφ))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 pushoutDesc_left
{β₁ : H ⟶ H₁} {β₂ : H ⟶ H₂}
{α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
{K : ProCGrp ProC}
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(φ₁ : H₁ ⟶ K) (φ₂ : H₂ ⟶ K)
(hφ : β₁ ≫ φ₁ = β₂ ≫ φ₂) :
α₁ ≫ pushoutDesc hpo φ₁ φ₂ hφ = φ₁The pushout descent map has the prescribed left composite.
Show proof
(pushoutDesc_spec hpo φ₁ φ₂ hφ).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. 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 pushoutDesc_right
{β₁ : H ⟶ H₁} {β₂ : H ⟶ H₂}
{α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
{K : ProCGrp ProC}
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(φ₁ : H₁ ⟶ K) (φ₂ : H₂ ⟶ K)
(hφ : β₁ ≫ φ₁ = β₂ ≫ φ₂) :
α₂ ≫ pushoutDesc hpo φ₁ φ₂ hφ = φ₂The pushout descent map has the prescribed right composite.
Show proof
(pushoutDesc_spec hpo φ₁ φ₂ hφ).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. 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.
□theorem pushoutDesc_unique
{β₁ : H ⟶ H₁} {β₂ : H ⟶ H₂}
{α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
{K : ProCGrp ProC}
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(φ₁ : H₁ ⟶ K) (φ₂ : H₂ ⟶ K)
(hφ : β₁ ≫ φ₁ = β₂ ≫ φ₂)
{ψ : G ⟶ K}
(hψ : α₁ ≫ ψ = φ₁ ∧ α₂ ≫ ψ = φ₂) :
ψ = pushoutDesc hpo φ₁ φ₂ hφUniqueness of the chosen pushout descent map.
Show proof
by
rcases hpo.2 φ₁ φ₂ hφ with ⟨u, hu, huuniq⟩
have hψ' : ψ = u := huuniq _ hψ
have hdesc : pushoutDesc hpo φ₁ φ₂ hφ = u :=
huuniq _ (pushoutDesc_spec hpo φ₁ φ₂ hφ)
exact hψ'.trans hdesc.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. 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 pushoutDesc_self
{β₁ : H ⟶ H₁} {β₂ : H ⟶ H₂}
{α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂) :
pushoutDesc hpo α₁ α₂ hpo.1 = 𝟙 GThe self-descent map of a pushout object is the identity.
Show proof
by
symm
exact pushoutDesc_unique hpo α₁ α₂ hpo.1 (ψ := 𝟙 G) (by simp only [Category.comp_id, 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. 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.
□theorem pushout_hom_ext
{β₁ : H ⟶ H₁} {β₂ : H ⟶ H₂}
{α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
{K : ProCGrp ProC}
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
{ψ ψ' : G ⟶ K}
(h₁ : α₁ ≫ ψ = α₁ ≫ ψ')
(h₂ : α₂ ≫ ψ = α₂ ≫ ψ') :
ψ = ψ'Extensionality of morphisms out of a pro-\(C\) pushout object.
Show proof
by
have hφ : β₁ ≫ (α₁ ≫ ψ) = β₂ ≫ (α₂ ≫ ψ) := by
calc
β₁ ≫ (α₁ ≫ ψ) = (β₁ ≫ α₁) ≫ ψ := by simp only [Category.assoc]
_ = (β₂ ≫ α₂) ≫ ψ := by rw [hpo.1]
_ = β₂ ≫ (α₂ ≫ ψ) := by simp only [Category.assoc]
have hψ :
ψ = pushoutDesc hpo (α₁ ≫ ψ) (α₂ ≫ ψ) hφ := by
exact pushoutDesc_unique hpo (α₁ ≫ ψ) (α₂ ≫ ψ) hφ (ψ := ψ) ⟨rfl, rfl⟩
have hψ' :
ψ' = pushoutDesc hpo (α₁ ≫ ψ) (α₂ ≫ ψ) hφ := by
exact pushoutDesc_unique hpo (α₁ ≫ ψ) (α₂ ≫ ψ) hφ
(ψ := ψ') ⟨h₁.symm, h₂.symm⟩
exact hψ.trans hψ'.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 pushoutMapOfIsPushout
{α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
{α₁' : H₁ ⟶ G'} {α₂' : H₂ ⟶ G'}
(β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
G ⟶ G' :=
pushoutDesc hpo α₁' α₂' hpo'.1The canonical comparison map between two pro-\(C\) pushout objects of the same cospan.
@[simp] theorem pushoutMapOfIsPushout_self
{α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
(β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂) :
pushoutMapOfIsPushout β₁ β₂ hpo hpo = 𝟙 GThe comparison map from a pushout object to itself is the identity.
Show proof
by
exact pushoutDesc_self (hpo := hpo)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 pushoutMapOfIsPushout_left
{α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
{α₁' : H₁ ⟶ G'} {α₂' : H₂ ⟶ G'}
(β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
α₁ ≫ pushoutMapOfIsPushout β₁ β₂ hpo hpo' = α₁'The left composite of the canonical comparison map between pushout objects is the prescribed left leg.
Show proof
pushoutDesc_left hpo α₁' α₂' hpo'.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. 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 pushoutMapOfIsPushout_right
{α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
{α₁' : H₁ ⟶ G'} {α₂' : H₂ ⟶ G'}
(β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
α₂ ≫ pushoutMapOfIsPushout β₁ β₂ hpo hpo' = α₂'The right composite of the canonical comparison map between pushout objects is the prescribed right leg.
Show proof
pushoutDesc_right hpo α₁' α₂' hpo'.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. 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.
□noncomputable def pushoutIsoOfIsPushout
{α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
{α₁' : H₁ ⟶ G'} {α₂' : H₂ ⟶ G'}
(β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
G ≅ G' where
hom := pushoutMapOfIsPushout β₁ β₂ hpo hpo'
inv := pushoutMapOfIsPushout β₁ β₂ hpo' hpo
hom_inv_id := by
apply pushout_hom_ext hpo
· calc
α₁ ≫ pushoutMapOfIsPushout β₁ β₂ hpo hpo' ≫
pushoutMapOfIsPushout β₁ β₂ hpo' hpo =
α₁' ≫ pushoutMapOfIsPushout β₁ β₂ hpo' hpo := by
rw [← Category.assoc, pushoutMapOfIsPushout_left]
_ = α₁ := pushoutMapOfIsPushout_left β₁ β₂ hpo' hpo
· calc
α₂ ≫ pushoutMapOfIsPushout β₁ β₂ hpo hpo' ≫
pushoutMapOfIsPushout β₁ β₂ hpo' hpo =
α₂' ≫ pushoutMapOfIsPushout β₁ β₂ hpo' hpo := by
rw [← Category.assoc, pushoutMapOfIsPushout_right]
_ = α₂ := pushoutMapOfIsPushout_right β₁ β₂ hpo' hpo
inv_hom_id := by
apply pushout_hom_ext hpo'
· calc
α₁' ≫ pushoutMapOfIsPushout β₁ β₂ hpo' hpo ≫
pushoutMapOfIsPushout β₁ β₂ hpo hpo' =
α₁ ≫ pushoutMapOfIsPushout β₁ β₂ hpo hpo' := by
rw [← Category.assoc, pushoutMapOfIsPushout_left]
_ = α₁' := pushoutMapOfIsPushout_left β₁ β₂ hpo hpo'
· calc
α₂' ≫ pushoutMapOfIsPushout β₁ β₂ hpo' hpo ≫
pushoutMapOfIsPushout β₁ β₂ hpo hpo' =
α₂ ≫ pushoutMapOfIsPushout β₁ β₂ hpo hpo' := by
rw [← Category.assoc, pushoutMapOfIsPushout_right]
_ = α₂' := pushoutMapOfIsPushout_right β₁ β₂ hpo hpo'Any two pro-\(C\) pushout objects of the same cospan are canonically isomorphic.
@[simp] theorem pushoutIsoOfIsPushout_hom_left
{α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
{α₁' : H₁ ⟶ G'} {α₂' : H₂ ⟶ G'}
(β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
α₁ ≫ (pushoutIsoOfIsPushout β₁ β₂ hpo hpo').hom = α₁'The pro-\(C\) pushout statement is verified by composing with the canonical maps and using the universal property.
Show proof
pushoutMapOfIsPushout_left β₁ β₂ hpo hpo'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 pushoutIsoOfIsPushout_hom_right
{α₁ : H₁ ⟶ G} {α₂ : H₂ ⟶ G}
{α₁' : H₁ ⟶ G'} {α₂' : H₂ ⟶ G'}
(β₁ : H ⟶ H₁) (β₂ : H ⟶ H₂)
(hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
(hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
α₂ ≫ (pushoutIsoOfIsPushout β₁ β₂ hpo hpo').hom = α₂'The pro-\(C\) pushout statement is verified by composing with the canonical maps and using the universal property.
Show proof
pushoutMapOfIsPushout_right β₁ β₂ hpo hpo'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.
□