Documentation Verification Report

GaloisConnection

📁 Source: Mathlib/Order/Rel/GaloisConnection.lean

Statistics

Metric	Count
Definitions `GaloisConnection`, `equivFixedPoints`, `leftDual`, `leftFixedPoints`, `rightDual`, `rightFixedPoints`	6
Theorems `gc_leftDual_rightDual`, `leftDual_mem_rightFixedPoint`, `leftDual_rightDual_le_of_le`, `rightDual_leftDual_le_of_le`, `rightDual_mem_leftFixedPoint`	5
Total	11

SetRel

Definitions

Name	Category	Theorems
`equivFixedPoints` 📖	CompOp	—
`leftDual` 📖	CompOp	4 math math: `rightDual_leftDual_le_of_le`, `leftDual_mem_rightFixedPoint`, `gc_leftDual_rightDual`, `leftDual_rightDual_le_of_le`
`leftFixedPoints` 📖	CompOp	1 math math: `rightDual_mem_leftFixedPoint`
`rightDual` 📖	CompOp	4 math math: `rightDual_leftDual_le_of_le`, `gc_leftDual_rightDual`, `rightDual_mem_leftFixedPoint`, `leftDual_rightDual_le_of_le`
`rightFixedPoints` 📖	CompOp	1 math math: `leftDual_mem_rightFixedPoint`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gc_leftDual_rightDual` 📖	mathematical	—	`GaloisConnection` `Set` `OrderDual` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `leftDual` `rightDual` `OrderDual.ofDual`	—	—
`leftDual_mem_rightFixedPoint` 📖	mathematical	—	`Set` `Set.instMembership` `rightFixedPoints` `leftDual`	—	`le_antisymm` `GaloisConnection.monotone_l` `gc_leftDual_rightDual` `GaloisConnection.le_u_l` `GaloisConnection.l_u_le`
`leftDual_rightDual_le_of_le` 📖	mathematical	`Set` `Set.instMembership` `rightFixedPoints` `Set.instLE`	`leftDual` `rightDual`	—	`GaloisConnection.monotone_l` `gc_leftDual_rightDual` `GaloisConnection.monotone_u`
`rightDual_leftDual_le_of_le` 📖	mathematical	`Set` `Set.instMembership` `leftFixedPoints` `Set.instLE`	`rightDual` `leftDual`	—	`GaloisConnection.monotone_u` `gc_leftDual_rightDual` `GaloisConnection.monotone_l`
`rightDual_mem_leftFixedPoint` 📖	mathematical	—	`Set` `Set.instMembership` `leftFixedPoints` `rightDual`	—	`le_antisymm` `GaloisConnection.monotone_u` `gc_leftDual_rightDual` `GaloisConnection.l_u_le` `GaloisConnection.le_u_l`

(root)

Definitions

Name	Category	Theorems
`GaloisConnection` 📖	MathDef	120 math math: `NonUnitalAlgebra.gc`, `Set.preimage_kernImage`, `Subgroup.gc_map_comap`, `Nat.galoisConnection_mul_div`, `FirstOrder.Language.Substructure.gc_map_comap`, `FloorDiv.floorDiv_gc`, `ProjectiveSpectrum.gc_homogeneousIdeal`, `ofAddUnits_addUnits_gc`, `ClosedSubmodule.orthogonal_gc`, `ENat.gc_toENNReal_floor`, `AlgebraicGeometry.Scheme.IdealSheafData.gc`, `PrimeSpectrum.gc`, `LieIdeal.gc_map_comap`, `Subsemiring.gc_map_comap`, `Filter.bind_smallSets_gc`, `CategoryTheory.Localization.LeftBousfield.galoisConnection`, `TopologicalSpace.Closeds.gc`, `gc_upperPolar_lowerPolar`, `Sublattice.gc_map_comap`, `gc_upperBounds_lowerBounds`, `SetRel.image_core_gc`, `gc_floorDiv_mul`, `NonUnitalSubsemiring.gc_map_comap`, `LowerAdjoint.gc`, `OrderIso.to_galoisConnection`, `FloorRing.gc_ceil_coe`, `fixingAddSubmonoid_fixedPoints_gc`, `Subsemigroup.gc_map_comap`, `CategoryTheory.Adjunction.gc`, `Ideal.homogeneousHull.gc`, `TopologicalSpace.Opens.gc`, `Finset.gc_map_inr_toRight`, `Subalgebra.gc_map_comap`, `AddSubmonoid.gc_map_comap`, `NonUnitalStarAlgebra.gc`, `ProjectiveSpectrum.gc_set`, `Filter.gc_comap_kernMap`, `Submodule.orthogonal_gc`, `Subfield.gc_map_comap`, `CategoryTheory.ObjectProperty.galoisConnection_isColocal`, `StarSubalgebra.gc_map_comap`, `CategoryTheory.MorphismProperty.gc_llp_rlp`, `Nat.gc_count_nth`, `Set.image_preimage`, `LowerAdjoint.gc'`, `ENat.gc_ceil_toENNReal`, `Int.gc_coe_floor`, `gc_sdiff_sup`, `gc_mul_ceilDiv`, `Nat.gc_ceil_coe`, `ofUnits_units_gc`, `gc_Ici_sInf`, `LinearMap.polar_gc`, `FloorSemiring.gc_ceil`, `Cardinal.toENatAux_gc`, `NonUnitalSubalgebra.gc_map_comap`, `Order.PFilter.sInf_gc`, `GaloisConnection.monotone_intro`, `gc_nhdsKer_interior`, `Subring.gc_map_comap`, `gc_upperClosure_coe`, `IntermediateField.gc_map_comap`, `ClosedSubmodule.gc_map_comap`, `Submodule.dualAnnihilator_gc`, `Submodule.gc_map_comap`, `AddSubgroup.gc_map_comap`, `MeasurableSpace.gc_comap_map`, `Cardinal.gc_ord_card`, `ProjectiveSpectrum.gc_ideal`, `CeilDiv.ceilDiv_gc`, `GaloisCoinsertion.gc`, `ContinuousMap.ideal_gc`, `AffineSubspace.gc_map_comap`, `PrimeSpectrum.gc_set`, `StarAlgebra.gc`, `gc_inf_himp`, `NonUnitalStarSubalgebra.gc_map_comap`, `GaloisConnection.id`, `gc_sSup_Iic`, `Submodule.torsion_gc`, `LieSubmodule.gc_map_comap`, `fixingSubmonoid_fixedPoints_gc`, `Submonoid.gc_map_comap`, `CategoryTheory.Sieve.galoisConnection`, `CategoryTheory.Sieve.functor_galoisConnection`, `Cardinal.enat_gc`, `MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection`, `TopologicalSpace.gc_generateFrom`, `SetRel.gc_leftDual_rightDual`, `fixingAddSubgroup_fixedPoints_gc`, `Int.gc_ceil_coe`, `TwoSidedIdeal.gc`, `fixingSubgroup_fixedPoints_gc`, `gc_nhds`, `FloorRing.gc_coe_floor`, `gc_floorDiv_smul`, `ConvexCone.gc_hull_coe`, `gc_smul_ceilDiv`, `NonUnitalSubring.gc_map_comap`, `Filter.gc_map_comap`, `Order.gc_pred_succ`, `IntermediateField.gc`, `LieSubmodule.gc_lcs_ucs`, `CategoryTheory.ObjectProperty.galoisConnection_isLocal`, `BooleanSubalgebra.gc_map_comap`, `gc_lowerClosure_coe`, `UniformFun.gc`, `Set.sUnion_powerset_gc`, `CategoryTheory.Subgroupoid.galoisConnection_map_comap`, `Finset.gc_map_inl_toLeft`, `PrimitiveSpectrum.gc`, `AlgebraicGeometry.Scheme.IdealSheafData.map_gc`, `Ideal.gc_map_comap`, `Algebra.gc`, `gc_coinduced_induced`, `LieSubalgebra.gc_map_comap`, `AddSubsemigroup.gc_map_comap`, `Ideal.homogeneousCore.gc`, `GaloisInsertion.gc`, `LieSubmodule.gc_top_lie_normalizer`

---

← Back to Index