Loogle!

Result

Found 154 declarations mentioning CategoryTheory.Aut.

• CategoryTheory.Aut 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : Type v
• CategoryTheory.Aut.inhabited 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : Inhabited (CategoryTheory.Aut X)
• CategoryTheory.Aut.instGroup 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : Group (CategoryTheory.Aut X)
• CategoryTheory.Aut.ext 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {φ₁ φ₂ : CategoryTheory.Aut X} (h : φ₁.hom = φ₂.hom) : φ₁ = φ₂
• CategoryTheory.Aut.ext_iff 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {φ₁ φ₂ : CategoryTheory.Aut X} : φ₁ = φ₂ ↔ φ₁.hom = φ₂.hom
• CategoryTheory.Aut.Aut_inv_def 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (f : CategoryTheory.Aut X) : f⁻¹ = CategoryTheory.Iso.symm f
• CategoryTheory.Aut.toEnd 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : CategoryTheory.Aut X →* CategoryTheory.End X
• CategoryTheory.Aut.unitsEndEquivAut 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.End X)ˣ ≃* CategoryTheory.Aut X
• CategoryTheory.Aut.Aut_mul_def 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (f g : CategoryTheory.Aut X) : f * g = g ≪≫ f
• CategoryTheory.Aut.autMulEquivOfIso 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : X ≅ Y) : CategoryTheory.Aut X ≃* CategoryTheory.Aut Y
• CategoryTheory.Functor.mapAut 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] (f : CategoryTheory.Functor C D) : CategoryTheory.Aut X →* CategoryTheory.Aut (f.obj X)
• CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) : CategoryTheory.Aut X ≃* CategoryTheory.Aut (f.obj X)
• CategoryTheory.Aut.toEnd_apply 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (x : CategoryTheory.Aut X) : (CategoryTheory.Aut.toEnd X) x = ↑((CategoryTheory.Aut.unitsEndEquivAut X).symm x)
• CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_hom 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (i : X ≅ X) : ((hf.autMulEquivOfFullyFaithful X) i).hom = f.map i.hom
• CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_inv 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (i : X ≅ X) : ((hf.autMulEquivOfFullyFaithful X) i).inv = f.map i.inv
• CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_hom 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (e : f.obj X ≅ f.obj X) : ((hf.autMulEquivOfFullyFaithful X).symm e).hom = hf.preimage e.hom
• CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_inv 📋 Mathlib.CategoryTheory.Endomorphism
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (e : f.obj X ≅ f.obj X) : ((hf.autMulEquivOfFullyFaithful X).symm e).inv = hf.preimage e.inv
• CategoryTheory.Aut.isoPerm 📋 Mathlib.Algebra.Category.Grp.Basic
  {α : Type u} : GrpCat.of (CategoryTheory.Aut α) ≅ GrpCat.of (Equiv.Perm α)
• CategoryTheory.Aut.mulEquivPerm 📋 Mathlib.Algebra.Category.Grp.Basic
  {α : Type u} : CategoryTheory.Aut α ≃* Equiv.Perm α
• CategoryTheory.Iso.conjAut 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) : CategoryTheory.Aut X ≃* CategoryTheory.Aut Y
• CategoryTheory.Iso.conjAut_apply 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) : α.conjAut f = α.symm ≪≫ f ≪≫ α
• CategoryTheory.Iso.conjAut_hom 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) : (α.conjAut f).hom = α.conj f.hom
• CategoryTheory.Iso.conjAut_zpow 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) (n : ℤ) : α.conjAut (f ^ n) = α.conjAut f ^ n
• CategoryTheory.Iso.conjAut_pow 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) (n : ℕ) : α.conjAut (f ^ n) = α.conjAut f ^ n
• CategoryTheory.Iso.trans_conjAut 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (β : Y ≅ Z) (f : CategoryTheory.Aut X) : (α ≪≫ β).conjAut f = β.conjAut (α.conjAut f)
• CategoryTheory.Iso.conjAut_trans 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f g : CategoryTheory.Aut X) : α.conjAut (f ≪≫ g) = α.conjAut f ≪≫ α.conjAut g
• CategoryTheory.Iso.conjAut_mul 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f g : CategoryTheory.Aut X) : α.conjAut (f * g) = α.conjAut f * α.conjAut g
• CategoryTheory.Functor.map_conjAut 📋 Mathlib.CategoryTheory.Conj
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C D) {X Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) : F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.mapIso f)
• FintypeCat.instFiniteAut 📋 Mathlib.CategoryTheory.FintypeCat
  (X : FintypeCat) : Finite (CategoryTheory.Aut X)
