2. The candidate as a profinite group🔗

Lemma2.1

Group: The candidate as a profinite group (2)

Hover another entry in this group to preview it.

Preview

Lemma 2.2

Loading preview

Hover a group entry to preview it.

✓L∃∀Nused by 1

Lemma 2.1 of the paper (Finite subdirect closure).

If F\twoheadrightarrow G_i are finitely many admissible quotients and Y is the image of F in \prod_iG_i, then F\twoheadrightarrow Y is admissible and its kernel is the intersection of the given kernels.

Lean code for Lemma2.1●2 theorems

theoremdefined in Q2Presentation/Candidate/AdmissibleCat.lean

complete

theorem Q2Presentation.admissibleIndex_isCofiltered :
  CategoryTheory.IsCofilteredCategoryTheory.IsCofiltered.{v, u} (C : Type u) [CategoryTheory.Category.{v, u} C] : PropA category `IsCofiltered` if
1. for every pair of objects there exists another object "to the left",
2. for every pair of parallel morphisms there exists a morphism to the left so the compositions
   are equal, and
3. there exists some object.  Q2Presentation.AdmissibleIndexQ2Presentation.AdmissibleIndex : TypeA concrete admissible marked finite group with carrier the skeleton `Fin n`.

Fixing the carrier to `Fin n` (rather than an arbitrary finite type) keeps the
index category used to build `Γ_A` small.  The fields are the size `n`, a proof
that the carrier is nonempty (`0 < n`), the group structure `groupFin`, the
marking `q`, and a proof that `q` is `Admissible` for that structure.

theorem Q2Presentation.admissibleIndex_isCofiltered :
  CategoryTheory.IsCofilteredCategoryTheory.IsCofiltered.{v, u} (C : Type u) [CategoryTheory.Category.{v, u} C] : PropA category `IsCofiltered` if
1. for every pair of objects there exists another object "to the left",
2. for every pair of parallel morphisms there exists a morphism to the left so the compositions
   are equal, and
3. there exists some object. 
    Q2Presentation.AdmissibleIndexQ2Presentation.AdmissibleIndex : TypeA concrete admissible marked finite group with carrier the skeleton `Fin n`.

Fixing the carrier to `Fin n` (rather than an arbitrary finite type) keeps the
index category used to build `Γ_A` small.  The fields are the size `n`, a proof
that the carrier is nonempty (`0 < n`), the group structure `groupFin`, the
marking `q`, and a proof that `q` is `Admissible` for that structure.

**The admissible index category is cofiltered** (the Lean form of manuscript
Lemma 2.1 + Lemma 2.2).  Binary cones are the subdirect objects `subdirectObj`;
the `cone_maps` (equalizer) half is automatic because any two parallel arrows are
equal (`admissibleHom_ext`); nonemptiness is the trivial admissible quotient.

theoremdefined in Q2Presentation/Foundation/Subdirect.lean

complete

theorem Q2Presentation.admissible_subdirect.{u_1, u_2} {ιType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 ιType u_1]
  {Gι → Type u_2 : ιType u_1 → Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [(iι : ιType u_1) → GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 (Gι → Type u_2 iι)] [∀ (iι : ιType u_1), FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 (Gι → Type u_2 iι)]
  (q(i : ι) → Q2Presentation.Marking (G i) : (iι : ιType u_1) → Q2Presentation.MarkingQ2Presentation.Marking.{u_1} (G : Type u_1) [Group G] : Type u_1A marking assigns a group element to each of the four generators.  (Gι → Type u_2 iι))
  (h∀ (i : ι), Q2Presentation.Admissible (q i) : ∀ (iι : ιType u_1), Q2Presentation.AdmissibleQ2Presentation.Admissible.{u_1} {G : Type u_1} [Group G] [Finite G] (q : Q2Presentation.Marking G) : PropA marking is **admissible** when it generates, satisfies the tame and wild
relators, and sends `x₀, x₁` into the 2-core.  (q(i : ι) → Q2Presentation.Marking (G i) iι)) :
  Q2Presentation.AdmissibleQ2Presentation.Admissible.{u_1} {G : Type u_1} [Group G] [Finite G] (q : Q2Presentation.Marking G) : PropA marking is **admissible** when it generates, satisfies the tame and wild
relators, and sends `x₀, x₁` into the 2-core.  (Q2Presentation.diagonalSubdirectMarkingQ2Presentation.diagonalSubdirectMarking.{u_1, u_2} {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)]
  (q : (i : ι) → Q2Presentation.Marking (G i)) : Q2Presentation.Marking ↥(Q2Presentation.subdirectSubgroup q)The diagonal marking, corestricted to the subdirect subgroup it generates.  q(i : ι) → Q2Presentation.Marking (G i))

