Categories

📁 Source: FLT/Deformations/Categories.lean

Statistics

Metric	Count
Definitions `toContinuousAlgEquiv`, `IsLocalProartinianAlgebra`, `ProartinianCat`, `hom`, `algebra`, `carrier`, `commRing`, `fromSelf`, `instCategory`, `instCoeSortType`, `instFieldCarrierResidueField`, `instUniqueHomResidueField`, `instUniqueHomSelf`, `isInitialSelf`, `isTerminalResidueField`, `of`, `ofEquiv`, `ofHom`, `residueField`, `self`, `toResidueField`, `topologicalSpace`	22
Theorems `toIsLocalHom`, `toIsLocalRing`, `toIsProartinian`, `toIsResidueAlgebra`, `toIsTopologicalRing`, `ext`, `ext_iff`, `coe_of`, `comp_apply`, `hom_comp`, `hom_ext`, `hom_ext_iff`, `hom_id`, `hom_ofHom`, `id_apply`, `instDiscreteTopologyCarrierResidueField`, `instIsAdicTopologyCarrierSelf`, `instIsLocalHomCarrierContinuousAlgHomHom`, `isLocalProartinianAlgebra`, `ker_toResidueField`, `ofEquiv_hom_hom`, `ofEquiv_inv_hom`, `ofHom_comp`, `ofHom_hom`, `ofHom_id`, `toResidueField_surjective`, `to_residueField_apply`	27
Total	49

CategoryTheory.Iso

Definitions

Name	Category	Theorems
`toContinuousAlgEquiv` 📖	CompOp	—

Deformation

Definitions

Name	Category	Theorems
`IsLocalProartinianAlgebra` 📖	CompData	1 math math: `ProartinianCat.isLocalProartinianAlgebra`
`ProartinianCat` 📖	CompData	11 math math: `isCorepresentable_deformationFunctor`, `ProartinianCat.hom_id`, `ProartinianCat.hom_comp`, `ProartinianCat.id_apply`, `ProartinianCat.ofHom_id`, `ProartinianCat.ofHom_comp`, `repnFunctor_map`, `ProartinianCat.ofEquiv_inv_hom`, `ProartinianCat.ofEquiv_hom_hom`, `ProartinianCat.comp_apply`, `toFramedGaloisRep_map`