• Units.toAut 📋 Mathlib.CategoryTheory.SingleObj
  (M : Type u) [Monoid M] : Mˣ ≃* CategoryTheory.Aut (CategoryTheory.SingleObj.star M)
• Units.toAut_hom 📋 Mathlib.CategoryTheory.SingleObj
  (M : Type u) [Monoid M] (x : Mˣ) : ((Units.toAut M) x).hom = (CategoryTheory.SingleObj.toEnd M) ↑x
• Units.toAut_inv 📋 Mathlib.CategoryTheory.SingleObj
  (M : Type u) [Monoid M] (x : Mˣ) : ((Units.toAut M) x).inv = (CategoryTheory.SingleObj.toEnd M) ↑x⁻¹
• Action.ρAut 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Group G] (A : Action V G) : G →* CategoryTheory.Aut A.V
• Action.ρAut_apply_hom 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Group G] (A : Action V G) (g : G) : (A.ρAut g).hom = A.ρ g
• Action.ρAut_apply_inv 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Group G] (A : Action V G) (g : G) : (A.ρAut g).inv = A.ρ g⁻¹
• CategoryTheory.PreGaloisCategory.instFiniteAutOfIsConnected 📋 Mathlib.CategoryTheory.Galois.Basic
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (A : C) [CategoryTheory.PreGaloisCategory.IsConnected A] : Finite (CategoryTheory.Aut A)
• CategoryTheory.PreGaloisCategory.card_aut_le_card_fiber_of_connected 📋 Mathlib.CategoryTheory.Galois.Basic
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C) [CategoryTheory.PreGaloisCategory.IsConnected A] : Nat.card (CategoryTheory.Aut A) ≤ Nat.card (F.obj A).obj
• CategoryTheory.PreGaloisCategory.instMulActionAutFunctorFintypeCatObjFiniteObj 📋 Mathlib.CategoryTheory.Galois.Basic
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) : MulAction (CategoryTheory.Aut F) (F.obj X).obj
• CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected 📋 Mathlib.CategoryTheory.Galois.Basic
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C) [CategoryTheory.PreGaloisCategory.IsConnected A] (a : (F.obj A).obj) : Function.Injective fun f => (CategoryTheory.ConcreteCategory.hom (F.map f.hom)) a
• CategoryTheory.PreGaloisCategory.mulAction_def 📋 Mathlib.CategoryTheory.Galois.Basic
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {X : C} (σ : CategoryTheory.Aut F) (x : (F.obj X).obj) : σ • x = (CategoryTheory.ConcreteCategory.hom (σ.hom.app X)) x
• CategoryTheory.PreGaloisCategory.mulAction_naturality 📋 Mathlib.CategoryTheory.Galois.Basic
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {X Y : C} (σ : CategoryTheory.Aut F) (f : X ⟶ Y) (x : (F.obj X).obj) : σ • (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f)) (σ • x)
• CategoryTheory.PreGaloisCategory.autMap 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {A B : C} [CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.PreGaloisCategory.IsGalois B] (f : A ⟶ B) (σ : CategoryTheory.Aut A) : CategoryTheory.Aut B
• CategoryTheory.PreGaloisCategory.autMap_id 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {A : C} [CategoryTheory.PreGaloisCategory.IsGalois A] : CategoryTheory.PreGaloisCategory.autMap (CategoryTheory.CategoryStruct.id A) = id
• CategoryTheory.PreGaloisCategory.autMulFiber 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) : MulAction (CategoryTheory.Aut X) (F.obj X).obj
• CategoryTheory.PreGaloisCategory.autMap_surjective_of_isGalois 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {A B : C} [CategoryTheory.PreGaloisCategory.IsGalois A] [CategoryTheory.PreGaloisCategory.IsGalois B] (f : A ⟶ B) : Function.Surjective (CategoryTheory.PreGaloisCategory.autMap f)
• CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C) [CategoryTheory.PreGaloisCategory.IsGalois A] (a : (F.obj A).obj) : CategoryTheory.Aut A ≃ (F.obj A).obj
• CategoryTheory.PreGaloisCategory.comp_autMap 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {A B : C} [CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.PreGaloisCategory.IsGalois B] (f : A ⟶ B) (σ : CategoryTheory.Aut A) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.PreGaloisCategory.autMap f σ).hom = CategoryTheory.CategoryStruct.comp σ.hom f
• CategoryTheory.PreGaloisCategory.exists_autMap 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {A B : C} (f : A ⟶ B) [CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.PreGaloisCategory.IsGalois B] (σ : CategoryTheory.Aut A) : ∃! τ, CategoryTheory.CategoryStruct.comp f τ.hom = CategoryTheory.CategoryStruct.comp σ.hom f
• CategoryTheory.PreGaloisCategory.autMapHom 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {A B : C} [CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.PreGaloisCategory.IsGalois B] (f : A ⟶ B) : CategoryTheory.Aut A →* CategoryTheory.Aut B
• CategoryTheory.PreGaloisCategory.autMap_unique 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {A B : C} [CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.PreGaloisCategory.IsGalois B] (f : A ⟶ B) (σ : CategoryTheory.Aut A) (τ : CategoryTheory.Aut B) (h : CategoryTheory.CategoryStruct.comp f τ.hom = CategoryTheory.CategoryStruct.comp σ.hom f) : CategoryTheory.PreGaloisCategory.autMap f σ = τ
• CategoryTheory.PreGaloisCategory.autMap_comp 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {X Y Z : C} [CategoryTheory.PreGaloisCategory.IsConnected X] [CategoryTheory.PreGaloisCategory.IsGalois Y] [CategoryTheory.PreGaloisCategory.IsGalois Z] (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.PreGaloisCategory.autMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.PreGaloisCategory.autMap g ∘ CategoryTheory.PreGaloisCategory.autMap f
• CategoryTheory.PreGaloisCategory.isPretransitive_of_isGalois 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X] : MulAction.IsPretransitive (CategoryTheory.Aut X) (F.obj X).obj
• CategoryTheory.PreGaloisCategory.isGalois_iff_pretransitive 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X] : CategoryTheory.PreGaloisCategory.IsGalois X ↔ MulAction.IsPretransitive (CategoryTheory.Aut X) (F.obj X).obj
• CategoryTheory.PreGaloisCategory.stabilizer_normal_of_isGalois 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X] (x : (F.obj X).obj) : (MulAction.stabilizer (CategoryTheory.Aut F) x).Normal
• CategoryTheory.PreGaloisCategory.isTerminalQuotientOfIsGalois 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X] : CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X)))
• CategoryTheory.PreGaloisCategory.IsGalois.mk 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {X : C} [toIsConnected : CategoryTheory.PreGaloisCategory.IsConnected X] (quotientByAutTerminal : Nonempty (CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X))))) : CategoryTheory.PreGaloisCategory.IsGalois X
• CategoryTheory.PreGaloisCategory.isGalois_iff_aux 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X] : CategoryTheory.PreGaloisCategory.IsGalois X ↔ Nonempty (CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X))))
• CategoryTheory.PreGaloisCategory.IsGalois.quotientByAutTerminal 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{u₂, u₁} C} {inst✝¹ : CategoryTheory.GaloisCategory C} {X : C} [self : CategoryTheory.PreGaloisCategory.IsGalois X] : Nonempty (CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X))))
• CategoryTheory.PreGaloisCategory.autMap_apply_mul 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {A B : C} [CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.PreGaloisCategory.IsGalois B] (f : A ⟶ B) (σ τ : CategoryTheory.Aut A) : CategoryTheory.PreGaloisCategory.autMap f (σ * τ) = CategoryTheory.PreGaloisCategory.autMap f σ * CategoryTheory.PreGaloisCategory.autMap f τ
• CategoryTheory.PreGaloisCategory.autMapHom_apply 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {A B : C} [CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.PreGaloisCategory.IsGalois B] (f : A ⟶ B) (σ : CategoryTheory.Aut A) : (CategoryTheory.PreGaloisCategory.autMapHom f) σ = CategoryTheory.PreGaloisCategory.autMap f σ
• CategoryTheory.PreGaloisCategory.quotientByAutTerminalEquivUniqueQuotient 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X] : CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X))) ≃ Unique (MulAction.orbitRel.Quotient (CategoryTheory.Aut X) (F.obj X).obj)
• CategoryTheory.PreGaloisCategory.evaluation_aut_bijective_of_isGalois 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C) [CategoryTheory.PreGaloisCategory.IsGalois A] (a : (F.obj A).obj) : Function.Bijective fun f => (CategoryTheory.ConcreteCategory.hom (F.map f.hom)) a
• CategoryTheory.PreGaloisCategory.evaluation_aut_surjective_of_isGalois 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C) [CategoryTheory.PreGaloisCategory.IsGalois A] (a : (F.obj A).obj) : Function.Surjective fun f => (CategoryTheory.ConcreteCategory.hom (F.map f.hom)) a
• CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_apply 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C) [CategoryTheory.PreGaloisCategory.IsGalois A] (a : (F.obj A).obj) (φ : CategoryTheory.Aut A) : (CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois F A a) φ = (CategoryTheory.ConcreteCategory.hom (F.map φ.hom)) a
• CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_symm_fiber 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C) [CategoryTheory.PreGaloisCategory.IsGalois A] (a b : (F.obj A).obj) : (CategoryTheory.ConcreteCategory.hom (F.map ((CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois F A a).symm b).hom)) a = b
• CategoryTheory.PreGaloisCategory.comp_autMap_apply 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) {A B : C} [CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.PreGaloisCategory.IsGalois B] (f : A ⟶ B) (σ : CategoryTheory.Aut A) (a : (F.obj A).obj) : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.PreGaloisCategory.autMap f σ).hom)) ((CategoryTheory.ConcreteCategory.hom (F.map f)) a) = (CategoryTheory.ConcreteCategory.hom (F.map f)) ((CategoryTheory.ConcreteCategory.hom (F.map σ.hom)) a)
• CategoryTheory.PreGaloisCategory.autGaloisSystem_obj_coe 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : ↑((CategoryTheory.PreGaloisCategory.autGaloisSystem F).obj A) = CategoryTheory.Aut A.obj
• CategoryTheory.PreGaloisCategory.AutGalois.π 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : CategoryTheory.PreGaloisCategory.AutGalois F →* CategoryTheory.Aut A.obj
• CategoryTheory.PreGaloisCategory.autGaloisSystem_map 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} (f : A ⟶ B) : (CategoryTheory.PreGaloisCategory.autGaloisSystem F).map f = GrpCat.ofHom (CategoryTheory.PreGaloisCategory.autMapHom f.val)
• CategoryTheory.PreGaloisCategory.autMulEquivAutGalois 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.Aut F ≃* (CategoryTheory.PreGaloisCategory.AutGalois F)ᵐᵒᵖ
• CategoryTheory.PreGaloisCategory.AutGalois.π_surjective 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : Function.Surjective ⇑(CategoryTheory.PreGaloisCategory.AutGalois.π F A)
• CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isConnected 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X] : MulAction.IsPretransitive (CategoryTheory.Aut F) (F.obj X).obj
• CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isGalois 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X] : MulAction.IsPretransitive (CategoryTheory.Aut F) (F.obj X).obj
• CategoryTheory.PreGaloisCategory.AutGalois.ext 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) {f g : CategoryTheory.PreGaloisCategory.AutGalois F} (h : ∀ (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F), (CategoryTheory.PreGaloisCategory.AutGalois.π F A) f = (CategoryTheory.PreGaloisCategory.AutGalois.π F A) g) : f = g
• CategoryTheory.PreGaloisCategory.AutGalois.π_apply 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) (x : CategoryTheory.PreGaloisCategory.AutGalois F) : (CategoryTheory.PreGaloisCategory.AutGalois.π F A) x = ↑x A
• CategoryTheory.PreGaloisCategory.endEquivAutGalois_π 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.End F) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : (CategoryTheory.ConcreteCategory.hom (F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F A) ((CategoryTheory.PreGaloisCategory.endEquivAutGalois F) f)).hom)) A.pt = (CategoryTheory.ConcreteCategory.hom (f.app A.obj)) A.pt
• CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.End F) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) : (CategoryTheory.ConcreteCategory.hom (F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F A) (MulOpposite.unop ((CategoryTheory.PreGaloisCategory.endMulEquivAutGalois F) f))).hom)) A.pt = (CategoryTheory.ConcreteCategory.hom (f.app A.obj)) A.pt
• CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) (b : (F.obj A.obj).obj) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.PreGaloisCategory.autIsoFibers F).inv.app A)) b = (CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois F A.obj A.pt).symm b
• CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_π 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (f : CategoryTheory.Aut F) (A : C) [CategoryTheory.PreGaloisCategory.IsGalois A] (a : (F.obj A).obj) : (CategoryTheory.ConcreteCategory.hom (F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) (MulOpposite.unop ((CategoryTheory.PreGaloisCategory.autMulEquivAutGalois F) f))).hom)) a = (CategoryTheory.ConcreteCategory.hom (f.hom.app A)) a
• CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_symm_app 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (x : CategoryTheory.PreGaloisCategory.AutGalois F) (A : C) [CategoryTheory.PreGaloisCategory.IsGalois A] (a : (F.obj A).obj) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.PreGaloisCategory.autMulEquivAutGalois F).symm { unop' := x }).hom.app A)) a = (CategoryTheory.ConcreteCategory.hom (F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) x).hom)) a
• CategoryTheory.PreGaloisCategory.functorToAction 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) : CategoryTheory.Functor C (Action FintypeCat (CategoryTheory.Aut F))
• CategoryTheory.PreGaloisCategory.instFaithfulActionFintypeCatAutFunctorFunctorToAction 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : (CategoryTheory.PreGaloisCategory.functorToAction F).Faithful
• CategoryTheory.PreGaloisCategory.instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.Limits.PreservesFiniteCoproducts (CategoryTheory.PreGaloisCategory.functorToAction F)
• CategoryTheory.PreGaloisCategory.instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.PreGaloisCategory.functorToAction F)
• CategoryTheory.PreGaloisCategory.instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.PreGaloisCategory.PreservesIsConnected (CategoryTheory.PreGaloisCategory.functorToAction F)
• CategoryTheory.PreGaloisCategory.instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : (CategoryTheory.PreGaloisCategory.functorToAction F).PreservesMonomorphisms
• CategoryTheory.PreGaloisCategory.instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : (CategoryTheory.PreGaloisCategory.functorToAction F).ReflectsIsomorphisms
• CategoryTheory.PreGaloisCategory.instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : (CategoryTheory.PreGaloisCategory.functorToAction F).ReflectsMonomorphisms
• CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (G : Type u_2) [Group G] [Finite G] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.SingleObj G) (CategoryTheory.PreGaloisCategory.functorToAction F)
• CategoryTheory.PreGaloisCategory.instMulActionAutObjFiniteVFintypeCatFunctorObjActionFunctorToAction 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) : MulAction (CategoryTheory.Aut X) ((CategoryTheory.PreGaloisCategory.functorToAction F).obj X).V.obj
• CategoryTheory.PreGaloisCategory.instIsPretransitiveAutObjFiniteVFintypeCatFunctorObjActionFunctorToActionOfIsGalois 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X] : MulAction.IsPretransitive (CategoryTheory.Aut X) ((CategoryTheory.PreGaloisCategory.functorToAction F).obj X).V.obj
• CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) : (CategoryTheory.PreGaloisCategory.functorToAction F).comp (CategoryTheory.forget₂ (Action FintypeCat (CategoryTheory.Aut F)) FintypeCat) = F
• CategoryTheory.PreGaloisCategory.functorToAction_map 📋 Mathlib.CategoryTheory.Galois.Action
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) {X Y : C} (f : X ⟶ Y) : ((CategoryTheory.PreGaloisCategory.functorToAction F).map f).hom = F.map f
• CategoryTheory.PreGaloisCategory.functorToAction_full 📋 Mathlib.CategoryTheory.Galois.Full
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : (CategoryTheory.PreGaloisCategory.functorToAction F).Full
• CategoryTheory.PreGaloisCategory.exists_lift_of_mono 📋 Mathlib.CategoryTheory.Galois.Full
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) (Y : Action FintypeCat (CategoryTheory.Aut F)) (i : Y ⟶ (CategoryTheory.PreGaloisCategory.functorToAction F).obj X) [CategoryTheory.Mono i] : ∃ Z f u, CategoryTheory.Mono f ∧ CategoryTheory.CategoryStruct.comp u.hom ((CategoryTheory.PreGaloisCategory.functorToAction F).map f) = i
• CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected 📋 Mathlib.CategoryTheory.Galois.Full
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) (Y : Action FintypeCat (CategoryTheory.Aut F)) (i : Y ⟶ (CategoryTheory.PreGaloisCategory.functorToAction F).obj X) [CategoryTheory.Mono i] [CategoryTheory.PreGaloisCategory.IsConnected Y] : ∃ Z f u, CategoryTheory.PreGaloisCategory.IsConnected Z ∧ CategoryTheory.Mono f ∧ i = CategoryTheory.CategoryStruct.comp u.hom ((CategoryTheory.PreGaloisCategory.functorToAction F).map f)
• CategoryTheory.PreGaloisCategory.instTopologicalSpaceAutFintypeCatObj 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) : TopologicalSpace (CategoryTheory.Aut (F.obj X))
• CategoryTheory.PreGaloisCategory.instTopologicalSpaceAutFunctorFintypeCat 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : TopologicalSpace (CategoryTheory.Aut F)
• CategoryTheory.PreGaloisCategory.aut_discreteTopology 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) : DiscreteTopology (CategoryTheory.Aut (F.obj X))
• CategoryTheory.PreGaloisCategory.instCompactSpaceAutFunctorFintypeCat 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : CompactSpace (CategoryTheory.Aut F)
• CategoryTheory.PreGaloisCategory.instT2SpaceAutFunctorFintypeCat 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : T2Space (CategoryTheory.Aut F)
• CategoryTheory.PreGaloisCategory.instTotallyDisconnectedSpaceAutFunctorFintypeCat 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : TotallyDisconnectedSpace (CategoryTheory.Aut F)
• CategoryTheory.PreGaloisCategory.instSMulAutFintypeCatObjObjFinite 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) : SMul (CategoryTheory.Aut (F.obj X)) (F.obj X).obj
• CategoryTheory.PreGaloisCategory.instIsTopologicalGroupAutFunctorFintypeCat 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : IsTopologicalGroup (CategoryTheory.Aut F)
• CategoryTheory.PreGaloisCategory.instContinuousSMulAutFintypeCatObjObjFinite 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) : ContinuousSMul (CategoryTheory.Aut (F.obj X)) (F.obj X).obj
• CategoryTheory.PreGaloisCategory.instContinuousInvAutFunctorFintypeCat 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : ContinuousInv (CategoryTheory.Aut F)
• CategoryTheory.PreGaloisCategory.instContinuousMulAutFunctorFintypeCat 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : ContinuousMul (CategoryTheory.Aut F)
• CategoryTheory.PreGaloisCategory.autEmbedding 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : CategoryTheory.Aut F →* (X : C) → CategoryTheory.Aut (F.obj X)
• CategoryTheory.PreGaloisCategory.continuousSMul_aut_fiber 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) : ContinuousSMul (CategoryTheory.Aut F) (F.obj X).obj
• CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : (nhds 1).HasBasis (fun x => True) fun X => ↑(MulAction.stabilizer (CategoryTheory.Aut F) X.pt)
• CategoryTheory.PreGaloisCategory.autEquivAutWhiskerRight 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {G : CategoryTheory.Functor FintypeCat FintypeCat} (h : G.FullyFaithful) : CategoryTheory.Aut F ≃ₜ* CategoryTheory.Aut (F.comp G)
• CategoryTheory.PreGaloisCategory.exists_set_ker_evaluation_subset_of_isOpen 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {H : Set (CategoryTheory.Aut F)} (h1 : 1 ∈ H) (h : IsOpen H) : ∃ I x, (∀ X ∈ I, CategoryTheory.PreGaloisCategory.IsConnected X) ∧ ∀ (σ : CategoryTheory.Aut F), (∀ (X : ↑I), σ.hom.app ↑X = CategoryTheory.CategoryStruct.id (F.obj ↑X)) → σ ∈ H
• CategoryTheory.PreGaloisCategory.autEmbedding_injective 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : Function.Injective ⇑(CategoryTheory.PreGaloisCategory.autEmbedding F)
• CategoryTheory.PreGaloisCategory.autEmbedding_apply 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (σ : CategoryTheory.Aut F) (X : C) : (CategoryTheory.PreGaloisCategory.autEmbedding F) σ X = CategoryTheory.Iso.app σ X
• CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : Topology.IsClosedEmbedding ⇑(CategoryTheory.PreGaloisCategory.autEmbedding F)
• CategoryTheory.PreGaloisCategory.autEmbedding_range_isClosed 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : IsClosed (Set.range ⇑(CategoryTheory.PreGaloisCategory.autEmbedding F))
• CategoryTheory.PreGaloisCategory.autEmbedding_range 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : Set.range ⇑(CategoryTheory.PreGaloisCategory.autEmbedding F) = ⋂ f, {a | CategoryTheory.CategoryStruct.comp (F.map f.hom) (a f.right).hom = CategoryTheory.CategoryStruct.comp (a f.left).hom (F.map f.hom)}
• CategoryTheory.PreGaloisCategory.continuous_mapAut_whiskeringRight 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : CategoryTheory.Functor FintypeCat FintypeCat) : Continuous ⇑(CategoryTheory.Functor.mapAut F ((CategoryTheory.Functor.whiskeringRight C FintypeCat FintypeCat).obj G))
• CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup 📋 Mathlib.CategoryTheory.Galois.EssSurj
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (V : OpenSubgroup (CategoryTheory.Aut F)) : ∃ X, Nonempty ((CategoryTheory.PreGaloisCategory.functorToAction F).obj X ≅ Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑V)))
• CategoryTheory.PreGaloisCategory.exists_lift_of_continuous 📋 Mathlib.CategoryTheory.Galois.EssSurj
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : Action FintypeCat (CategoryTheory.Aut F)) [TopologicalSpace X.V.obj] [DiscreteTopology X.V.obj] [ContinuousSMul (CategoryTheory.Aut F) X.V.obj] : ∃ A, Nonempty ((CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅ X)
• CategoryTheory.PreGaloisCategory.fiberIsoQuotientStabilizer 📋 Mathlib.CategoryTheory.Galois.EssSurj
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X] (x : (F.obj X).obj) : (CategoryTheory.PreGaloisCategory.functorToAction F).obj X ≅ Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ MulAction.stabilizer (CategoryTheory.Aut F) x))
• CategoryTheory.PreGaloisCategory.functorToContAction 📋 Mathlib.CategoryTheory.Galois.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) : CategoryTheory.Functor C (ContAction FintypeCat (CategoryTheory.Aut F))
• CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatFunObjFiniteAutFunctorFunctorToContAction 📋 Mathlib.CategoryTheory.Galois.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : (CategoryTheory.PreGaloisCategory.functorToContAction F).EssSurj
• CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatFunObjFiniteAutFunctorFunctorToContActionOfFiberFunctor 📋 Mathlib.CategoryTheory.Galois.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.PreGaloisCategory.FiberFunctor F] : (CategoryTheory.PreGaloisCategory.functorToContAction F).EssSurj
• CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatFunObjFiniteAutFunctorFunctorToContAction 📋 Mathlib.CategoryTheory.Galois.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : (CategoryTheory.PreGaloisCategory.functorToContAction F).Faithful
• CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatFunObjFiniteAutFunctorFunctorToContAction 📋 Mathlib.CategoryTheory.Galois.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : (CategoryTheory.PreGaloisCategory.functorToContAction F).Full
• CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatFunObjFiniteAutFunctorFunctorToContAction 📋 Mathlib.CategoryTheory.Galois.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : (CategoryTheory.PreGaloisCategory.functorToContAction F).IsEquivalence
• CategoryTheory.PreGaloisCategory.functorToContAction_obj_obj 📋 Mathlib.CategoryTheory.Galois.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C) : ((CategoryTheory.PreGaloisCategory.functorToContAction F).obj X).obj = (CategoryTheory.PreGaloisCategory.functorToAction F).obj X
• CategoryTheory.PreGaloisCategory.functorToContAction_map 📋 Mathlib.CategoryTheory.Galois.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.PreGaloisCategory.functorToContAction F).map f = CategoryTheory.ObjectProperty.homMk ((CategoryTheory.PreGaloisCategory.functorToAction F).map f)
• CategoryTheory.PreGaloisCategory.instIsFundamentalGroupAutFunctorFintypeCat 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F (CategoryTheory.Aut F)
• CategoryTheory.PreGaloisCategory.toAutHomeo 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] (G : Type u_1) [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] : G ≃ₜ CategoryTheory.Aut F
• CategoryTheory.PreGaloisCategory.toAut 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1) [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] : G →* CategoryTheory.Aut F
• CategoryTheory.PreGaloisCategory.toAutMulEquiv 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] (G : Type u_1) [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] : G ≃* CategoryTheory.Aut F
• CategoryTheory.PreGaloisCategory.toAut_bijective 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] (G : Type u_1) [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] : Function.Bijective ⇑(CategoryTheory.PreGaloisCategory.toAut F G)
• CategoryTheory.PreGaloisCategory.toAut_isHomeomorph 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] (G : Type u_1) [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] : IsHomeomorph ⇑(CategoryTheory.PreGaloisCategory.toAut F G)
• CategoryTheory.PreGaloisCategory.isPretransitive_of_surjective 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1) [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (h : Function.Surjective ⇑(CategoryTheory.PreGaloisCategory.toAut F G)) (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X] : MulAction.IsPretransitive G (F.obj X).obj
• CategoryTheory.PreGaloisCategory.toAut_continuous 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1) [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [IsTopologicalGroup G] [∀ (X : C), ContinuousSMul G (F.obj X).obj] : Continuous ⇑(CategoryTheory.PreGaloisCategory.toAut F G)
• CategoryTheory.PreGaloisCategory.toAut_injective_of_non_trivial 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1) [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] (h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1) : Function.Injective ⇑(CategoryTheory.PreGaloisCategory.toAut F G)
• CategoryTheory.PreGaloisCategory.toAut_surjective_of_isPretransitive 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1) [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [∀ (X : C), ContinuousSMul G (F.obj X).obj] (h : ∀ (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X], MulAction.IsPretransitive G (F.obj X).obj) : Function.Surjective ⇑(CategoryTheory.PreGaloisCategory.toAut F G)
• CategoryTheory.PreGaloisCategory.toAutHomeo_apply 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] {G : Type u_1} [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (g : G) : (CategoryTheory.PreGaloisCategory.toAutHomeo F G) g = (CategoryTheory.PreGaloisCategory.toAut F G) g
• CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1) [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (t : CategoryTheory.Aut F) (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X] [MulAction.IsPretransitive G (F.obj X).obj] : ∃ g, ∀ (x : (F.obj X).obj), g • x = (CategoryTheory.ConcreteCategory.hom (t.hom.app X)) x
• CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois_finite_family 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1) [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (t : CategoryTheory.Aut F) {ι : Type u_2} [Finite ι] (X : ι → C) [∀ (i : ι), CategoryTheory.PreGaloisCategory.IsGalois (X i)] (h : ∀ (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X], MulAction.IsPretransitive G (F.obj X).obj) : ∃ g, ∀ (i : ι) (x : (F.obj (X i)).obj), g • x = (CategoryTheory.ConcreteCategory.hom (t.hom.app (X i))) x
• CategoryTheory.PreGaloisCategory.toAutMulEquiv_isHomeomorph 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] (G : Type u_1) [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] : IsHomeomorph ⇑(CategoryTheory.PreGaloisCategory.toAutMulEquiv F G)
• CategoryTheory.PreGaloisCategory.toAut_hom_app_apply 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {G : Type u_1} [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] (g : G) {X : C} (x : (F.obj X).obj) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.PreGaloisCategory.toAut F G) g).hom.app X)) x = g • x
• CategoryTheory.PreGaloisCategory.toAutMulEquiv_apply 📋 Mathlib.CategoryTheory.Galois.IsFundamentalgroup
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] {G : Type u_1} [Group G] [(X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (g : G) : (CategoryTheory.PreGaloisCategory.toAutMulEquiv F G) g = (CategoryTheory.PreGaloisCategory.toAut F G) g
• TannakaDuality.FiniteGroup.algHomOfRightFDRepComp 📋 Mathlib.RepresentationTheory.Tannaka
  {k G : Type u} [CommRing k] [Group G] [Finite G] (η : CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G)) : (G → k) →ₐ[k] G → k
• TannakaDuality.FiniteGroup.equivHom 📋 Mathlib.RepresentationTheory.Tannaka
  (k G : Type u) [CommRing k] [Group G] : G →* CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G)