theorem Q2Presentation.admissible_subdirect.{u_1,
    u_2}
  {ιType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 ιType u_1]
  {Gι → Type u_2 : ιType u_1 → Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [(iι : ιType u_1) → GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 (Gι → Type u_2 iι)]
  [∀ (iι : ιType u_1), FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 (Gι → Type u_2 iι)]
  (q(i : ι) → Q2Presentation.Marking (G i) :
    (iι : ιType u_1) →
      Q2Presentation.MarkingQ2Presentation.Marking.{u_1} (G : Type u_1) [Group G] : Type u_1A marking assigns a group element to each of the four generators.  (Gι → Type u_2 iι))
  (h∀ (i : ι), Q2Presentation.Admissible (q i) :
    ∀ (iι : ιType u_1),
      Q2Presentation.AdmissibleQ2Presentation.Admissible.{u_1} {G : Type u_1} [Group G] [Finite G] (q : Q2Presentation.Marking G) : PropA marking is **admissible** when it generates, satisfies the tame and wild
relators, and sends `x₀, x₁` into the 2-core.  (q(i : ι) → Q2Presentation.Marking (G i) iι)) :
  Q2Presentation.AdmissibleQ2Presentation.Admissible.{u_1} {G : Type u_1} [Group G] [Finite G] (q : Q2Presentation.Marking G) : PropA marking is **admissible** when it generates, satisfies the tame and wild
relators, and sends `x₀, x₁` into the 2-core. 
    (Q2Presentation.diagonalSubdirectMarkingQ2Presentation.diagonalSubdirectMarking.{u_1, u_2} {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)]
  (q : (i : ι) → Q2Presentation.Marking (G i)) : Q2Presentation.Marking ↥(Q2Presentation.subdirectSubgroup q)The diagonal marking, corestricted to the subdirect subgroup it generates. 
      q(i : ι) → Q2Presentation.Marking (G i))

**Finite subdirect closure of admissibility** (manuscript Lemma 2.1).  If each
`q i` is admissible, then the corestricted diagonal marking into the subdirect
subgroup is admissible.

Lemma2.2

Group: The candidate as a profinite group (2)

Hover another entry in this group to preview it.

Preview

Lemma 2.1

Loading preview

Hover a group entry to preview it.

✓L∃∀Nused by 0

Lemma 2.2 of the paper (Cofinality).

Every finite quotient of \GA is an admissible marked quotient. In particular, \WA is pro-2.

Lean code for Lemma2.2●1 theorem

theoremdefined in Q2Presentation/Candidate/FiniteFactor.lean

complete

