This file proves Stacks Project, Tag 0BMV.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]abbrev OpenKernelSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]instance : Min (OpenKernel G) where
min H K :=
⟨H.1 ⊓ K.1, by
let : H.toOpenNormalSubgroup.toSubgroup.FiniteIndex := H.finiteIndex'
let : K.toOpenNormalSubgroup.toSubgroup.FiniteIndex := K.finiteIndex'
change Subgroup.FiniteIndex
(H.toOpenNormalSubgroup.toSubgroup ⊓ K.toOpenNormalSubgroup.toSubgroup)
infer_instance⟩Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]instance : SemilatticeInf (OpenKernel G)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def topOpenKernel : OpenKernel G where
val :=
{ toOpenSubgroup :=
{ toSubgroup := ⊤
isOpen' := isOpen_univ }
isNormal' := by infer_instance }
property := by infer_instanceSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]instance : Nonempty (OpenKernel G)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]instance quotientFintype (H : OpenKernel G) :
Fintype (G ⧸ H.toOpenNormalSubgroup.toSubgroup)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]instance quotientFinite (H : OpenKernel G) :
Finite (G ⧸ H.toOpenNormalSubgroup.toSubgroup)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem quotient_continuousSMul
(K : Subgroup G) [K.Normal]
[TopologicalSpace (G ⧸ K)] [DiscreteTopology (G ⧸ K)]
(hK : IsOpen (K : Set G)) :
ContinuousSMul G (G ⧸ K)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def quotientObject (H : OpenKernel G) :
ContAction FintypeCat.{u} GSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def quotientMap {H K : OpenKernel G} (f : H ⟶ K) :
quotientObject G H ⟶ quotientObject G KSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def quotientDiagram :
OpenKernel G ⥤ ContAction FintypeCat.{u} G where
obj := quotientObject G
map := quotientMap G
map_id H := by
apply ObjectProperty.hom_ext
apply Action.hom_ext
ext q
obtain ⟨g, rfl⟩ :=
QuotientGroup.mk'_surjective H.toOpenNormalSubgroup.toSubgroup q
rfl
map_comp {H K L} f g := by
apply ObjectProperty.hom_ext
apply Action.hom_ext
ext q
obtain ⟨a, rfl⟩ :=
QuotientGroup.mk'_surjective H.toOpenNormalSubgroup.toSubgroup q
rflSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]abbrev quotientFibers
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u}) :
OpenKernel G ⥤ Type uSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] intheorem nonempty_image_of_nonempty
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteColimits F] [PreservesFiniteLimits F]
(X : ContAction FintypeCat.{u} G)
[Nonempty
((forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj X)] :
Nonempty (F.obj X)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]instance quotientFiber_finite
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
(H : OpenKernel G) :
Finite ((quotientFibers G F).obj H)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]instance quotientFiber_nonempty
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteColimits F] [PreservesFiniteLimits F]
(H : OpenKernel G) :
Nonempty ((quotientFibers G F).obj H)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def coherentPoint
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteColimits F] [PreservesFiniteLimits F] :
(quotientFibers G F).sectionsSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]instance carrierMulAction
(X : ContAction FintypeCat.{u} G) :
MulAction G
((forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj X)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]instance carrierContinuousSMul
(X : ContAction FintypeCat.{u} G) :
ContinuousSMul G
((forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj X)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] intheorem actionKernel_isOpen
(X : ContAction FintypeCat.{u} G) :
IsOpen
((MulAction.toPermHom G
((forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj X)).ker :
Set G)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def actionKernelIndex
(X : ContAction FintypeCat.{u} G) : OpenKernel G where
val :=
{ toOpenSubgroup :=
{ toSubgroup :=
(MulAction.toPermHom G
((forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj X)).ker
isOpen' := actionKernel_isOpen G X }
isNormal' := by infer_instance }
property :=
Subgroup.finiteIndex_ker
(MulAction.toPermHom G
((forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj X))Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def evaluation
(X : ContAction FintypeCat.{u} G)
(x : (forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj X) :
quotientObject G (actionKernelIndex G X) ⟶ XSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem evaluation_common_refinement
{X Y : ContAction FintypeCat.{u} G} (f : X ⟶ Y)
(x : (forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj X) :
quotientMap G
(homOfLE inf_le_left :
actionKernelIndex G X ⊓ actionKernelIndex G Y ⟶
actionKernelIndex G X) ≫
evaluation G X x ≫ f =
quotientMap G
(homOfLE inf_le_right :
actionKernelIndex G X ⊓ actionKernelIndex G Y ⟶
actionKernelIndex G Y) ≫
evaluation G Y
((forget₂ (ContAction FintypeCat.{u} G) FintypeCat).map f x)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def fiberComparisonApp
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteColimits F] [PreservesFiniteLimits F]
(X : ContAction FintypeCat.{u} G) :
(forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj X ⟶ F.obj XSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def fiberComparison
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteColimits F] [PreservesFiniteLimits F] :
forget₂ (ContAction FintypeCat.{u} G) FintypeCat ⟶ F where
app := fiberComparisonApp G F
naturality {X Y} f := by
ext x
let HX := actionKernelIndex G X
let HY := actionKernelIndex G Y
let L := HX ⊓ HY
let pX : L ⟶ HX := homOfLE inf_le_left
let pY : L ⟶ HY := homOfLE inf_le_right
let γ := coherentPoint G F
let γL : (F.obj (quotientObject G L)).obj := γ.val L
have hγX :
F.map (quotientMap G pX) γL = γ.val HX := by
exact γ.property pX
have hγY :
F.map (quotientMap G pY) γL = γ.val HY := by
exact γ.property pY
have heval :
quotientMap G pX ≫ evaluation G X x ≫ f =
quotientMap G pY ≫ evaluation G Y
((forget₂ (ContAction FintypeCat.{u} G) FintypeCat).map f x) := by
exact evaluation_common_refinement G f x
change
F.map
(evaluation G Y
((forget₂ (ContAction FintypeCat.{u} G) FintypeCat).map f x))
(γ.val HY) =
F.map f
(F.map (evaluation G X x) (γ.val HX))
rw [← hγX, ← hγY]
simpa only [Functor.map_comp, ConcreteCategory.comp_apply] using
ConcreteCategory.congr_hom (F.congr_map heval.symm) γLSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def rightEndHomOnG (H : OpenKernel G) :
G →* End (quotientObject G H) where
toFun g :=
ObjectProperty.homMk <|
Action.FintypeCat.toEndHom
H.toOpenNormalSubgroup.toSubgroup g
map_one' := by
apply ObjectProperty.hom_ext
exact
(Action.FintypeCat.toEndHom
H.toOpenNormalSubgroup.toSubgroup).map_one
map_mul' g h := by
apply ObjectProperty.hom_ext
exact
(Action.FintypeCat.toEndHom
H.toOpenNormalSubgroup.toSubgroup).map_mul g hSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def rightEndHom (H : OpenKernel G) :
G ⧸ H.toOpenNormalSubgroup.toSubgroup →*
End (quotientObject G H)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem rightEndHom_mk_apply
(H : OpenKernel G) (g a : G) :
((rightEndHom G H (QuotientGroup.mk g)).hom.hom :
G ⧸ H.toOpenNormalSubgroup.toSubgroup →
G ⧸ H.toOpenNormalSubgroup.toSubgroup)
(QuotientGroup.mk a) =
QuotientGroup.mk (a * g⁻¹)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def rightActionDiagram (H : OpenKernel G) :
SingleObj (G ⧸ H.toOpenNormalSubgroup.toSubgroup) ⥤
ContAction FintypeCat.{u} GSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]instance hasRightActionColimits
(H : OpenKernel G) :
HasColimitsOfShape
(SingleObj (G ⧸ H.toOpenNormalSubgroup.toSubgroup))
(ContAction FintypeCat.{u} G)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]instance preservesRightActionColimits
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteColimits F] (H : OpenKernel G) :
PreservesColimitsOfShape
(SingleObj (G ⧸ H.toOpenNormalSubgroup.toSubgroup)) FSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]instance preservesRightActionColimitsToType
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteColimits F] (H : OpenKernel G) :
PreservesColimitsOfShape
(SingleObj (G ⧸ H.toOpenNormalSubgroup.toSubgroup))
(F ⋙ FintypeCat.incl)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem rightEndHom_apply
(H : OpenKernel G)
(r q : G ⧸ H.toOpenNormalSubgroup.toSubgroup) :
((rightEndHom G H r).hom.hom :
G ⧸ H.toOpenNormalSubgroup.toSubgroup →
G ⧸ H.toOpenNormalSubgroup.toSubgroup) q =
q * r⁻¹Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem quotient_right_pretransitive (H : OpenKernel G) :
let J :=
rightActionDiagram G H ⋙
forget₂ (ContAction FintypeCat.{u} G) FintypeCat ⋙
FintypeCat.incl
MulAction.IsPretransitive
(G ⧸ H.toOpenNormalSubgroup.toSubgroup)
(J.obj (SingleObj.star
(G ⧸ H.toOpenNormalSubgroup.toSubgroup))) := by
dsimp only
constructor
intro x y
change G ⧸ H.toOpenNormalSubgroup.toSubgroup at x y
refine ⟨y⁻¹ * x, ?_⟩
change
((rightEndHom G H (y⁻¹ * x)).hom.hom :
G ⧸ H.toOpenNormalSubgroup.toSubgroup →
G ⧸ H.toOpenNormalSubgroup.toSubgroup) x = y
rw [rightEndHom_apply]
group
rflSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def rightActionColimitTerminal
(H : OpenKernel G) :
IsTerminal (colimit (rightActionDiagram G H))Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem image_right_pretransitive
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteLimits F] [PreservesFiniteColimits F]
(H : OpenKernel G) :
let R := G ⧸ H.toOpenNormalSubgroup.toSubgroup
let JF := rightActionDiagram G H ⋙ F ⋙ FintypeCat.incl
MulAction.IsPretransitive R
(JF.obj (SingleObj.star R)) := by
let R := G ⧸ H.toOpenNormalSubgroup.toSubgroup
let J := rightActionDiagram G H
let JF := J ⋙ F ⋙ FintypeCat.incl
have hterminal : IsTerminal (F.obj (colimit J)) :=
IsTerminal.isTerminalObj F (colimit J)
(rightActionColimitTerminal G H)
let : Unique (F.obj (colimit J) : Type u) :=
Concrete.uniqueOfTerminalOfPreserves
(F.obj (colimit J)) hterminal
let e :
(F.obj (colimit J) : Type u) ≃
MulAction.orbitRel.Quotient R
(JF.obj (SingleObj.star R)) :=
(preservesColimitIso (F ⋙ FintypeCat.incl) J ≪≫
Equiv.toIso (SingleObj.Types.colimitEquivQuotient JF)).toEquiv
let : Unique
(MulAction.orbitRel.Quotient R
(JF.obj (SingleObj.star R))) :=
{ default := e default
uniq := fun x => e.symm.injective (Subsingleton.elim _ _) }
let : Nonempty (JF.obj (SingleObj.star R)) := by
change Nonempty (F.obj (quotientObject G H))
exact quotientFiber_nonempty G F H
exact
(MulAction.pretransitive_iff_unique_quotient_of_nonempty
R (JF.obj (SingleObj.star R))).mpr ⟨inferInstance⟩Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def finiteEqualizerEquiv
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteLimits F]
{X Y : ContAction FintypeCat.{u} G} (f g : X ⟶ Y) :
F.obj (equalizer f g) ≃
{ x : F.obj X // F.map f x = F.map g x }Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem rightEndHom_fixed_implies_one
(H : OpenKernel G)
(r : G ⧸ H.toOpenNormalSubgroup.toSubgroup)
(q :
(forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj
(quotientObject G H))
(hq :
(forget₂ (ContAction FintypeCat.{u} G) FintypeCat).map
(rightEndHom G H r) q = q) :
r = 1Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem image_right_fixed_implies_one
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteLimits F] [PreservesFiniteColimits F]
(H : OpenKernel G)
(r : G ⧸ H.toOpenNormalSubgroup.toSubgroup)
(s : F.obj (quotientObject G H))
(hs : F.map (rightEndHom G H r) s = s) :
r = 1Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem image_right_transitive
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteLimits F] [PreservesFiniteColimits F]
(H : OpenKernel G)
(x y : F.obj (quotientObject G H)) :
∃ r : G ⧸ H.toOpenNormalSubgroup.toSubgroup,
F.map (rightEndHom G H r) x = ySurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem fiberComparison_right_equivariant
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteLimits F] [PreservesFiniteColimits F]
(H : OpenKernel G)
(r : G ⧸ H.toOpenNormalSubgroup.toSubgroup)
(q :
(forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj
(quotientObject G H)) :
fiberComparisonApp G F (quotientObject G H)
((forget₂ (ContAction FintypeCat.{u} G) FintypeCat).map
(rightEndHom G H r) q) =
F.map (rightEndHom G H r)
(fiberComparisonApp G F (quotientObject G H) q)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem fiberComparison_quotient_bijective
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteLimits F] [PreservesFiniteColimits F]
(H : OpenKernel G) :
Function.Bijective
(fiberComparisonApp G F (quotientObject G H))Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def copiesDiagram
(X : ContAction FintypeCat.{u} G) :
Discrete
((forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj X) ⥤
ContAction FintypeCat.{u} GSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]abbrev copiesObject
(X : ContAction FintypeCat.{u} G) :
ContAction FintypeCat.{u} GSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def copiesCover
(X : ContAction FintypeCat.{u} G) :
copiesObject G X ⟶ XSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem copies_ι_cover
(X : ContAction FintypeCat.{u} G)
(x : (forget₂
(ContAction FintypeCat.{u} G) FintypeCat).obj X) :
colimit.ι (copiesDiagram G X) ⟨x⟩ ≫ copiesCover G X =
evaluation G X xSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem evaluation_one
(X : ContAction FintypeCat.{u} G)
(x : (forget₂
(ContAction FintypeCat.{u} G) FintypeCat).obj X) :
(forget₂ (ContAction FintypeCat.{u} G) FintypeCat).map
(evaluation G X x)
(QuotientGroup.mk 1) = xSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem copiesCover_surjective
(X : ContAction FintypeCat.{u} G) :
Function.Surjective (copiesCover G X)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem fiberComparison_copies_isIso
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteLimits F] [PreservesFiniteColimits F]
(X : ContAction FintypeCat.{u} G) :
IsIso
((fiberComparison G F).app (copiesObject G X))Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]def finitePullbackEquiv
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteLimits F]
{X A B : ContAction FintypeCat.{u} G}
(f : A ⟶ X) (g : B ⟶ X) :
F.obj (pullback f g) ≃
{ p : F.obj A × F.obj B //
F.map f p.1 = F.map g p.2 }Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] intheorem finitePullbackEquiv_symm_fst_apply
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteLimits F]
{X A B : ContAction FintypeCat.{u} G}
{f : A ⟶ X} {g : B ⟶ X}
(a : F.obj A) (b : F.obj B)
(h : F.map f a = F.map g b) :
F.map (pullback.fst f g)
((finitePullbackEquiv G F f g).symm
⟨(a, b), h⟩) = aSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] intheorem finitePullbackEquiv_symm_snd_apply
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteLimits F]
{X A B : ContAction FintypeCat.{u} G}
{f : A ⟶ X} {g : B ⟶ X}
(a : F.obj A) (b : F.obj B)
(h : F.map f a = F.map g b) :
F.map (pullback.snd f g)
((finitePullbackEquiv G F f g).symm
⟨(a, b), h⟩) = bSurrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem fiberComparison_surjective
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteLimits F] [PreservesFiniteColimits F]
(X : ContAction FintypeCat.{u} G) :
Function.Surjective
((fiberComparison G F).app X)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem fiberComparison_injective
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteLimits F] [PreservesFiniteColimits F]
(X : ContAction FintypeCat.{u} G) :
Function.Injective
((fiberComparison G F).app X)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem fiberComparison_bijective
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteLimits F] [PreservesFiniteColimits F]
(X : ContAction FintypeCat.{u} G) :
Function.Bijective
((fiberComparison G F).app X)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]theorem nonempty_iso_forget_of_exact
(F : ContAction FintypeCat.{u} G ⥤ FintypeCat.{u})
[PreservesFiniteLimits F] [PreservesFiniteColimits F] :
Nonempty
(forget₂ (ContAction FintypeCat.{u} G) FintypeCat ≅ F)