Documentation Verification Report

Etale

📁 Source: FLT/Deformations/RepresentationTheory/Etale.lean

Statistics

Metric	Count
Definitions `evalMulActionHom`, `quotientEquivFixedFieldEmb`, `etaleSubalgebraEquiv`, `homEquivProdFixedPoints`, `sigmaRangeQuotientStabilizer`, `compLeftAlgHom`, `evalAlgHom`, `toFunAlgHom`, `single`, `algHomEquivOfIsDomain`, `ringHomEquivOfIsDomain`, `piIndex`, `projPiIndex`, `instAlgebraMulActionHomIdOfSMulCommClass_fLT`, `instMonoidAlgHom_fLT`, `instMulActionAlgHomOfSMulCommClass_fLT`, `instMulDistribMulActionAlgEquivAlgHom_fLT`, `instMulDistribMulActionAlgEquivAlgHom_fLT_1`, `instMulDistribMulActionAlgEquivAlgHom_fLT_2`, `instSMulMulActionHomIdOfSMulCommClass_fLT`	20
Theorems `evalAlgHom_bijective`, `evalMulActionHom_bijective`, `evalMulActionHom_bijective_of_isSepClosed`, `homEquivProdFixedPoints_apply_coe`, `homEquivProdFixedPoints_symm_apply_apply`, `mk_smul`, `sigmaRangeQuotientStabilizer_apply`, `sigmaRangeQuotientStabilizer_symm_apply_fst_coe`, `sigmaRangeQuotientStabilizer_symm_apply_snd`, `evalAlgHom_apply`, `single_apply`, `algHomEquivOfIsDomain_apply_fst`, `algHomEquivOfIsDomain_apply_snd_apply`, `algHomEquivOfIsDomain_symm_apply_apply`, `ringHomEquivOfIsDomain_apply_fst`, `ringHomEquivOfIsDomain_apply_snd`, `ringHomEquivOfIsDomain_symm_apply_apply`, `exists_map_single_ne_zero`, `projPiIndex_apply`, `single_piIndex`, `single_piIndex_ne_zero`, `single_piIndex_one`, `toNonUnitalRingHom_apply`, `instContinuousSMulDiscreteAlgEquivAlgHomOfFinite`, `instEtaleMulActionHomAlgEquivIdOfIsGaloisOfFiniteOfContinuousSMulDiscrete`, `instFiniteMulActionHomAlgEquivIdOfIsGaloisOfFiniteOfContinuousSMulDiscrete`, `instFormallyEtaleMulActionHomAlgEquivIdOfIsGaloisOfFinite_fLT`	27
Total	47

AlgHom

Definitions

Name	Category	Theorems
`evalMulActionHom` 📖	CompOp	2 math math: `InfiniteGalois.evalMulActionHom_bijective`, `InfiniteGalois.evalMulActionHom_bijective_of_isSepClosed`

InfiniteGalois

Definitions

Name	Category	Theorems
`quotientEquivFixedFieldEmb` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`evalAlgHom_bijective` 📖	mathematical	—	`instAlgebraMulActionHomIdOfSMulCommClass_fLT` `instMulActionAlgHomOfSMulCommClass_fLT` `MulActionHom.evalAlgHom`	—	`ContinuousSMulDiscrete.isOpen_stabilizer`
`evalMulActionHom_bijective` 📖	mathematical	—	`instMulActionAlgHomOfSMulCommClass_fLT` `instAlgebraMulActionHomIdOfSMulCommClass_fLT` `AlgHom.evalMulActionHom`	—	—
`evalMulActionHom_bijective_of_isSepClosed` 📖	mathematical	—	`instMulActionAlgHomOfSMulCommClass_fLT` `instAlgebraMulActionHomIdOfSMulCommClass_fLT` `AlgHom.evalMulActionHom`	—	`evalMulActionHom_bijective`

MulAction

Definitions

Name	Category	Theorems
`etaleSubalgebraEquiv` 📖	CompOp	—
`homEquivProdFixedPoints` 📖	CompOp	2 math math: `homEquivProdFixedPoints_apply_coe`, `homEquivProdFixedPoints_symm_apply_apply`
`sigmaRangeQuotientStabilizer` 📖	CompOp	3 math math: `sigmaRangeQuotientStabilizer_symm_apply_fst_coe`, `sigmaRangeQuotientStabilizer_apply`, `sigmaRangeQuotientStabilizer_symm_apply_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homEquivProdFixedPoints_apply_coe` 📖	mathematical	—	`homEquivProdFixedPoints`	—	—
`homEquivProdFixedPoints_symm_apply_apply` 📖	mathematical	—	`homEquivProdFixedPoints`	—	—
`sigmaRangeQuotientStabilizer_apply` 📖	mathematical	—	`sigmaRangeQuotientStabilizer`	—	—
`sigmaRangeQuotientStabilizer_symm_apply_fst_coe` 📖	mathematical	—	`sigmaRangeQuotientStabilizer`	—	—
`sigmaRangeQuotientStabilizer_symm_apply_snd` 📖	mathematical	—	`sigmaRangeQuotientStabilizer`	—	—

MulAction.orbitRel.Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_smul` 📖	—	—	—	—	—

MulActionHom

Definitions

Name	Category	Theorems
`compLeftAlgHom` 📖	CompOp	—
`evalAlgHom` 📖	CompOp	2 math math: `InfiniteGalois.evalAlgHom_bijective`, `evalAlgHom_apply`
`toFunAlgHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`evalAlgHom_apply` 📖	mathematical	—	`instAlgebraMulActionHomIdOfSMulCommClass_fLT` `instMulActionAlgHomOfSMulCommClass_fLT` `evalAlgHom`	—	—