theorem Q2Presentation.GammaA_map_to_finite_factors {HType : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 HType]
  [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 HType]
  (φQ2Presentation.GammaA ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H) :
    Q2Presentation.GammaAQ2Presentation.GammaA : ProfiniteGrp.{0}The candidate profinite group `Γ_A`, the cofiltered inverse limit (in
`ProfiniteGrp`) of all admissible finite marked quotients (manuscript
eq. `candidateinverse`).  ⟶Quiver.Hom.{v, u} {V : Type u} [self : Quiver V] : V → V → Type vThe type of edges/arrows/morphisms between a given source and target.  ProfiniteGrp.ofFiniteGrpProfiniteGrp.ofFiniteGrp.{u_1} (G : FiniteGrp.{u_1}) : ProfiniteGrp.{u_1}A `FiniteGrp` when given the discrete topology can be considered as a profinite group.  (FiniteGrp.ofFiniteGrp.of.{u} (G : Type u) [Group G] [Finite G] : FiniteGrp.{u}Construct a term of `FiniteGrp` from a type endowed with the structure of a finite group.  HType)) :
  ∃ AQ2Presentation.AdmissibleIndex ψQ2Presentation.admissibleDiagram.obj A ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H),
    φQ2Presentation.GammaA ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      CategoryTheory.CategoryStruct.compCategoryTheory.CategoryStruct.comp.{v, u} {obj : Type u} [self : CategoryTheory.CategoryStruct.{v, u} obj]
  {X Y Z : obj} : (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)Composition of morphisms in a category, written `f ≫ g`. 
        (CategoryTheory.Limits.limit.πCategoryTheory.Limits.limit.π.{v₁, u₁, v, u} {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u}
  [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] (j : J) :
  CategoryTheory.Limits.limit F ⟶ F.obj jThe projection from the limit object to a value of the functor.  Q2Presentation.admissibleDiagramQ2Presentation.admissibleDiagram : CategoryTheory.Functor Q2Presentation.AdmissibleIndex ProfiniteGrp.{0}The inverse system of admissible finite marked quotients, as a functor into
`ProfiniteGrp`.  An admissible index `A` maps to its finite carrier `Fin A.n`
(discrete profinite group); a generator-preserving hom `f` maps to the induced
continuous group homomorphism. 
          AQ2Presentation.AdmissibleIndex)
        ψQ2Presentation.admissibleDiagram.obj A ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H)

theorem Q2Presentation.GammaA_map_to_finite_factors
  {HType : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 HType] [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 HType]
  (φQ2Presentation.GammaA ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H) :
    Q2Presentation.GammaAQ2Presentation.GammaA : ProfiniteGrp.{0}The candidate profinite group `Γ_A`, the cofiltered inverse limit (in
`ProfiniteGrp`) of all admissible finite marked quotients (manuscript
eq. `candidateinverse`).  ⟶Quiver.Hom.{v, u} {V : Type u} [self : Quiver V] : V → V → Type vThe type of edges/arrows/morphisms between a given source and target. 
      ProfiniteGrp.ofFiniteGrpProfiniteGrp.ofFiniteGrp.{u_1} (G : FiniteGrp.{u_1}) : ProfiniteGrp.{u_1}A `FiniteGrp` when given the discrete topology can be considered as a profinite group. 
        (FiniteGrp.ofFiniteGrp.of.{u} (G : Type u) [Group G] [Finite G] : FiniteGrp.{u}Construct a term of `FiniteGrp` from a type endowed with the structure of a finite group.  HType)) :
  ∃ AQ2Presentation.AdmissibleIndex ψQ2Presentation.admissibleDiagram.obj A ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H),
    φQ2Presentation.GammaA ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      CategoryTheory.CategoryStruct.compCategoryTheory.CategoryStruct.comp.{v, u} {obj : Type u} [self : CategoryTheory.CategoryStruct.{v, u} obj]
  {X Y Z : obj} : (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)Composition of morphisms in a category, written `f ≫ g`. 
        (CategoryTheory.Limits.limit.πCategoryTheory.Limits.limit.π.{v₁, u₁, v, u} {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u}
  [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] (j : J) :
  CategoryTheory.Limits.limit F ⟶ F.obj jThe projection from the limit object to a value of the functor. 
          Q2Presentation.admissibleDiagramQ2Presentation.admissibleDiagram : CategoryTheory.Functor Q2Presentation.AdmissibleIndex ProfiniteGrp.{0}The inverse system of admissible finite marked quotients, as a functor into
`ProfiniteGrp`.  An admissible index `A` maps to its finite carrier `Fin A.n`
(discrete profinite group); a generator-preserving hom `f` maps to the induced
continuous group homomorphism. 
          AQ2Presentation.AdmissibleIndex)
        ψQ2Presentation.admissibleDiagram.obj A ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H)