Deformation.IsLocalProartinianAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsLocalHom` 📖	—	—	—	—	—
`toIsLocalRing` 📖	—	—	—	—	—
`toIsProartinian` 📖	mathematical	—	`IsProartinian` `toIsTopologicalRing`	—	—
`toIsResidueAlgebra` 📖	mathematical	—	`IsResidueAlgebra` `toIsLocalRing`	—	—
`toIsTopologicalRing` 📖	—	—	—	—	—

Deformation.ProartinianCat

Definitions

Name	Category	Theorems
`algebra` 📖	CompOp	13 math math: `instIsAdicTopologyCarrierSelf`, `hom_id`, `hom_comp`, `id_apply`, `toResidueField_surjective`, `Deformation.repnFunctor_map`, `to_residueField_apply`, `comp_apply`, `isLocalProartinianAlgebra`, `Deformation.toFramedGaloisRep_map`, `ofHom_hom`, `ker_toResidueField`, `instIsLocalHomCarrierContinuousAlgHomHom`
`carrier` 📖	CompOp	15 math math: `instIsAdicTopologyCarrierSelf`, `hom_id`, `hom_comp`, `id_apply`, `toResidueField_surjective`, `Deformation.repnFunctor_map`, `coe_of`, `to_residueField_apply`, `instDiscreteTopologyCarrierResidueField`, `comp_apply`, `isLocalProartinianAlgebra`, `Deformation.toFramedGaloisRep_map`, `ofHom_hom`, `ker_toResidueField`, `instIsLocalHomCarrierContinuousAlgHomHom`
`commRing` 📖	CompOp	13 math math: `instIsAdicTopologyCarrierSelf`, `hom_id`, `hom_comp`, `id_apply`, `toResidueField_surjective`, `Deformation.repnFunctor_map`, `to_residueField_apply`, `comp_apply`, `isLocalProartinianAlgebra`, `Deformation.toFramedGaloisRep_map`, `ofHom_hom`, `ker_toResidueField`, `instIsLocalHomCarrierContinuousAlgHomHom`
`fromSelf` 📖	CompOp	—
`instCategory` 📖	CompOp	11 math math: `Deformation.isCorepresentable_deformationFunctor`, `hom_id`, `hom_comp`, `id_apply`, `ofHom_id`, `ofHom_comp`, `Deformation.repnFunctor_map`, `ofEquiv_inv_hom`, `ofEquiv_hom_hom`, `comp_apply`, `Deformation.toFramedGaloisRep_map`
`instCoeSortType` 📖	CompOp	—
`instFieldCarrierResidueField` 📖	CompOp	—
`instUniqueHomResidueField` 📖	CompOp	—
`instUniqueHomSelf` 📖	CompOp	—
`isInitialSelf` 📖	CompOp	—
`isTerminalResidueField` 📖	CompOp	—
`of` 📖	CompOp	6 math math: `ofHom_id`, `ofHom_comp`, `coe_of`, `ofEquiv_inv_hom`, `ofEquiv_hom_hom`, `hom_ofHom`
`ofEquiv` 📖	CompOp	2 math math: `ofEquiv_inv_hom`, `ofEquiv_hom_hom`
`ofHom` 📖	CompOp	4 math math: `ofHom_id`, `ofHom_comp`, `hom_ofHom`, `ofHom_hom`
`residueField` 📖	CompOp	4 math math: `toResidueField_surjective`, `to_residueField_apply`, `instDiscreteTopologyCarrierResidueField`, `ker_toResidueField`
`self` 📖	CompOp	1 math math: `instIsAdicTopologyCarrierSelf`
`toResidueField` 📖	CompOp	2 math math: `toResidueField_surjective`, `ker_toResidueField`
`topologicalSpace` 📖	CompOp	14 math math: `instIsAdicTopologyCarrierSelf`, `hom_id`, `hom_comp`, `id_apply`, `toResidueField_surjective`, `Deformation.repnFunctor_map`, `to_residueField_apply`, `instDiscreteTopologyCarrierResidueField`, `comp_apply`, `isLocalProartinianAlgebra`, `Deformation.toFramedGaloisRep_map`, `ofHom_hom`, `ker_toResidueField`, `instIsLocalHomCarrierContinuousAlgHomHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_of` 📖	mathematical	—	`carrier` `of`	—	—
`comp_apply` 📖	mathematical	—	`carrier` `commRing` `topologicalSpace` `algebra` `Hom.hom` `Deformation.ProartinianCat` `instCategory`	—	—
`hom_comp` 📖	mathematical	—	`Hom.hom` `Deformation.ProartinianCat` `instCategory` `carrier` `commRing` `topologicalSpace` `algebra`	—	—
`hom_ext` 📖	—	`Hom.hom`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.hom`	—	`hom_ext`
`hom_id` 📖	mathematical	—	`Hom.hom` `Deformation.ProartinianCat` `instCategory` `carrier` `commRing` `topologicalSpace` `algebra`	—	—
`hom_ofHom` 📖	mathematical	—	`Hom.hom` `of` `ofHom`	—	—
`id_apply` 📖	mathematical	—	`carrier` `commRing` `topologicalSpace` `algebra` `Hom.hom` `Deformation.ProartinianCat` `instCategory`	—	—
`instDiscreteTopologyCarrierResidueField` 📖	mathematical	—	`carrier` `residueField` `topologicalSpace`	—	—
`instIsAdicTopologyCarrierSelf` 📖	mathematical	—	`IsLocalRing.IsAdicTopology` `carrier` `self` `commRing` `Deformation.IsLocalProartinianAlgebra.toIsLocalRing` `topologicalSpace` `algebra` `isLocalProartinianAlgebra` `Deformation.IsLocalProartinianAlgebra.toIsTopologicalRing`	—	`Deformation.IsLocalProartinianAlgebra.toIsLocalRing` `isLocalProartinianAlgebra` `Deformation.IsLocalProartinianAlgebra.toIsTopologicalRing`
`instIsLocalHomCarrierContinuousAlgHomHom` 📖	mathematical	—	`carrier` `commRing` `topologicalSpace` `algebra` `Hom.hom`	—	`isLocalHom_of_isContinuous_of_isProartinian` `Deformation.IsLocalProartinianAlgebra.toIsTopologicalRing` `isLocalProartinianAlgebra` `Deformation.IsLocalProartinianAlgebra.toIsLocalRing` `Deformation.IsLocalProartinianAlgebra.toIsProartinian`
`isLocalProartinianAlgebra` 📖	mathematical	—	`Deformation.IsLocalProartinianAlgebra` `carrier` `commRing` `topologicalSpace` `algebra`	—	—
`ker_toResidueField` 📖	mathematical	—	`carrier` `residueField` `commRing` `topologicalSpace` `algebra` `Hom.hom` `toResidueField` `Deformation.IsLocalProartinianAlgebra.toIsLocalRing` `isLocalProartinianAlgebra`	—	`Deformation.IsLocalProartinianAlgebra.toIsLocalRing` `isLocalProartinianAlgebra` `Deformation.IsLocalProartinianAlgebra.toIsResidueAlgebra` `Deformation.IsLocalProartinianAlgebra.toIsLocalHom`
`ofEquiv_hom_hom` 📖	mathematical	—	`Hom.hom` `of` `Deformation.ProartinianCat` `instCategory` `ofEquiv`	—	—
`ofEquiv_inv_hom` 📖	mathematical	—	`Hom.hom` `of` `Deformation.ProartinianCat` `instCategory` `ofEquiv`	—	—
`ofHom_comp` 📖	mathematical	—	`ofHom` `Deformation.ProartinianCat` `instCategory` `of`	—	—
`ofHom_hom` 📖	mathematical	—	`ofHom` `carrier` `commRing` `algebra` `topologicalSpace` `isLocalProartinianAlgebra` `Hom.hom`	—	`isLocalProartinianAlgebra`
`ofHom_id` 📖	mathematical	—	`ofHom` `Deformation.ProartinianCat` `instCategory` `of`	—	—
`toResidueField_surjective` 📖	mathematical	—	`carrier` `residueField` `commRing` `topologicalSpace` `algebra` `Hom.hom` `toResidueField`	—	`Deformation.IsLocalProartinianAlgebra.toIsLocalRing` `isLocalProartinianAlgebra` `Deformation.IsLocalProartinianAlgebra.toIsResidueAlgebra` `Deformation.IsLocalProartinianAlgebra.toIsLocalHom`
`to_residueField_apply` 📖	mathematical	—	`carrier` `commRing` `topologicalSpace` `residueField` `algebra` `Hom.hom` `IsResidueAlgebra.preimage` `Deformation.IsLocalProartinianAlgebra.toIsLocalRing` `isLocalProartinianAlgebra` `Deformation.IsLocalProartinianAlgebra.toIsResidueAlgebra`	—	`Deformation.IsLocalProartinianAlgebra.toIsLocalRing` `isLocalProartinianAlgebra` `Deformation.IsLocalProartinianAlgebra.toIsResidueAlgebra` `instIsLocalHomRingHomOfContinuousAlgHom_fLT_1` `instIsLocalHomCarrierContinuousAlgHomHom` `IsResidueAlgebra.preimage_spec`

Deformation.ProartinianCat.Hom

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	16 math math: `Deformation.ProartinianCat.hom_id`, `Deformation.ProartinianCat.hom_comp`, `Deformation.ProartinianCat.id_apply`, `Deformation.ProartinianCat.toResidueField_surjective`, `Deformation.ProartinianCat.hom_ext_iff`, `Deformation.repnFunctor_map`, `Deformation.ProartinianCat.ofEquiv_inv_hom`, `Deformation.ProartinianCat.ofEquiv_hom_hom`, `Deformation.ProartinianCat.to_residueField_apply`, `Deformation.ProartinianCat.hom_ofHom`, `Deformation.ProartinianCat.comp_apply`, `Deformation.toFramedGaloisRep_map`, `ext_iff`, `Deformation.ProartinianCat.ofHom_hom`, `Deformation.ProartinianCat.ker_toResidueField`, `Deformation.ProartinianCat.instIsLocalHomCarrierContinuousAlgHomHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`hom`	—	—	—
`ext_iff` 📖	mathematical	—	`hom`	—	`ext`

---

← Back to Index