• TannakaDuality.FiniteGroup.equiv 📋 Mathlib.RepresentationTheory.Tannaka
  (k G : Type u) [CommRing k] [Group G] [Finite G] [IsDomain k] : G ≃* CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G)
• TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp 📋 Mathlib.RepresentationTheory.Tannaka
  {k G : Type u} [CommRing k] [Group G] [Finite G] (η : CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G)) (f g : G → k) : have α := ModuleCat.Hom.hom (η.hom.hom.app TannakaDuality.FiniteGroup.rightFDRep).hom; α (f * g) = α f * α g
• TannakaDuality.FiniteGroup.toRightFDRepComp_injective 📋 Mathlib.RepresentationTheory.Tannaka
  {k G : Type u} [CommRing k] [Group G] [Finite G] {η₁ η₂ : CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G)} (h : η₁.hom.hom.app TannakaDuality.FiniteGroup.rightFDRep = η₂.hom.hom.app TannakaDuality.FiniteGroup.rightFDRep) : η₁ = η₂
• TannakaDuality.FiniteGroup.equivHom_injective 📋 Mathlib.RepresentationTheory.Tannaka
  {k G : Type u} [CommRing k] [Group G] [Finite G] [Nontrivial k] : Function.Injective ⇑(TannakaDuality.FiniteGroup.equivHom k G)
• TannakaDuality.FiniteGroup.equivHom_surjective 📋 Mathlib.RepresentationTheory.Tannaka
  {k G : Type u} [CommRing k] [Group G] [Finite G] [IsDomain k] : Function.Surjective ⇑(TannakaDuality.FiniteGroup.equivHom k G)
• TannakaDuality.FiniteGroup.equivHom_apply 📋 Mathlib.RepresentationTheory.Tannaka
  (k G : Type u) [CommRing k] [Group G] (g : G) : (TannakaDuality.FiniteGroup.equivHom k G) g = CategoryTheory.LaxMonoidalFunctor.isoOfComponents (TannakaDuality.FiniteGroup.equivApp g) ⋯ ⋯ ⋯
• TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular 📋 Mathlib.RepresentationTheory.Tannaka
  {k G : Type u} [CommRing k] [Group G] [Finite G] [IsDomain k] (η : CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G)) : ∃ s, ModuleCat.Hom.hom (η.hom.hom.app TannakaDuality.FiniteGroup.rightFDRep).hom = TannakaDuality.FiniteGroup.rightRegular s

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c