feat(CategoryTheory): ContAction FintypeCat G is a Galois category

[joelriou]

---

• depends on: feat(CategoryTheory): properties of objects that are closed under finite limits #42396
• depends on: feat(CategoryTheory/Galois): full subcategories #42320

[github-actions]

PR summary 85d72a2743

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.ObjectProperty.FiniteLimits (new file)	910
Mathlib.CategoryTheory.Galois.FullSubcategory (new file)	1055
Mathlib.CategoryTheory.Galois.ContAction (new file)	1461

---

Declarations diff (regex)

+ Action.isContinuous
+ IsClosedUnderFiniteColimits
+ IsClosedUnderFiniteLimits
+ IsGaloisSubcategory
+ exists_openSubgroup_of_isContinuous_of_finite
+ iInfOfFinite
+ iInfOfFinite_le
+ instance (J : Type*) [Category* J] [HasColimitsOfShape J V] (S : Set G) :
+ instance (J : Type*) [Category* J] [HasLimitsOfShape J V] (S : Set G) :
+ instance (P : ObjectProperty C) [P.IsClosedUnderFiniteColimits]
+ instance (S : Set G) : (trivialOnSet FintypeCat.{w} S).IsGaloisSubcategory
+ instance (S : Set G) [HasPullbacks V] :
+ instance : (isContinuous FintypeCat.{w} G).IsClosedUnderFiniteColimits
+ instance : (isContinuous FintypeCat.{w} G).IsClosedUnderFiniteLimits
+ instance : (isContinuous FintypeCat.{w} G).IsClosedUnderSubobjects := by
+ instance : (isContinuous FintypeCat.{w} G).IsGaloisSubcategory
+ instance : HasFiniteColimits P.FullSubcategory
+ instance : HasFiniteLimits P.FullSubcategory
+ instance : P.IsClosedUnderFiniteCoproducts
+ instance : P.IsClosedUnderFiniteProducts
+ instance : PreservesFiniteColimits P.ι
+ instance : PreservesFiniteLimits P.ι
+ instance [GaloisCategory C] (P : ObjectProperty C) [P.IsGaloisSubcategory] :
+ instance [HasFiniteColimits V] (S : Set G) :
+ instance [HasFiniteLimits V] (S : Set G) :
+ instance {ι : Type*} (P : ι → ObjectProperty C) [∀ i, (P i).IsClosedUnderQuotients] :
+ instance {ι : Type*} (P : ι → ObjectProperty C) [∀ i, (P i).IsClosedUnderSubobjects] :
+ isContinuous_eq_iSup
+ trivialOnSet
+ trivialOnSet_antitone
+ trivialOnSet_le_isContinuous
++ instance [PreGaloisCategory C] [MonoCoprod C]

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 85d72a2).

• +55 new declarations
• −0 removed declarations

+Action.exists_openSubgroup_of_isContinuous_of_finite
+Action.instIsClosedUnderColimitsOfShapeTrivialOnSetOfHasColimitsOfShape
+Action.instIsClosedUnderFiniteColimitsFintypeCatIsContinuousFunObjFinite
+Action.instIsClosedUnderFiniteColimitsTrivialOnSetOfHasFiniteColimits
+Action.instIsClosedUnderFiniteLimitsFintypeCatIsContinuousFunObjFinite
+Action.instIsClosedUnderFiniteLimitsTrivialOnSetOfHasFiniteLimits
+Action.instIsClosedUnderLimitsOfShapeTrivialOnSetOfHasLimitsOfShape
+Action.instIsClosedUnderSubobjectsFintypeCatIsContinuousFunObjFinite
+Action.instIsClosedUnderSubobjectsTrivialOnSetOfHasPullbacks
+Action.instIsGaloisSubcategoryFintypeCatIsContinuousFunObjFinite
+Action.instIsGaloisSubcategoryFintypeCatTrivialOnSet
+Action.isContinuous
+Action.isContinuous_eq_iSup
+Action.trivialOnSet
+Action.trivialOnSet_antitone
+Action.trivialOnSet_le_isContinuous
+CategoryTheory.GaloisCategory.instFullSubcategoryOfIsGaloisSubcategory
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits.casesOn
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits.instHasFiniteColimitsFullSubcategory
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits.instIsClosedUnderFiniteCoproducts
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits.instPreservesFiniteColimitsFullSubcategoryι
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits.isClosedUnderColimitsOfShape
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits.mk
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits.rec
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits.recOn
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits.casesOn
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits.instHasFiniteLimitsFullSubcategory
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits.instIsClosedUnderFiniteProducts
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits.instPreservesFiniteLimitsFullSubcategoryι
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits.isClosedUnderLimitsOfShape
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits.mk
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits.rec
+CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits.recOn
+CategoryTheory.ObjectProperty.IsGaloisSubcategory
+CategoryTheory.ObjectProperty.IsGaloisSubcategory.casesOn
+CategoryTheory.ObjectProperty.IsGaloisSubcategory.isClosedUnderColimitsOfShape_discrete
+CategoryTheory.ObjectProperty.IsGaloisSubcategory.isClosedUnderColimitsOfShape_singleObj
+CategoryTheory.ObjectProperty.IsGaloisSubcategory.isClosedUnderLimitsOfShape_discrete_pEmpty
+CategoryTheory.ObjectProperty.IsGaloisSubcategory.isClosedUnderLimitsOfShape_walkingCospan
+CategoryTheory.ObjectProperty.IsGaloisSubcategory.isClosedUnderSubobjects
+CategoryTheory.ObjectProperty.IsGaloisSubcategory.mk
+CategoryTheory.ObjectProperty.IsGaloisSubcategory.preservesEpimorphisms
+CategoryTheory.ObjectProperty.IsGaloisSubcategory.rec
+CategoryTheory.ObjectProperty.IsGaloisSubcategory.recOn
+CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeSingleObjOfIsClosedUnderFiniteColimitsOfFinite
+CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsISup
+CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsISup
+CategoryTheory.PreGaloisCategory.instFiberFunctorFullSubcategoryCompFintypeCatι
+CategoryTheory.PreGaloisCategory.instFullSubcategoryOfMonoCoprodOfIsGaloisSubcategory
+OpenAddSubgroup.iInfOfFinite
+OpenAddSubgroup.iInfOfFinite_le
+OpenSubgroup.iInfOfFinite
+OpenSubgroup.iInfOfFinite_le

---

Increase in strong tech debt: (relative, absolute) = (1.23, 0.00)

Current number	Change	Type (strong)
4367	1	backward.defeqAttrib.useBackward
6994	2	backward.isDefEq.respectTransparency
3995	1	backward.isDefEq.respectTransparency.types

Increase in weak tech debt: (relative, absolute) = (3.00, 0.00)

Current number	Change	Type (weak)
5050	3	exposed public sections

Current commit 85d72a2743
Reference commit 1f8806b67d

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(CategoryTheory): properties of objects that are closed under finite limits #42396
• feat(CategoryTheory/Galois): full subcategories #42320
  By Dependent Issues (🤖). Happy coding!