NonUnitalRingHom

Definitions

Name	Category	Theorems
`single` 📖	CompOp	1 math math: `single_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`single_apply` 📖	mathematical	—	`single`	—	—

Pi

Definitions

Name	Category	Theorems
`algHomEquivOfIsDomain` 📖	CompOp	3 math math: `algHomEquivOfIsDomain_symm_apply_apply`, `algHomEquivOfIsDomain_apply_snd_apply`, `algHomEquivOfIsDomain_apply_fst`
`ringHomEquivOfIsDomain` 📖	CompOp	3 math math: `ringHomEquivOfIsDomain_symm_apply_apply`, `ringHomEquivOfIsDomain_apply_snd`, `ringHomEquivOfIsDomain_apply_fst`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algHomEquivOfIsDomain_apply_fst` 📖	mathematical	—	`algHomEquivOfIsDomain` `RingHom.piIndex`	—	—
`algHomEquivOfIsDomain_apply_snd_apply` 📖	mathematical	—	`RingHom.piIndex` `algHomEquivOfIsDomain`	—	—
`algHomEquivOfIsDomain_symm_apply_apply` 📖	mathematical	—	`algHomEquivOfIsDomain`	—	—
`ringHomEquivOfIsDomain_apply_fst` 📖	mathematical	—	`ringHomEquivOfIsDomain` `RingHom.piIndex`	—	—
`ringHomEquivOfIsDomain_apply_snd` 📖	mathematical	—	`ringHomEquivOfIsDomain` `RingHom.projPiIndex`	—	—
`ringHomEquivOfIsDomain_symm_apply_apply` 📖	mathematical	—	`ringHomEquivOfIsDomain`	—	—

RingHom

Definitions

Name	Category	Theorems
`piIndex` 📖	CompOp	6 math math: `single_piIndex_one`, `projPiIndex_apply`, `single_piIndex`, `Pi.algHomEquivOfIsDomain_apply_snd_apply`, `Pi.ringHomEquivOfIsDomain_apply_fst`, `Pi.algHomEquivOfIsDomain_apply_fst`
`projPiIndex` 📖	CompOp	2 math math: `Pi.ringHomEquivOfIsDomain_apply_snd`, `projPiIndex_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_map_single_ne_zero` 📖	—	—	—	—	—
`projPiIndex_apply` 📖	mathematical	—	`piIndex` `projPiIndex`	—	—
`single_piIndex` 📖	mathematical	—	`piIndex`	—	`single_piIndex_one`
`single_piIndex_ne_zero` 📖	—	—	—	—	`exists_map_single_ne_zero`
`single_piIndex_one` 📖	mathematical	—	`piIndex`	—	`single_piIndex_ne_zero`
`toNonUnitalRingHom_apply` 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
`instAlgebraMulActionHomIdOfSMulCommClass_fLT` 📖	CompOp	6 math math: `InfiniteGalois.evalMulActionHom_bijective`, `InfiniteGalois.evalAlgHom_bijective`, `instEtaleMulActionHomAlgEquivIdOfIsGaloisOfFiniteOfContinuousSMulDiscrete`, `InfiniteGalois.evalMulActionHom_bijective_of_isSepClosed`, `MulActionHom.evalAlgHom_apply`, `instFormallyEtaleMulActionHomAlgEquivIdOfIsGaloisOfFinite_fLT`
`instMonoidAlgHom_fLT` 📖	CompOp	—
`instMulActionAlgHomOfSMulCommClass_fLT` 📖	CompOp	5 math math: `InfiniteGalois.evalMulActionHom_bijective`, `InfiniteGalois.evalAlgHom_bijective`, `InfiniteGalois.evalMulActionHom_bijective_of_isSepClosed`, `MulActionHom.evalAlgHom_apply`, `instContinuousSMulDiscreteAlgEquivAlgHomOfFinite`
`instMulDistribMulActionAlgEquivAlgHom_fLT` 📖	CompOp	—
`instMulDistribMulActionAlgEquivAlgHom_fLT_1` 📖	CompOp	—
`instMulDistribMulActionAlgEquivAlgHom_fLT_2` 📖	CompOp	—
`instSMulMulActionHomIdOfSMulCommClass_fLT` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instContinuousSMulDiscreteAlgEquivAlgHomOfFinite` 📖	mathematical	—	`ContinuousSMulDiscrete` `instMulActionAlgHomOfSMulCommClass_fLT`	—	`continuousSMulDiscrete_iff_isOpen_stabilizer`
`instEtaleMulActionHomAlgEquivIdOfIsGaloisOfFiniteOfContinuousSMulDiscrete` 📖	mathematical	—	`instAlgebraMulActionHomIdOfSMulCommClass_fLT`	—	`instFormallyEtaleMulActionHomAlgEquivIdOfIsGaloisOfFinite_fLT` `instFiniteMulActionHomAlgEquivIdOfIsGaloisOfFiniteOfContinuousSMulDiscrete`
`instFiniteMulActionHomAlgEquivIdOfIsGaloisOfFiniteOfContinuousSMulDiscrete` 📖	—	—	—	—	`ContinuousSMulDiscrete.isOpen_stabilizer`
`instFormallyEtaleMulActionHomAlgEquivIdOfIsGaloisOfFinite_fLT` 📖	mathematical	—	`instAlgebraMulActionHomIdOfSMulCommClass_fLT`	—	—

---

← Back to Index