**Finite factorization (manuscript Lemma 2.2, plan §5 / work order B4).**

Every continuous homomorphism `φ : Γ_A ⟶ H` to a finite group factors through one
of the finite admissible quotients: there is an admissible index `A` and a
(continuous) homomorphism `ψ : Fin A.n ⟶ H` with `φ = π_A ≫ ψ`.

The proof transports the single-coordinate factorization `limit_finite_factor`
across the bridge `gammaIso`, then lifts `φ` over the surjection `π_A`
(`piMon_surjective`) using `MonoidHom.liftOfSurjective`: the kernel containment
`ker π_A ≤ ker φ` holds because `φ` is constant on `π_A`-fibres.  The lifted
monoid hom is continuous for free (`Fin A.n` is discrete), giving `ψ`.

Proof

Proved in §2 of the paper. Ingredients: Lemma 2.1.

Theorem2.3

Group: The candidate as a profinite group (2)

Hover another entry in this group to preview it.

Preview

Lemma 2.1

Loading preview

Hover a group entry to preview it.

✓L∃∀Nused by 0

Proposition 2.3 of the paper (Epimorphic finite-quotient semantics).

For every finite group G, epimorphisms \GA\twoheadrightarrow G are in natural bijection with generating quadruples (\sigma,\tau,x_0,x_1)\in G^4 satisfying (5), (6), and x_0,x_1\in O_2(G).

Lean code for Theorem2.3●2 declarations

defdefined in Q2Presentation/Candidate/EpiSemantics.lean

complete

def Q2Presentation.GammaA_epi_equiv_admissible (GType : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType]
  [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 GType] [NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 GType] :
  Q2Presentation.Profinite.SurjContHomQ2Presentation.Profinite.SurjContHom.{u} (P Q : ProfiniteGrp.{u}) : Type uA surjective continuous homomorphism of profinite groups (a profinite
"epimorphism", recorded as data: the morphism together with surjectivity of the
underlying map).  Q2Presentation.GammaAQ2Presentation.GammaA : ProfiniteGrp.{0}The candidate profinite group `Γ_A`, the cofiltered inverse limit (in
`ProfiniteGrp`) of all admissible finite marked quotients (manuscript
eq. `candidateinverse`). 
      (ProfiniteGrp.ofFiniteGrpProfiniteGrp.ofFiniteGrp.{u_1} (G : FiniteGrp.{u_1}) : ProfiniteGrp.{u_1}A `FiniteGrp` when given the discrete topology can be considered as a profinite group.  (FiniteGrp.ofFiniteGrp.of.{u} (G : Type u) [Group G] [Finite G] : FiniteGrp.{u}Construct a term of `FiniteGrp` from a type endowed with the structure of a finite group.  GType)) ≃Equiv.{u_1, u_2} (α : Sort u_1) (β : Sort u_2) : Sort (max (max 1 u_1) u_2)`α ≃ β` is the type of functions from `α → β` with a two-sided inverse. 
    {Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`. qQ2Presentation.Marking G //Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`. Q2Presentation.AdmissibleQ2Presentation.Admissible.{u_1} {G : Type u_1} [Group G] [Finite G] (q : Q2Presentation.Marking G) : PropA marking is **admissible** when it generates, satisfies the tame and wild
relators, and sends `x₀, x₁` into the 2-core.  qQ2Presentation.Marking G }Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`.

def Q2Presentation.GammaA_epi_equiv_admissible
  (GType : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType] [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 GType]
  [NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 GType] :
  Q2Presentation.Profinite.SurjContHomQ2Presentation.Profinite.SurjContHom.{u} (P Q : ProfiniteGrp.{u}) : Type uA surjective continuous homomorphism of profinite groups (a profinite
"epimorphism", recorded as data: the morphism together with surjectivity of the
underlying map). 
      Q2Presentation.GammaAQ2Presentation.GammaA : ProfiniteGrp.{0}The candidate profinite group `Γ_A`, the cofiltered inverse limit (in
`ProfiniteGrp`) of all admissible finite marked quotients (manuscript
eq. `candidateinverse`). 
      (ProfiniteGrp.ofFiniteGrpProfiniteGrp.ofFiniteGrp.{u_1} (G : FiniteGrp.{u_1}) : ProfiniteGrp.{u_1}A `FiniteGrp` when given the discrete topology can be considered as a profinite group. 
        (FiniteGrp.ofFiniteGrp.of.{u} (G : Type u) [Group G] [Finite G] : FiniteGrp.{u}Construct a term of `FiniteGrp` from a type endowed with the structure of a finite group.  GType)) ≃Equiv.{u_1, u_2} (α : Sort u_1) (β : Sort u_2) : Sort (max (max 1 u_1) u_2)`α ≃ β` is the type of functions from `α → β` with a two-sided inverse. 
    {Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`. qQ2Presentation.Marking G //Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`. Q2Presentation.AdmissibleQ2Presentation.Admissible.{u_1} {G : Type u_1} [Group G] [Finite G] (q : Q2Presentation.Marking G) : PropA marking is **admissible** when it generates, satisfies the tame and wild
relators, and sends `x₀, x₁` into the 2-core.  qQ2Presentation.Marking G }Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`.

**Epimorphic finite-quotient semantics (manuscript Proposition 2.3).**  For
every finite group `G`, the surjective continuous homomorphisms `Γ_A ↠ G` are in
natural bijection with the admissible markings of `G`.

Forward: a surjection induces an admissible marking of `G` via the exact-image
theorem with image `⊤` (`admissible_of_surj`).  Backward: an admissible marking
skeletalizes to an admissible stage whose limit projection, transported by
`skelEquiv`, is an epimorphism (`epiOfMarking`).  The two are mutually inverse
because a hom out of `Γ_A` is determined by its values on `gammaGen`
(`epiHom_ext`).

theoremdefined in Q2Presentation/Induction/Section7FrattiniTrivialElementary.lean

complete

theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateLowerBoundarySurjData
  {pQ2Presentation.Induction.FramedPair : Q2Presentation.Induction.FramedPairQ2Presentation.Induction.FramedPair : Type 1A **framed pair** `(𝒴, F)`: a boundary-framed marked target together with a
boundary frame for it (manuscript Definition 4.1 + `eq:beta`).  This is the index of
Theorem 4.2: the boundary-framed surjection count `e_Γ^β` is a function of the pair.
The induction of `sec:induction` ranges over *all* such pairs simultaneously
("the induction is stated globally", l.1213), ordered by `|L_Y|`. }
  (h¬Q2Presentation.Induction.ScalarTerminal p : ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.Q2Presentation.Induction.ScalarTerminalQ2Presentation.Induction.ScalarTerminal (p : Q2Presentation.Induction.FramedPair) : Prop**Scalar-terminal framed pair.**  pQ2Presentation.Induction.FramedPair)
  (chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p : Q2Presentation.Induction.FirstNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA non-scalar chief factor of `L_Y` that is **first**: every chief factor strictly
below it (i.e. with upper term contained in `lower`) is scalar.  This is the manuscript's
choice `S ◁ P` at l.3616–3623 ("all chief factors below `S` are scalar and `V` is the
first non-scalar simple factor"), which `lem:collapse` requires for the coprime step
`[S, Ñ] = 1`.  pQ2Presentation.Induction.FramedPair)
  (KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.)  chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p.toNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor.toNonScalarChiefFactor {p : Q2Presentation.Induction.FramedPair}
  (self : Q2Presentation.Induction.FirstNonScalarChiefFactor p) : Q2Presentation.Induction.NonScalarChiefFactor p)
  (hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1 : Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`.  ↥(Q2Presentation.Induction.kernelFrattiniQ2Presentation.Induction.kernelFrattini {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Subgroup p.fst.YThe literal Frattini subgroup `R = Φ(K)` of the kernel, as a subgroup of `Y`
(the manuscript's `R`, l.3626).  KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1) :
  NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.

    (Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerBoundarySurjDataQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerBoundarySurjData
  {p : Q2Presentation.Induction.FramedPair} (h : ¬Q2Presentation.Induction.ScalarTerminal p)
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1) : TypeA boundary-framed source map to the literal lower quotient `C = Y/K`.

This is a stricter manuscript-shaped provenance datum than a bare map
`Γ_A ↠ towerC K`: it records an actual candidate boundary-framed surjection to the
lower child constructed from the same quotient and the same inherited frame.  The bare
finite source-map packet below is recovered by forgetting the boundary-compatibility
proof and the framing predicate.

      h¬Q2Presentation.Induction.ScalarTerminal p chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1)

theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateLowerBoundarySurjData
  {pQ2Presentation.Induction.FramedPair :
    Q2Presentation.Induction.FramedPairQ2Presentation.Induction.FramedPair : Type 1A **framed pair** `(𝒴, F)`: a boundary-framed marked target together with a
boundary frame for it (manuscript Definition 4.1 + `eq:beta`).  This is the index of
Theorem 4.2: the boundary-framed surjection count `e_Γ^β` is a function of the pair.
The induction of `sec:induction` ranges over *all* such pairs simultaneously
("the induction is stated globally", l.1213), ordered by `|L_Y|`. }
  (h¬Q2Presentation.Induction.ScalarTerminal p :
    ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.Q2Presentation.Induction.ScalarTerminalQ2Presentation.Induction.ScalarTerminal (p : Q2Presentation.Induction.FramedPair) : Prop**Scalar-terminal framed pair.** 
        pQ2Presentation.Induction.FramedPair)
  (chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p :
    Q2Presentation.Induction.FirstNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA non-scalar chief factor of `L_Y` that is **first**: every chief factor strictly
below it (i.e. with upper term contained in `lower`) is scalar.  This is the manuscript's
choice `S ◁ P` at l.3616–3623 ("all chief factors below `S` are scalar and `V` is the
first non-scalar simple factor"), which `lem:collapse` requires for the coprime step
`[S, Ñ] = 1`. 
      pQ2Presentation.Induction.FramedPair)
  (KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.) 
      chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p.toNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor.toNonScalarChiefFactor {p : Q2Presentation.Induction.FramedPair}
  (self : Q2Presentation.Induction.FirstNonScalarChiefFactor p) : Q2Presentation.Induction.NonScalarChiefFactor p)
  (hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1 :
    Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`. 
        ↥(Q2Presentation.Induction.kernelFrattiniQ2Presentation.Induction.kernelFrattini {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Subgroup p.fst.YThe literal Frattini subgroup `R = Φ(K)` of the kernel, as a subgroup of `Y`
(the manuscript's `R`, l.3626). 
            KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      1) :
  NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.

    (Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerBoundarySurjDataQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerBoundarySurjData
  {p : Q2Presentation.Induction.FramedPair} (h : ¬Q2Presentation.Induction.ScalarTerminal p)
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1) : TypeA boundary-framed source map to the literal lower quotient `C = Y/K`.

This is a stricter manuscript-shaped provenance datum than a bare map
`Γ_A ↠ towerC K`: it records an actual candidate boundary-framed surjection to the
lower child constructed from the same quotient and the same inherited frame.  The bare
finite source-map packet below is recovered by forgetting the boundary-compatibility
proof and the framing predicate.

      h¬Q2Presentation.Induction.ScalarTerminal p chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1)

Former lower boundary-surjection leaf, now theorem-level from the finite admissible
marking with generator boundary compatibility.  The proof is exactly
`prop:epi-semantics`: an admissible finite marking gives `Γ_A ↠ C`; since both maps to
`H × E` agree on the four dense generators, the boundary-framed equation holds for all
`γ : Γ_A`.